Benford's law: leading digits, Benford probabilities, Benford sequences

Definition

BenfordLaw_Defs

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

benford-lawequidistributionleading-digits

Core definitions for Benford's law in an integer base $b$ (in the theorems $b \ge 2$ , usually $b = 10$ ). Write $\{t\} = t - \lfloor t\rfloor$ for the fractional part.

Leading digit. $D_b(x) = \left\lfloor b^{\{\log_b |x|\}}\right\rfloor$ . For $x \ne 0$ , writing $|x| = m\,b^e$ with $1 \le m < b$ , $e\in\mathbb Z$ , this is $\lfloor m\rfloor\in\{1,\dots,b-1\}$ .
First $k$ digits. $D_b^{(k)}(x) = \left\lfloor b^{\{\log_b |x|\} + k - 1}\right\rfloor$ , the integer formed by the first $k$ significant digits (leading zeros discarded).
$n$ -th digit. $\mathrm{dig}_b^{(n)}(x) = D_b^{(n)}(x) \bmod b$ .
Benford probability. $P_b(d) = \log_b\!\left(1 + \frac1d\right) = \log_b(d+1) - \log_b d$ .
Digit frequency. For a real sequence $(a_n)_{n\ge0}$ , $\mathrm{freq}_{b,d}(a, N) = \frac{1}{N}\#\{0\le n<N : D_b(a_n)=d\}$ .
Benford sequence. $(a_n)$ satisfies Benford's law in base $b$ if $\mathrm{freq}_{b,d}(a,N) \to P_b(d)$ as $N\to\infty$ for every $1 \le d < b$ .
Strong form (uniform log-significand). A random variable $X$ on $(\Omega,\mathbb P)$ has a uniform log-significand in base $b$ if $X$ is measurable, $X>0$ almost surely, and the law of $\{\log_b X\}$ is the uniform (Lebesgue) distribution on $[0,1)$ .

These are the objects in which every statement of the mission is phrased.

Formalization Note. Real.logb uses $\log|x|$ , so $D_b(-x) = D_b(x)$ , and $D_b(0) = 1$ (junk value). For $N = 0$ the frequency is $0/0 = 0$ . The strong-form predicate is a Prop-valued definition HasUniformLogMantissa b P X; it forces $\mathbb P(\Omega)=1$ .

Definition code

import Mathlib

/-!
# Benford's law — core definitions

Shared definitions for the Benford's-law mission (source: Wikipedia, "Benford's law").
-/

namespace BenfordLaw

/-- The leading (most significant) digit of `x` in base `b`: writing `|x| = m · b^e` with
`1 ≤ m < b` and `e ∈ ℤ`, this is `⌊m⌋`. It is computed as `⌊b ^ frac(log_b |x|)⌋`.
(Junk value: for `x = 0` this returns `1`.) -/
noncomputable def leadingDigit (b : ℕ) (x : ℝ) : ℕ :=
  ⌊(b : ℝ) ^ Int.fract (Real.logb b x)⌋₊

/-- The integer formed by the first `k` significant digits of `x` in base `b`
(leading zeros discarded): `⌊m · b^(k-1)⌋` where `|x| = m · b^e`, `1 ≤ m < b`. -/
noncomputable def leadingDigits (b k : ℕ) (x : ℝ) : ℕ :=
  ⌊(b : ℝ) ^ (Int.fract (Real.logb b x) + ((k : ℝ) - 1))⌋₊

/-- The `n`-th significant digit of `x` in base `b` (`n = 1` is the leading digit). -/
noncomputable def digitAt (b n : ℕ) (x : ℝ) : ℕ :=
  leadingDigits b n x % b

/-- The Benford probability of leading digit `d` in base `b`:
`log_b (d + 1) - log_b d = log_b (1 + 1/d)`. -/
noncomputable def benfordProb (b d : ℕ) : ℝ :=
  Real.logb b (1 + 1 / (d : ℝ))

/-- Relative frequency of leading digit `d` (base `b`) among the first `N` terms
`a 0, …, a (N-1)` of a sequence. -/
noncomputable def digitFreq (b d : ℕ) (a : ℕ → ℝ) (N : ℕ) : ℝ :=
  (((Finset.range N).filter (fun n => leadingDigit b (a n) = d)).card : ℝ) / N

/-- A real sequence satisfies Benford's law (exactly, in the asymptotic limit) in base `b`
if for every digit `1 ≤ d < b` the relative frequency of leading digit `d` among the first
`N` terms tends to `log_b (1 + 1/d)` as `N → ∞`. -/
def IsBenfordSeq (b : ℕ) (a : ℕ → ℝ) : Prop :=
  ∀ d : ℕ, 1 ≤ d → d < b →
    Filter.Tendsto (digitFreq b d a) Filter.atTop (nhds (benfordProb b d))

/-- Strong form of Benford's law for a random variable: `X` is measurable, almost surely
positive, and the fractional part of `log_b X` is uniformly distributed on `[0, 1)`. -/
def HasUniformLogMantissa {Ω : Type*} [MeasurableSpace Ω] (b : ℕ)
    (P : MeasureTheory.Measure Ω) (X : Ω → ℝ) : Prop :=
  Measurable X ∧ (∀ᵐ ω ∂P, 0 < X ω) ∧
    P.map (fun ω => Int.fract (Real.logb b (X ω))) =
      MeasureTheory.volume.restrict (Set.Ico (0 : ℝ) 1)

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, sections "Definition", "In other bases", "Generalization to digits beyond the first", "Distributions known to obey Benford's law".

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.

The file defines, in namespace BenfordLaw, the following objects (all real logarithms are $\log_b|x| = \ln|x| / \ln b$ , Lean's convention, and $\{t\}=t-\lfloor t\rfloor$ ).

$\mathrm{leadingDigit}(b, x) = \lfloor b^{\{\log_b x\}}\rfloor_{\mathbb N}$ (floor into the naturals, which is $0$ for negative arguments). For $x=0$ , $\log_b 0 = 0$ , so the value is $\lfloor 1\rfloor = 1$ . For $b = 0$ or $b = 1$ , $\log_b$ divides by $\ln b \le 0$ (with $\ln 0 = \ln 1 = 0$ , so $\log_b x = 0$ ) and the value is $\lfloor b^0 \rfloor = 1$ ; no base restriction is built into the definition.
$\mathrm{leadingDigits}(b, k, x) = \lfloor b^{\{\log_b x\} + (k - 1)}\rfloor_{\mathbb N}$ , where $k-1$ is computed in $\mathbb R$ (so $k = 0$ gives exponent $\{\log_b x\} - 1$ , a value in $[b^{-1},1)$ , floor $0$ ).
$\mathrm{digitAt}(b, n, x) = \mathrm{leadingDigits}(b, n, x) \bmod b$ (natural-number remainder; $\bmod\ 0$ is the identity).
$\mathrm{benfordProb}(b, d) = \log_b(1 + 1/d)$ with $1/d$ real division; for $d = 0$ this is $\log_b 1 = 0$ .
$\mathrm{digitFreq}(b, d, a, N) = \#\{n \in \{0,\dots,N-1\} : \mathrm{leadingDigit}(b, a_n) = d\} / N$ in $\mathbb R$ ; for $N=0$ this is $0$ .
$\mathrm{IsBenfordSeq}(b, a)$ holds iff for every natural $d$ with $1 \le d < b$ , $\mathrm{digitFreq}(b,d,a,N) \to \mathrm{benfordProb}(b,d)$ as $N \to \infty$ (along the naturals). For $b \le 1$ the condition is vacuous, so every sequence qualifies.
For a measurable space $\Omega$ , a measure $P$ (not assumed to be a probability measure) and $X:\Omega\to\mathbb R$ : $\mathrm{HasUniformLogMantissa}(b,P,X)$ holds iff (i) $X$ is measurable, (ii) $X(\omega)>0$ for $P$ -almost every $\omega$ , and (iii) the pushforward measure of $P$ under $\omega\mapsto\{\log_b X(\omega)\}$ equals Lebesgue measure restricted to $[0,1)$ . (If the map were not a.e.-measurable the pushforward would be the zero measure, so (iii) cannot hold then; (iii) also forces $P(\Omega) = 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