Prove2Me

lean_workbook_plus_79665

Proved

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

Construct a series {xn,yn}\{x_n,y_n\} as follows: x1=y1=1x_1=y_1=1, xn+1=(2d+1)xn+(2d+2)ynx_{n+1}=(2d+1)x_n+(2d+2)y_n, yn+1=2dxn+(2d+1)yny_{n+1}=2dx_n+(2d+1)y_n. Show that dxn2+1=(d+1)yn2,∀ndx_n^2+1=(d+1)y_n^2, \forall n.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79665 (d : ℕ) (x y : ℕ → ℕ) (h₀ : x 1 = 1 ∧ y 1 = 1) (h₁ : ∀ n, x (n + 1) = (2 * d + 1) * x n + (2 * d + 2) * y n) (h₂ : ∀ n, y (n + 1) = 2 * d * x n + (2 * d + 1) * y n) : ∀ n, d * x n ^ 2 + 1 = (d + 1) * y n ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph