Prove2Me

lean_workbook_plus_13360

Proved

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

Given the sequences xn{x_n} and yn{y_n} defined by x0=3,y0=2,xn=3xn−1+4yn−1,yn=2xn−1+3yn−1∀nx_0=3,y_0=2, x_n = 3x_{n-1}+4y_{n-1}, y_n = 2x_{n-1}+3y_{n-1} \forall n, prove that (xn,yn)(x_n, y_n) are roots of the Pell's equation: x2−2y2=1x^2-2y^2=1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13360 (x y : ℕ → ℕ) (hx : x 0 = 3) (hy : y 0 = 2) (hn: ∀ n, x (n + 1) = 3 * x n + 4 * y n) (h'n: ∀ n, y (n + 1) = 2 * x n + 3 * y n) : ∀ n, (x n)^2 - 2 * (y n)^2 = 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph