Uniform $\{\log_b X\}$ implies the first-digit law

Proved

BenfordLaw.benford_of_uniform_log_mantissa

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

benford-lawequidistributionleading-digits

Let $b\ge2$ and let $X$ be a random variable on a probability space $(\Omega,\mathcal F,\mathbb P)$ such that $X > 0$ almost surely and the fractional part $\{\log_b X\}$ is uniformly distributed on $[0,1)$ . Then for every digit $d\in\{1,\dots,b-1\}$ ,

\mathbb P\big(D_b(X) = d\big) = \log_b\!\left(1+\frac1d\right).

This is the derivation of Benford's law from its strong form stated in the source.

Formalization Note. The hypothesis is HasUniformLogMantissa b P X; it includes measurability of $X$ and forces $\mathbb P$ to be a probability measure. The probability is stated as (P {ω | leadingDigit b (X ω) = d}).toReal.

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem benford_of_uniform_log_mantissa {Ω : Type*} [MeasurableSpace Ω]
    (b : ℕ) (hb : 2 ≤ b) (P : MeasureTheory.Measure Ω) (X : Ω → ℝ)
    (hX : HasUniformLogMantissa b P X) (d : ℕ) (hd1 : 1 ≤ d) (hdb : d < b) :
    (P {ω | leadingDigit b (X ω) = d}).toReal = benfordProb b d := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Definition" ("this is the distribution expected if the logarithms of the numbers ... are uniformly and randomly distributed"; "Benford's law is sometimes stated in a stronger form ...").

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.

Let $\Omega$ be any type with a $\sigma$ -algebra, $P$ any measure on it, $X:\Omega\to\mathbb R$ , and $b$ a natural number with $b\ge2$ . Assume $\mathrm{HasUniformLogMantissa}(b,P,X)$ : $X$ is measurable, $X>0$ $P$ -a.e., and the pushforward of $P$ under $\omega\mapsto\{\log_b X(\omega)\}$ is Lebesgue measure on $[0,1)$ . Then for every natural $d$ with $1\le d<b$ ,

P\big(\{\omega : \lfloor b^{\{\log_b X(\omega)\}}\rfloor = d\}\big) \text{ (converted from } [0,\infty] \text{ to } \mathbb R) = \log_b(1+1/d).

The conversion maps $\infty$ to $0$ , but the measure here is at most $1$ .

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

Uniform {log⁡bX}\{\log_b X\}{logb​X} implies the first-digit law

Uniform $\{\log_b X\}$ implies the first-digit law