lean_workbook_plus_66489

Proved

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

Let $a_1= 1, a_2 = 7, a_{n+2} = 2a_{n+1} +15a_n$ where $n$ belongs in the set of natural numbers. Find a formula for $a_n$ in terms of $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66489 (a : ℕ → ℕ) (a1 : a 0 = 1) (a2 : a 1 = 7) (a_rec : ∀ n, a (n + 2) = 2 * a (n + 1) + 15 * a n) : ∃ f : ℕ → ℕ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph