lean_workbook_plus_42239

Proved

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

Given that $a_1 = 1, a_2 = 2, a_3 = 2$ , and that $a_{n+3} = a_{n+2} + a_{n+1} - 2a_n$ find the explicit formula for $a_k$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42239 (a : ℕ → ℕ) (a1 : a 0 = 1) (a2 : a 1 = 2) (a3 : a 2 = 2) (a_rec : ∀ n, a (n + 3) = a (n + 2) + a (n + 1) - 2 * a n) : ∃ f : ℕ → ℕ, ∀ k, a k = f k   :=  by sorry

Source

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

View graph