lean_workbook_plus_28337

Proved

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

Note that $a_n=\frac{(2+\sqrt{3})^{2n+1}+(2-\sqrt{3})^{2n+1}}{4}$ . Define $b_n:=\frac{1}{\sqrt{2}}\left(\left(\frac{\sqrt{3}+1}{\sqrt{2}}\right)^{2n+1}-\left(\frac{\sqrt{3}-1}{\sqrt{2}}\right)^{2n+1}\right)$ . We see that $\left\{b_n\right\}$ satisfies $b_0=1$ , $b_1=5$ , and $b_n=4b_{n-1}-b_{n-2}$ for all $n \geq 2$ . Note that $b_n$ is odd for each $n$ . Now, we may write $a_n=\left(\frac{b_n+1}{2}\right)^2+\left(\frac{b_n-1}{2}\right)^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28337  (a : ℕ → ℕ)
  (b : ℕ → ℕ)
  (h₀ : b 0 = 1)
  (h₁ : b 1 = 5)
  (h₂ : ∀ n ≥ 2, b n = 4 * b (n - 1) - b (n - 2))
  (h₃ : ∀ n, Odd (b n))
  (h₄ : ∀ n, a n = (b n + 1)^2 / 2^2 + (b n - 1)^2 / 2^2) :
  ∀ n, ∃ x y : ℕ, a n = x^2 + y^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph