Conway’s refinement property for omnific integers
Follow the latest progress by email.
For Conway’s cut-defined omnific integers, does ab=cd always admit refinement a=ef, b=gh, c=eg, d=fh with omnific e,f,g,h, including zero cases?
Why it matters and what counts as progress
Why it matters: It asks for a multiplicative factorization property in the surreal-integer setting. Formal encodings must match the intended objects rather than merely reuse their name.
What counts as progress: Prove multiplicative refinement for Conway’s omnific integers including zero cases; a formal proof must retain the intended cut-defined objects.
How the problem developed
- 1976 · Conjecture [1]
John H. Conway Stated the refinement conjecture for omnific integers in On Numbers and Games.
- 2000 · Partial result [2]
Alessandro Berarducci Developed factorization theory for generalized power series, a foundation later work used to study omnific integers.
- 2024 · Partial result [2]
Sonia L’Innocente and Vincenzo Mantova Advanced factorization theory for generalized power series and omnific integers, supplying recent background to the refinement question.
Dan Abramov and AI assistants A public Lean repository reports a proof of Conway’s four-factor refinement statement, while its author says the work is not yet completed mathematical work.
AI contribution
AI-built Lean proof reports Conway’s omnific refinement property
For cut-defined omnific integers a,b,c,d represented as numeric games, a Lean theorem says ab=cd implies omnific e,f,g,h with a=ef, b=gh, c=eg and d=fh, including zero cases. The theorem is stated at each Lean universe, rather than putting all surreal numbers into one type.
Sources
Website timeline
Publication dates and editorial changes.
AI-built Lean proof reports Conway’s omnific refinement property