Conway's refinement conjecture (Conway 1976) asserts that every equality 
of omnific integers
admits a multiplicative refinement. More precisely, there should exist omnific
integers 
, 
, 
, and 
such that 
, 
, 
,
and 
.
The four factors can be viewed as the entries of a two-by-two array whose row products are 
and 
and whose column products are 
and 
.
The analogous statement for ordinary integers follows
from greatest common divisors. Omnific
integers form a much larger ordered ring inside
the surreal numbers, so this integer
argument does not automatically extend.
Abramov (2026) reported a proof developed through interactive work with ChatGPT and Claude. VibeMathed (2026) rebuilt the complete Lean formalization using only standard logical axioms. As of Sep. 7, 2026, independent specialist review of the formal definitions and their agreement with Conway's intended statement had not been reported.
