lean_workbook_plus_80412

Proved

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

Find the closed form of the sequence $(a_n)$ defined as $a_1 = 33$ , $a_2 = 49$ , $a_3 = 177$ , and $a_{n+3} = 8a_{n+2} - 8a_{n+1} + a_n$ for all $n \geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80412 (a : ℕ → ℤ) (a1 : a 0 = 33) (a2 : a 1 = 49) (a3 : a 2 = 177) (a_rec : ∀ n, n ≥ 1 → a (n + 3) = 8 * a (n + 2) - 8 * a (n + 1) + a n) : ∃ f : ℕ → ℤ, ∀ n, n ≥ 1 → a n = f n   :=  by sorry

Source

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

View graph