lean_workbook_plus_51878

Proved

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

Find a closed form for the sequence $(a_n)_{n=0}^{\infty}$ defined as: $a_0=1$ , $a_1=2$ , $a_{n}=4a_{n-1}-5a_{n-2}$ for $n>1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51878 (a : ℕ → ℝ) (a0 : a 0 = 1) (a1 : a 1 = 2) (a_rec : ∀ n, n > 1 → a n = 4 * a (n - 1) - 5 * a (n - 2)) : ∃ f : ℕ → ℝ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph