Leading digits of Zipf ( $s=1$ ) data follow Benford's law

Proved

ZipfLaw.zipf_one_leadingDigit_benford

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

harmonic-numberspower-lawzipf-law

Let $K_N$ be a random rank drawn from the Zipf distribution with $s=1$ on $\{1,\dots,N\}$ , $\mathbb P(K_N=k)=\frac{1}{H_N\,k}$ . For every digit $d\in\{1,\dots,9\}$ , the probability that the leading decimal digit of $K_N$ equals $d$ tends to the Benford probability:

\lim_{N\to\infty}\sum_{\substack{1\le k\le N\\ D_{10}(k)=d}}\frac{1}{H_N\,k}=\log_{10}\!\left(1+\frac1d\right).

Formalization Note. The source's sentence does not say which numbers' leading digits are meant; this item reads it as the leading digits of the ranks $k$ when $k$ occurs with Zipf ( $s=1$ ) frequency $\propto 1/k$ . (The other reading, the leading digits of the values $C/k$ for $k = 1, \dots, N$ counted once each, is the reciprocal sequence, which does not satisfy Benford's law.)

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem zipf_one_leadingDigit_benford (d : ℕ) (hd1 : 1 ≤ d) (hd9 : d ≤ 9) :
    Filter.Tendsto
      (fun N : ℕ => ∑ k ∈ (Finset.Icc 1 N).filter (fun k => leadingDigit k = d), zipfPMF N 1 k)
      Filter.atTop (nhds (Real.logb 10 (1 + 1 / (d : ℝ)))) := by sorry

end ZipfLaw

Source

Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, section "Related laws" ("The leading digits of data satisfying Zipf's law with s = 1, satisfy 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.

For every natural $d$ with $1\le d\le9$ : as $N\to\infty$ (naturals),

\sum_{\substack{k\in\{1,\dots,N\}\\ \mathrm{leadingDigit}(k)=d}}\mathrm{zipfPMF}(N,1,k)\longrightarrow\log_{10}(1+1/d),

where $\mathrm{leadingDigit}(k)=k\operatorname{div}10^{\lfloor\log_{10}k\rfloor}$ (natural numbers) and $\mathrm{zipfPMF}(N,1,k)=1/(k\,H_N)$ for $1\le k\le 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

Leading digits of Zipf (s=1s=1s=1) data follow Benford's law

Leading digits of Zipf ( $s=1$ ) data follow Benford's law