Prove2Me

lean_workbook_plus_65788

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Adding the constraint xn≡1(mod4)x_n\equiv 1\pmod 4 , we get that we must keep one xnx_n every two And so : (x1,y1)=(17,6)(x_1,y_1)=(17,6) and (xn+1,yn+1)=(17xn+48yn,6xn+17yn)(x_{n+1},y_{n+1})=(17x_n+48y_n,6x_n+17y_n)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65788  (x y : ℕ → ℕ)
  (h₀ : x 0 = 17)
  (h₁ : y 0 = 6)
  (h₂ : ∀ n, x (n + 1) = 17 * x n + 48 * y n)
  (h₃ : ∀ n, y (n + 1) = 6 * x n + 17 * y n)
  (h₄ : ∀ n, x n ≡ 1 [ZMOD 4]) :
  ∃ n, 0 < n ∧ x n = y n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph