The Copeland-Erdős constant is the constant with decimal expansion 0.23571113171923... (OEIS A033308) obtained by concatenating consecutive primes: 2, 23, 235, 2357, 235711, ... (OEIS A019518). It is one of the Smarandache sequences and is considered as an infinite word by Allouche and Shallit (2003, pp. 299 and 334).
It is therefore given by the formula
Copeland and Erdős (1946) showed that it is a normal number in base 10.
A simply strongly normal number in base
has the law of the iterated logarithm
fluctuations expected for the number of occurrences of each individual base-
digit. CaptainSude (2026) reported that the Copeland-Erdős
constant is not simply strongly normal in base 10, and hence is not strongly
normal, because the digit 0 violates the required fluctuation
bound. The argument uses Ingham's theorem (Ingham 1937) on gaps
between consecutive primes. The remaining argument
was formalized in Lean conditional on that theorem. CaptainSude (2026) credits GPT-6
Astra with selecting the question, finding the proof, and writing the formalization.
As of Sep. 22, 2026, the Lean development had passed the project's checks, but
independent specialist review had not been reported.
Interestingly, while the Champernowne constant continued fraction contains sporadic very large terms, making the continued fraction difficult to calculate, the Copeland-Erdős constant continued fraction is well-behaved and does not show the "large term" phenomenon.