Prove2Me

The Fibonacci numbers satisfy Benford's law

Proved
BenfordLaw.fib_isBenfordSeq

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

benford-lawequidistributionleading-digits

Let F1=F2=1F_1 = F_2 = 1, Fn+2=Fn+1+FnF_{n+2} = F_{n+1} + F_n be the Fibonacci numbers. The sequence F1,F2,F3,…F_1, F_2, F_3, \dots satisfies Benford's law in base 1010: for every d∈{1,…,9}d\in\{1,\dots,9\},

lim⁡N→∞#{1≤n≤N:D10(Fn)=d}N=log⁡10 ⁣(1+1d).\lim_{N\to\infty}\frac{\#\{1\le n\le N : D_{10}(F_n)=d\}}{N}=\log_{10}\!\left(1+\frac1d\right).

Formalization Note. Encoded as IsBenfordSeq 10 (fun n => (Nat.fib (n + 1) : ℝ)); Mathlib's Nat.fib has fib 0 = 0, fib 1 = 1.

Preamble
import Mathlib
import Definitions.Def_BenfordLaw_Defs
Formal statement
namespace BenfordLaw

theorem fib_isBenfordSeq :
    IsBenfordSeq 10 (fun n => (Nat.fib (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" (refs. Washington 1981, https://doi.org/10.1080/00150517.1981.12430109; Duncan 1967, https://doi.org/10.1080/00150517.1967.12431312).
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.

IsBenfordSeq(10,a)\mathrm{IsBenfordSeq}(10,a) with an=fib(n+1)a_n = \mathrm{fib}(n+1) cast to R\mathbb R, where fib(0)=0\mathrm{fib}(0)=0, fib(1)=1\mathrm{fib}(1)=1, fib(m+2)=fib(m+1)+fib(m)\mathrm{fib}(m+2)=\mathrm{fib}(m+1)+\mathrm{fib}(m); so a=(1,1,2,3,5,8,… )a = (1,1,2,3,5,8,\dots). Unfolded: for every natural 1≤d<101\le d<10, the proportion of n∈{0,…,N−1}n\in\{0,\dots,N-1\} with ⌊10{log⁡10an}⌋=d\lfloor 10^{\{\log_{10} a_n\}}\rfloor = d tends to log⁡10(1+1/d)\log_{10}(1+1/d).

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