lean_workbook_plus_54602

Proved

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

Find a closed form expression for $a_n$ in the sequence defined by $a_n=a_{n-1}^2-2$ with $a_0=3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54602 (a : ℕ → ℤ) (a0 : a 0 = 3) (a_rec : ∀ n, a (n + 1) = a n ^ 2 - 2) : ∃ f : ℕ → ℤ, ∀ n, a n = f n   :=  by sorry

Source