In base $2$ every nonzero number has leading digit $1$

Proved

BenfordLaw.leadingDigit_two_eq_one

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

benford-lawequidistributionleading-digits

For every real number $x \neq 0$ , the leading binary digit of $x$ is $1$ :

D_2(x) = 1.

Consequently Benford's law in base $2$ is true but trivial: $P_2(1) = \log_2 2 = 1$ .

Formalization Note. Negative $x$ are read through $|x|$ (Lean's Real.logb convention).

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem leadingDigit_two_eq_one (x : ℝ) (hx : x ≠ 0) :
    leadingDigit 2 x = 1 := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "In other bases" ("For b = 2, 1 ... All binary and unary numbers (except for 0 or the empty set) start with the digit 1").

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 real $x$ with $x \neq 0$ : $\lfloor 2^{\{\log_2 x\}}\rfloor = 1$ , where $\log_2 x = \ln|x|/\ln 2$ and the floor is taken into $\mathbb N$ . (The hypothesis $x \neq 0$ is not needed for the value — $\mathrm{leadingDigit}(2,0)=1$ by the junk convention — but it is part of the statement.)

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

In base 222 every nonzero number has leading digit 111

In base $2$ every nonzero number has leading digit $1$