lean_workbook_plus_54386

Proved

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

Let $x_1=0$ and $x_{n+1}=5x_n+\sqrt{24x_n^2+1}$ . Prove $x_n$ is always a non-negative integer.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54386 (x : ℕ → ℝ) (x0 : x 0 = 0) (x_rec : ∀ n, x (n + 1) = 5 * x n + Real.sqrt (24 * (x n)^2 + 1)) : ∀ n, 0 ≤ x n   :=  by sorry

Source

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

View graph