lean_workbook_plus_76064

Proved

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

A sequence $\{a_n\}^\infty_{n=0}$ of positive integers satisfy $a_0=0$ , $a_1=2$ , and $a_n+a_{n-2}=2(a_{n-1}+1)$ for all integers $n\ge2$ . Find a closed-form formula for $a_n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76064 (a : ℕ → ℕ) (a0 : a 0 = 0) (a1 : a 1 = 2) (a_rec : ∀ n, n ≥ 2 → a n + a (n - 2) = 2 * (a (n - 1) + 1)) : ∃ f : ℕ → ℕ, ∀ n, a n = f n   :=  by sorry

Source

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

View graph