lean_workbook_plus_63364

Proved

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

Find a closed form for the sequence $u_n$ defined by $u_1=2, u_2=8$ and $u_{n+2}=4u_{n+1}-u_n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63364 (u : ℕ → ℕ) (u1 : u 0 = 2) (u2 : u 1 = 8) (un : ∀ n, u (n + 2) = 4 * u (n + 1) - u n) : ∃ f : ℕ → ℕ, ∀ n, u n = f n   :=  by sorry

Source

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

View graph