lean_workbook_plus_62528

Proved

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

Prove that the sequence $a_n = \sqrt{3a_{n-1} + 1}$ is strictly increasing and bounded above.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62528 (a : ℕ → ℝ) (ha : a 0 = 1) (hab : ∀ n, a (n + 1) = Real.sqrt (3 * a n + 1)) : ∃ M, ∀ n, a n < M   :=  by sorry

Source