lean_workbook_plus_74239

Disproved

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

We have $a_1=2$ and $a_{n+1}=10a_n+2n+2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74239 (n : ℕ) (f : ℕ → ℕ) (hf: f 1 = 2 ∧ ∀ n, f (n + 1) = 10 * f n + 2 * n + 2): f n = 12 * 10 ^ (n - 1) + 2 * n - 10   :=  by sorry

Source

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

View graph