Prove2Me

lean_workbook_plus_11280

Proved

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

Find the closed form for ana_n, given an=0.25⋅((2+1)2n−1−(2−1)2n−1+2)a_n = 0.25\cdot\left((\sqrt{2}+1)^{2n-1}-(\sqrt{2}-1)^{2n-1}+2\right).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11280 (a : ℕ → ℝ) (a_n : ∀ n, a n = 0.25 * ((Real.sqrt 2 + 1) ^ (2 * n - 1) - (Real.sqrt 2 - 1) ^ (2 * n - 1) + 2)) : ∃ f : ℕ → ℝ, ∀ n, a n = f n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph