First $k$ digits equal $n$ with probability $\log_{10}(1+1/n)$

Proved

BenfordLaw.leadingDigits_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)$ . Let $k\ge1$ and let $n$ be a $k$ -digit integer, $10^{k-1}\le n<10^k$ . Then the probability that $X$ starts with the string of digits $n$ (leading zeros discarded) is

\mathbb P\big(D^{(k)}_{10}(X) = n\big) = \log_{10}(n+1)-\log_{10}(n) = \log_{10}\!\left(1+\frac1n\right).

For example, the probability of starting with the digits $3,1,4$ is $\log_{10}(1+1/314)\approx 0.00138$ .

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem leadingDigits_prob_of_uniform_log_mantissa {Ω : Type*} [MeasurableSpace Ω]
    (P : MeasureTheory.Measure Ω) (X : Ω → ℝ) (hX : HasUniformLogMantissa 10 P X)
    (k n : ℕ) (hk : 1 ≤ k) (hn1 : 10 ^ (k - 1) ≤ n) (hn2 : n < 10 ^ k) :
    (P {ω | leadingDigits 10 k (X ω) = n}).toReal = Real.logb 10 (1 + 1 / (n : ℝ)) := 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

\log_{10}(n+1)-\log_{10}(n)=\log_{10}(1+1/n)

, ref. Hill 1995, https://doi.org/10.1080/00029890.1995.11990578).

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:\Omega\to\mathbb R$ satisfy $\mathrm{HasUniformLogMantissa}(10,P,X)$ (measurable, positive a.e., $\{\log_{10}X\}$ has law Lebesgue on $[0,1)$ ). For all naturals $k,n$ with $k\ge1$ , $10^{k-1}\le n$ (natural subtraction) and $n<10^k$ :

P\{\omega : \lfloor 10^{\{\log_{10}X(\omega)\}+(k-1)}\rfloor = n\} \ (\text{as a real}) = \log_{10}(1+1/n).

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

First kkk digits equal nnn with probability log⁡10(1+1/n)\log_{10}(1+1/n)log10​(1+1/n)

First $k$ digits equal $n$ with probability $\log_{10}(1+1/n)$