Distribution of the $n$ -th significant digit

Proved

BenfordLaw.digitAt_prob_of_uniform_log_mantissa

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

benford-lawequidistributionleading-digits

Let $X$ be a positive random variable whose log-significand $\{\log_{10}X\}$ is uniformly distributed on $[0,1)$ . For every position $n\ge2$ and every digit $d\in\{0,1,\dots,9\}$ , the probability that $d$ is the $n$ -th significant digit of $X$ is

\mathbb P\big(\mathrm{dig}^{(n)}_{10}(X) = d\big) = \sum_{k=10^{n-2}}^{10^{n-1}-1}\log_{10}\!\left(1+\frac{1}{10k+d}\right).

For $n = 2$ , $d = 2$ this is $\log_{10}(1+\tfrac1{12})+\log_{10}(1+\tfrac1{22})+\dots+\log_{10}(1+\tfrac1{92})\approx0.109$ .

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem digitAt_prob_of_uniform_log_mantissa {Ω : Type*} [MeasurableSpace Ω]
    (P : MeasureTheory.Measure Ω) (X : Ω → ℝ) (hX : HasUniformLogMantissa 10 P X)
    (n : ℕ) (hn : 2 ≤ n) (d : ℕ) (hd : d ≤ 9) :
    (P {ω | digitAt 10 n (X ω) = d}).toReal =
      ∑ k ∈ Finset.Ico (10 ^ (n - 2) : ℕ) (10 ^ (n - 1)),
        Real.logb 10 (1 + 1 / (10 * (k : ℝ) + d)) := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Generalization to digits beyond the first" (formula for the probability that d is the n-th digit, n > 1).

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$ carry a $\sigma$ -algebra and a measure $P$ , and let $X$ satisfy $\mathrm{HasUniformLogMantissa}(10,P,X)$ . For all naturals $n\ge2$ and $d\le9$ :

P\{\omega : \lfloor 10^{\{\log_{10}X(\omega)\}+(n-1)}\rfloor \bmod 10 = d\}\ (\text{as a real}) = \sum_{k=10^{n-2}}^{10^{n-1}-1}\log_{10}\!\left(1+\frac{1}{10k+d}\right),

the sum running over naturals $k$ with $10^{n-2}\le k<10^{n-1}$ (exponents are natural-number differences, fine since $n\ge2$ ), and $10k+d$ computed in $\mathbb R$ .

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

Distribution of the nnn-th significant digit

Distribution of the $n$ -th significant digit