lean_workbook_plus_58747

Proved

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

Find the closed form of the sequence $a_1 = 4, a_2 = 7,$ and $a_{n+1} = 2a_n - a_{n-1} + 2$ for $n \geq 2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58747 (a : ℕ → ℝ) (a1 : a 0 = 4) (a2 : a 1 = 7) (a_rec : ∀ n, n ≥ 2 → a (n + 1) = 2 * a n - a (n - 1) + 2) : ∃ f : ℕ → ℝ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph