lean_workbook_plus_78696

Proved

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

Let $U_{1}=1$ , and $U_{n+1}= U_{n}+ 3n^{2}+ 5n^{4}$ for all $n\geq 1$ . Find the general closed formula for $U_{n}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78696 (U : ℕ → ℕ) (h : U 1 = 1 ∧ ∀ n, U (n + 1) = U n + 3 * n ^ 2 + 5 * n ^ 4) : ∃ f : ℕ → ℕ, ∀ n, U n = f n   :=  by sorry

Source

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

View graph