Prove2Me

lean_workbook_plus_72773

Proved

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

Find the value of x9x_9 in the recursive sequence xn+1=2n+xnx_{n+1}=2n+x_n given x10=91x_{10}=91.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72773 (x : ℕ → ℕ) (h₁ : x 10 = 91) (h₂ : ∀ n, x (n + 1) = 2 * n + x n) : x 9 = 73   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph