lean_workbook_plus_55354

Proved

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

Given the sequence $a_1=1$ and $a_{n+1}=\frac{{a_n}^2+3}{a_n+1}$ , find the formula for $a_n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55354 (a : ℕ → ℚ) (a1 : a 0 = 1) (a_rec : ∀ n, a (n + 1) = (a n ^ 2 + 3) / (a n + 1)) : ∃ f : ℕ → ℚ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph