The $n$ -th digit becomes uniform as $n\to\infty$

Proved

BenfordLaw.nth_digit_prob_tendsto_uniform

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

benford-lawequidistributionleading-digits

For every digit $d\in\{0,\dots,9\}$ ,

\lim_{n\to\infty}\ \sum_{k=10^{n-2}}^{10^{n-1}-1}\log_{10}\!\left(1+\frac{1}{10k+d}\right) = \frac1{10}.

By the previous milestone, the left side is the Benford probability that $d$ is the $n$ -th significant digit; so the distribution of the $n$ -th digit approaches the uniform distribution on $\{0,\dots,9\}$ .

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem nth_digit_prob_tendsto_uniform (d : ℕ) (hd : d ≤ 9) :
    Filter.Tendsto
      (fun n : ℕ => ∑ k ∈ Finset.Ico (10 ^ (n - 2) : ℕ) (10 ^ (n - 1)),
        Real.logb 10 (1 + 1 / (10 * (k : ℝ) + d)))
      Filter.atTop (nhds (1 / 10)) := 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" ("The distribution of the n-th digit, as n increases, rapidly approaches a uniform distribution with 10% for each of the ten digits").

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 $d\le9$ : as $n\to\infty$ (naturals), $\sum_{k} \log_{10}\big(1 + 1/(10k+d)\big) \to 1/10$ , the sum over naturals $k$ with $10^{n-2}\le k<10^{n-1}$ (truncated natural subtraction in the exponents; for $n\le1$ both bounds equal $1$ and the sum is empty, which does not affect the limit).

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

The nnn-th digit becomes uniform as n→∞n\to\inftyn→∞

The $n$ -th digit becomes uniform as $n\to\infty$