lean_workbook_plus_34115

Proved

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

Given sequence u_{n} determined by $u_{0} = 6;u_{1} = 42$ and $u_{n + 2} = u_{n + 1} + 6u_{n} + 6n$ . Find the general formula of $u_n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34115 (n:ℕ) (u : ℕ → ℕ) (h₁ : u 0 = 6) (h₂ : u 1 = 42) (h₃ : ∀ n, u (n + 2) = u (n + 1) + 6 * u n + 6 * n) : ∃ f:ℕ → ℕ, ∀ n, u n = f n   :=  by sorry

Source

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

View graph