lean_workbook_plus_7081

Proved

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

Find the limit of the sequence $a_n$ defined by $a_1=2$ , $a_2=-2$ , and $a_{n+1}=\frac{1}{2}(a_n^2-a_{n-1})$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7081 (a : ℕ → ℝ) (a1 : a 0 = 2) (a2 : a 1 = -2) (a_rec : ∀ n, a (n + 1) = (a n)^2 / 2 - a (n - 1) / 2) : ∃ l, ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - l| < ε   :=  by sorry

Source

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

View graph