Prove2Me

Benford probabilities sum to 11 in every base b≥2b \ge 2

Proved
BenfordLaw.benfordProb_sum_eq_one

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

benford-lawequidistributionleading-digits

Let b≥2b \ge 2 be an integer base and Pb(d)=log⁡b ⁣(1+1d)P_b(d) = \log_b\!\left(1+\frac1d\right). Then the Benford probabilities of the digits 1,…,b−11,\dots,b-1 form a probability distribution:

∑d=1b−1log⁡b ⁣(1+1d)=1.\sum_{d=1}^{b-1} \log_b\!\left(1+\frac1d\right) = 1 .

This is the normalization that makes the first-digit law a genuine probability law in every base.

Preamble
import Mathlib
import Definitions.Def_BenfordLaw_Defs
Formal statement
namespace BenfordLaw

theorem benfordProb_sum_eq_one (b : ℕ) (hb : 2 ≤ b) :
    ∑ d ∈ Finset.Icc 1 (b - 1), benfordProb b d = 1 := by sorry

end BenfordLaw
Source
Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, sections "Definition" and "In other bases" (formula P(d)=log⁡b(d+1)−log⁡bdP(d)=\log_b(d+1)-\log_b d).
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.

For every natural number bb with b≥2b \ge 2:

∑d=1b−1benfordProb(b,d)=1,\sum_{d=1}^{b-1} \mathrm{benfordProb}(b,d) = 1,

where dd ranges over the naturals in the closed interval [1,b−1][1, b-1] (natural-number subtraction; since b≥2b\ge2, b−1≥1b-1 \ge 1 and the range is nonempty) and benfordProb(b,d)=log⁡b(1+1/d)=ln⁡(1+1/d)/ln⁡b\mathrm{benfordProb}(b,d) = \log_b(1+1/d) = \ln(1+1/d)/\ln b. No other hypotheses.

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