Prove2Me

The factorials satisfy Benford's law

Proved
BenfordLaw.factorial_isBenfordSeq

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

benford-lawequidistributionleading-digits

The sequence of factorials 1!,2!,3!,…1!, 2!, 3!, \dots satisfies Benford's law in base 1010: for every d∈{1,…,9}d\in\{1,\dots,9\},

lim⁡N→∞#{1≤n≤N:D10(n!)=d}N=log⁡10 ⁣(1+1d).\lim_{N\to\infty}\frac{\#\{1\le n\le N : D_{10}(n!)=d\}}{N}=\log_{10}\!\left(1+\frac1d\right).

Formalization Note. Encoded as IsBenfordSeq 10 (fun n => ((n + 1).factorial : ℝ)).

Preamble
import Mathlib
import Definitions.Def_BenfordLaw_Defs
Formal statement
namespace BenfordLaw

theorem factorial_isBenfordSeq :
    IsBenfordSeq 10 (fun n => ((n + 1).factorial : ℝ)) := by sorry

end BenfordLaw
Source
Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Distributions known to obey Benford's law" ("the factorials", ref. [56]).
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent reader, and no reviewer should treat it as one. Please compare it against the Lean code yourself.

IsBenfordSeq(10,a)\mathrm{IsBenfordSeq}(10,a) with an=(n+1)!a_n = (n+1)! cast to R\mathbb R, n=0,1,2,…n=0,1,2,\dots (so a=(1,2,6,24,… )a=(1,2,6,24,\dots)). Unfolded: for every natural 1≤d<101\le d<10, the proportion of n∈{0,…,N−1}n\in\{0,\dots,N-1\} with ⌊10{log⁡10(n+1)!}⌋=d\lfloor 10^{\{\log_{10} (n+1)!\}}\rfloor = d tends to log⁡10(1+1/d)\log_{10}(1+1/d) as N→∞N\to\infty.

Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph