lean_workbook_plus_81176

Proved

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

Prove that the sequence defined by $a_{n+1}=3a_{n-1}+\sqrt{8(a_n^2+a_{n-1}^2)}$ with $a_0=1$ and $a_1=41$ is all integers for $n\ge0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81176 (n : ℕ) (a : ℕ → ℝ) (a0 : a 0 = 1) (a1 : a 1 = 41) (a_rec : ∀ n, a (n + 1) = 3 * a (n - 1) + Real.sqrt (8 * (a n ^ 2 + a (n - 1) ^ 2))) : ∀ n, a n = ⌊a n⌋   :=  by sorry

Source

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

View graph