The powers of $2$ satisfy Benford's law

Proved

BenfordLaw.pow_two_isBenfordSeq

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

benford-lawequidistributionleading-digits

The sequence of powers of two, $2^1, 2^2, 2^3, \dots$ , satisfies Benford's law in base $10$ : for every $d \in \{1,\dots,9\}$ ,

\lim_{N\to\infty}\frac{\#\{1 \le n \le N : D_{10}(2^n) = d\}}{N} = \log_{10}\!\left(1+\frac1d\right).

This is the special case $k=2$ of the mission goal, listed separately in the source.

Formalization Note. Encoded as IsBenfordSeq 10 (fun n => (2 : ℝ) ^ (n + 1)), with $n$ starting at $0$ .

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem pow_two_isBenfordSeq :
    IsBenfordSeq 10 (fun n => (2 : ℝ) ^ (n + 1)) := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, sections "Examples" and "Distributions known to obey Benford's law" ("the powers of 2", ref. Raimi 1976, https://doi.org/10.2307/2319349).

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.

$\mathrm{IsBenfordSeq}(10, a)$ for $a_n = 2^{n+1}$ ( $n = 0,1,2,\dots$ , real powers of the real number $2$ ). Unfolded: for every natural $d$ with $1\le d<10$ ,

\frac{\#\{n \in\{0,\dots,N-1\} : \lfloor 10^{\{\log_{10} 2^{n+1}\}}\rfloor = d\}}{N} \longrightarrow \log_{10}(1+1/d) \quad (N\to\infty).

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 powers of 222 satisfy Benford's law

The powers of $2$ satisfy Benford's law