Conway's Refinement Conjecture for Omnific Integers

What the AI did

Dan Abramov describes the project as an AI-proof experiment. Claude first selected Conway's refinement conjecture as a promising open problem after noting recent progress by L'Innocente and Mantova. Over roughly a month, Abramov repeatedly used ChatGPT and Claude to generate mathematical ideas and then steered the systems into producing Lean proofs, using compilation and formal checking to reject invalid directions. The repository therefore attributes the mathematical proof search and much of the formal proof construction to interactive AI exploration under human steering.

VerificationAI

Site-confirmed: rebuilt here on 4 September 2026, not taken from the repository's CI. This site's verify-lean workflow checked out gaearon/conway-refinement at commit 264445c9, the commit the entry cites, installed the toolchain it pins (leanprover/lean4:v4.31.0) with its CombinatorialGames dependency, ran $\texttt{lake build}$ over every module (3145 jobs), then the project's own scripts/Axioms.lean, then $\texttt{lake env leanchecker}$ replaying the whole ConwayRefinement environment. 37 minutes, every step green.

Both formulations of the conjecture - the one over the CombinatorialGames $\texttt{Surreal}$ type and the Mathlib-only one with the surreal definitions inlined - report $\texttt{propext}$, $\texttt{Classical.choice}$ and $\texttt{Quot.sound}$ and nothing else. No $\texttt{sorryAx}$, no project axiom.

Still Candidate rather than Resolved, and the reason is the one the author gives himself: a kernel checks the proof against the statement as written, and whether that statement is Conway's conjecture is a reading a surreal-number specialist has to do. The definition used is Conway's own cut $x = \{x - 1 \mid x + 1\}$ and the statement is a few lines, so it is an afternoon's work for the right reader. Nobody without a stake has done it yet.

Sources

• Lean proofProof of that statement
• Lean statementCombinatorialGames statement of the conjecture · Mathlib-only statement, no CombinatorialGames dependency
• Palomar listingPalomar provenance and the comparator statement
• CodeGithub
• Independent workRebuilt here: lake build, axiom audit and leanchecker replay