Prove2Me

Lean-Workbook Plus 78499: Last digits of the first five factorials

Proved
WorkbookRestored.plus_78499

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

lean-workbookrestored-importssource-checked

Let f(n)=n−10⌊n/10⌋f(n)=n-10\lfloor n/10\rfloor for natural nn. Then f(0!)+f(1!)+f(2!)+f(3!)+f(4!)=14f(0!)+f(1!)+f(2!)+f(3!)+f(4!)=14.

Source: Lean-Workbook row lean_workbook_plus_78499 (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.Algebra.Order.Floor.Semiring
open Nat
Formal statement
theorem WorkbookRestored.plus_78499 (f : ℕ → ℕ) (f_def : ∀ n, f n = n - 10 * Nat.floor (n / 10)) : f 0! + f 1! + f 2! + f 3! + f 4! = 14   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_78499; immutable original Prove2Me node 0e8f509e-47eb-4e5f-b0e3-e138a03ce7a2

View graph