lean_workbook_plus_24368

Proved

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

Find a formula $a_n$ in term of $n$ for the sequence $\{a_n\}$ defined by $a_0=1$ and $a_{n+1}=5a_n\left(5a_n^4-5a_n^2+1\right)$ for all $n\geq0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24368 (a : ℕ → ℕ) (a0 : a 0 = 1) (a_rec : ∀ n, a (n + 1) = 5 * a n * (5 * (a n)^4 - 5 * (a n)^2 + 1)) : ∃ f : ℕ → ℕ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph