lean_workbook_plus_12307

Proved

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

Prove that $a_{n} > 2$ for all positive integers, given the sequence defined by $a_{n+1} = \sqrt{2+a_{n}}$ and $a_{1}=3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12307 (n : ℕ) (a : ℕ → ℝ) (a1 : a 0 = 3) (a_rec : ∀ n, a (n + 1) = Real.sqrt (2 + a n)) : ∀ n, a n > 2   :=  by sorry

Source