Reciprocals and square roots of the naturals are not Benford

Proved

BenfordLaw.not_isBenfordSeq_inv_sqrt

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

benford-lawequidistributionleading-digits

Neither the reciprocals $1/1, 1/2, 1/3,\dots$ nor the square roots $\sqrt1,\sqrt2,\sqrt3,\dots$ of the successive natural numbers satisfy Benford's law in base $10$ : for each of the two sequences there is a digit $d \in\{1,\dots,9\}$ for which the relative frequency of leading digit $d$ among the first $N$ terms does not converge to $\log_{10}(1+1/d)$ .

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem not_isBenfordSeq_inv_sqrt :
    ¬ IsBenfordSeq 10 (fun n => 1 / ((n : ℝ) + 1)) ∧
      ¬ IsBenfordSeq 10 (fun n => Real.sqrt ((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 disobey Benford's law" ("The square roots and reciprocals of successive natural numbers do not obey this law", ref. Raimi 1976).

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.

Both of the following hold: (i) it is not the case that $\mathrm{IsBenfordSeq}(10, a)$ for $a_n = 1/(n+1)$ ; (ii) it is not the case that $\mathrm{IsBenfordSeq}(10, a)$ for $a_n = \sqrt{n+1}$ ( $n = 0,1,\dots$ , real arithmetic). Unfolded, each says: there exists a natural $1\le d<10$ such that the proportion of $n\in\{0,\dots,N-1\}$ with $\lfloor 10^{\{\log_{10}a_n\}}\rfloor = d$ does not tend to $\log_{10}(1+1/d)$ (it may converge to something else or not converge at all).

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