lean_workbook_plus_79552

Proved

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

A sequence $(a_n)$ is defined by means of the recursion $a_1 = 1, a_{n+1} = \frac{1 + 4a_n +\sqrt{1+ 24a_n}}{16}.$ Find an explicit formula for $a_n.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79552 (a : ℕ → ℚ) (a1 : a 0 = 1) (a_rec : ∀ n, a (n + 1) = (1 + 4 * a n + Real.sqrt (1 + 24 * a n)) / 16) : ∃ f : ℕ → ℚ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph