Lean-Workbook Plus 71937: A rational recurrence and factorial evaluation

Proved

WorkbookRestored.plus_71937

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Let $f(0)=1$ and $f(x)=[f(x-1)+1]/(x+1)$ for natural $x\ge1$ . Then $(0!+1!+\cdots+7!)/f(7)=8!$ .

Source: Lean-Workbook row lean_workbook_plus_71937 (Apache-2.0), original record. This repair only restores required imports and namespaces; the mathematical declaration is unchanged.

Preamble

import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Rat.Defs
open Nat

Formal statement

theorem WorkbookRestored.plus_71937 (f : ℕ → ℚ) (f_def : f 0 = 1 ∧ ∀ x, 1 ≤ x → f x = (f (x - 1) + 1) / (x + 1)) : (0! + 1! + 2! + 3! + 4! + 5! + 6! + 7!) / f 7 = 8!   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_71937; immutable original Prove2Me node 27859aa1-22fb-4584-b2fd-b245f2ec76a9

View graph