A Stoneham number is a number 
of the form
 |
where 
are relatively prime positive
integers. Allowing 
and 
not to be relatively prime gives the generalized
Stoneham numbers. Stoneham (1973) proved that 
is 
-normal whenever 
is an odd prime and 
is a primitive root of 
. Bailey and Crandall (2002) showed
that 
is normal whenever 
and 
are relatively prime.
A project using ChatGPT-6 Astra reported the more general criterion that 
is 
-normal if and only if some
prime divisor of 
does not divide 
(VibeMathed 2026a). If every prime
divisor of 
divides 
,
the digit 0 instead has limiting frequency 1. In particular,
is not normal
in base 6 even though neither 6 nor 4 divides the other.
ChatGPT-6 Astra reportedly selected Bailey and Crandall's question, found the counterexample and criterion, and wrote the Lean
formalization. As of Sep. 15, 2026, the Lean sources had passed the project's
continuous integration, but independent specialist review and a definitive priority
check had not been reported.
Bailey and Borwein (2012) asked whether the sum of two Stoneham numbers with the same base must be normal
in that base. A project using ChatGPT-6 Astra reported that
if 
and 
is relatively prime to both 
and 
, then 
is 
-normal (VibeMathed 2026b).
ChatGPT-6 Astra reportedly selected the problem, proved the result, and produced
its Lean formalization. As of Sep. 13, 2026, the Lean sources had passed the
project's continuous integration and guarded checks, and VibeMathed had compared
the statement with Bailey and Borwein's question. The Lean build had not been independently
repeated, and independent specialist review of the proof had not been reported.
-Normality in the Rational
Fractions with Applications to Normal Numbers." Acta Arith. 22,
277-286, 1973.VibeMathed. "Bailey-Crandall's Mutual-Nondivisibility
Question for Stoneham Numbers." Sep. 12, 2026a.