The Copeland-Erdős constant is not strongly normal in base 10

The Copeland-Erdős constant $0.235711131719\ldots$ concatenates the primes in increasing order; Copeland and Erdős proved in 1946 that it is normal in base 10. Strong normality, introduced by Belshaw and Borwein, also prescribes the size of the digit-count fluctuations: $x$ is simply strongly normal in base $b$ if for every digit the discrepancy $Z_d(x;N) - N/b$ has $\limsup$ and $\liminf$ equal to $\pm\sqrt{b-1}/b$ on the scale $\sqrt{2N\log\log N}$ , and strongly normal if this holds in every base $b^k$ . Champernowne's number is normal but not strongly normal. Does the Copeland-Erdős concatenation of the primes also fail to be strongly normal in base 10?

Result: Proved(see note)
Status: Resolved
AI contribution: AI-discovered
Method: Argument
Field: Normal numbers; digit expansions
Posed by: Adrian Belshaw, On the Normality of Numbers, SFU M.Sc. thesis (2005), section 4.7; restated by Catt, Coons and Velich, Integers 16 (2016), section 3
Year posed: 2005
Years open: 21y
Solved: 2026-09-13
Model: ChatGPT-6 Astra
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Preprint
Significance: 25 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

No: the Copeland-Erdős constant is not simply strongly normal in base 10, hence not strongly normal in base 10, and the failure is already visible in the digit 0. The proof compares the zero count at two positions in the expansion. Every prime in [10^(6n), 10^(6n) + 10^(5n)) begins with 1 followed by n zeros, and Ingham's 1937 short-interval theorem with exponent 5/6 supplies about 10^(5n)/(6n log 10) such primes, so the zero excess across that stretch is of order 10^(5n), while simple strong normality would cap the discrepancy at O(sqrt(N log log N)) with N of order 10^(6n), that is at order 10^(3n). Belshaw and Borwein's 2013 Champernowne argument is the model; Ingham replaces the trivial prime count. Strong normality in other bases is not addressed.

What the AI did

The AI chose the question, proved it and then wrote the proof in Lean.

Verification

Checked here on 22 September 2026. The repository at HEAD (pushed 14 September) has 16 Lean files, 1,879 lines, no sorry, no axiom declaration, no native_decide. GitHub Actions run 34797497727 built it on a fresh runner with the pinned Lean 4.34.0-rc2 and mathlib de2ef68, and printed both final theorems, copelandErdos_not_simply_strong_normal_of_ingham and copelandErdos_not_strong_normal_of_ingham, with axioms propext, Classical.choice and Quot.sound. The statement was audited: copelandErdosReal is Real.ofDigits of the increasing prime concatenation and its canonical decimal digits are proved; SimplyStrongNormal is the Belshaw-Borwein law-of-the-iterated-logarithm condition with the constant sqrt(b-1)/b for every digit; StrongNormal quantifies over every positive power of the base. The one external input, Ingham's 1937 theorem specialised to intervals of length x^(5/6), enters as an explicit theorem hypothesis (Ingham1937Input), not as an axiom, with its specialisation to x = 10^(6n) and the endpoint bookkeeping proved in Lean. Lean-checked rather than Lean-verified for that reason, as the Erdős-Borwein 2-density entry was for AGP. The three-page argument was read and is correct.

Sources

Submitted by nufrogcaca on 15 Sep 2026

The Copeland-Erdős constant is not strongly normal in base 10

What was actually shown

What the AI did

Verification

Sources

Discussion