Prove2Me

lean_workbook_plus_25398

Proved

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

Find the closed form of the sequence {μn}\{\mu_n\} defined by μ0=2,μ1=4,\mu_0 = 2, \mu_1= 4, and μn=4μn−1+μn−2\mu_n = 4\mu_{n-1} + \mu_{n-2} for all n≥2n \geq 2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25398 (μ : ℕ → ℕ) (h₀ : μ 0 = 2) (h₁ : μ 1 = 4) (h₂ : ∀ n ≥ 2, μ n = 4 * μ (n - 1) + μ (n - 2)) : ∃ f : ℕ → ℕ, ∀ n, μ n = f n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph