Prove2Me

Mean 3.4403.440 and variance 6.0576.057 of the Benford first digit

Proved
BenfordLaw.benford_mean_variance

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

benford-lawequidistributionleading-digits

Let DD be a digit-valued random variable with the Benford distribution P(D=d)=log⁡10(1+1/d)\mathbb P(D=d) = \log_{10}(1+1/d), d=1,…,9d=1,\dots,9. Then, to three decimal places,

E[D]=∑d=19d log⁡10 ⁣(1+1d)≈3.440,Var⁡(D)=∑d=19d2log⁡10 ⁣(1+1d)−E[D]2≈6.057.\mathbb E[D] = \sum_{d=1}^9 d\,\log_{10}\!\left(1+\tfrac1d\right) \approx 3.440,\qquad \operatorname{Var}(D)=\sum_{d=1}^9 d^2\log_{10}\!\left(1+\tfrac1d\right)-\mathbb E[D]^2\approx 6.057.

Precisely: ∣E[D]−3.440∣<0.0005|\mathbb E[D]-3.440|<0.0005 and ∣Var⁡(D)−6.057∣<0.0005|\operatorname{Var}(D)-6.057|<0.0005.

Preamble
import Mathlib
import Definitions.Def_BenfordLaw_Defs
Formal statement
namespace BenfordLaw

theorem benford_mean_variance :
    |(∑ d ∈ Finset.Icc (1 : ℕ) 9, (d : ℝ) * benfordProb 10 d) - 3.440| < 0.0005 ∧
      |((∑ d ∈ Finset.Icc (1 : ℕ) 9, (d : ℝ) ^ 2 * benfordProb 10 d) -
          (∑ d ∈ Finset.Icc (1 : ℕ) 9, (d : ℝ) * benfordProb 10 d) ^ 2) - 6.057| < 0.0005 := by sorry

end BenfordLaw
Source
Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Moments" (mean 3.440, variance 6.057).
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.

With pd=log⁡10(1+1/d)p_d = \log_{10}(1+1/d) and sums over naturals d=1,…,9d=1,\dots,9 cast to reals, both of the following hold:

∣∑d=19d pd−3.440∣<0.0005and∣(∑d=19d2pd)−(∑d=19d pd)2−6.057∣<0.0005.\Big|\sum_{d=1}^9 d\,p_d - 3.440\Big| < 0.0005 \quad\text{and}\quad \Big|\Big(\sum_{d=1}^9 d^2 p_d\Big) - \Big(\sum_{d=1}^9 d\,p_d\Big)^2 - 6.057\Big| < 0.0005 .

The numbers 3.4403.440, 6.0576.057, 0.00050.0005 are exact real decimals.

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