Prove2Me

lean_workbook_plus_53966

Proved

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

Find a closed form for the sequence defined by an=2an−1+an−2a_n=2a_{n-1}+a_{n-2} with initial conditions a0=1,a1=3a_0=1, a_1=3.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53966 (a : ℕ → ℝ) (a0 : a 0 = 1) (a1 : a 1 = 3) (a_rec : ∀ n, a (n + 2) = 2 * a (n + 1) + a n) : ∃ f : ℕ → ℝ, ∀ n, a n = f n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph