Powers $k^n$ satisfy Benford's law when $\log_{10}k$ is irrational

Proved

BenfordLaw.pow_isBenfordSeq_of_irrational_logb

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

benford-lawequidistributionleading-digits

Let $k$ be a natural number such that $\log_{10}k$ is irrational (equivalently, $k\ge1$ is not a power of $10$ ). Then the sequence $k^1,k^2,k^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}(k^n)=d\}}{N}=\log_{10}\!\left(1+\frac1d\right).

This is the goal theorem of the mission; the powers of $2$ are the case $k=2$ .

Formalization Note. Encoded as IsBenfordSeq 10 (fun n => (k : ℝ) ^ (n + 1)). The case $k=0$ is excluded automatically because $\log_{10}0 = 0$ in Lean, which is rational.

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem pow_isBenfordSeq_of_irrational_logb (k : ℕ) (hk : Irrational (Real.logb 10 k)) :
    IsBenfordSeq 10 (fun n => (k : ℝ) ^ (n + 1)) := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Distributions known to obey Benford's law", Note 3 ("the sequence k1, k2, k3, etc., satisfies Benford's law exactly, under the condition that log10 k is an irrational number").

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 $k$ such that the real number $\log_{10}k = \ln k/\ln 10$ is irrational (this excludes $k=0$ , since Lean sets $\ln 0 = 0$ , and $k = 10^j$ ): $\mathrm{IsBenfordSeq}(10,a)$ for $a_n = k^{n+1}$ ( $n=0,1,\dots$ ). Unfolded: for every natural $1\le d<10$ , the proportion of $n\in\{0,\dots,N-1\}$ with $\lfloor 10^{\{\log_{10} k^{n+1}\}}\rfloor = d$ tends to $\log_{10}(1+1/d)$ as $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

Powers knk^nkn satisfy Benford's law when log⁡10k\log_{10}klog10​k is irrational

Powers $k^n$ satisfy Benford's law when $\log_{10}k$ is irrational