Conway's Refinement Conjecture for Omnific Integers
candidateconfidence 50%
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
If $a,b,c,d\in\mathbf{Oz}$ are omnific integers and
$$
ab=cd,
$$
then there exist omnific integers $e,f,g,h\in\mathbf{Oz}$ such that
$$
a=ef,\qquad b=gh,\qquad c=eg,\qquad d=fh.
$$
Equivalently, every equality of two products in the omnific integers admits a common four-factor refinement.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
ChatGPT; Claude
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.
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.
The repository gives a Lean proof of Conway's 1976 refinement conjecture for omnific integers: whenever
$$
ab=cd
$$
with $a,b,c,d\in\mathbf{Oz}$, there exist $e,f,g,h\in\mathbf{Oz}$ satisfying
$$
a=ef,\quad b=gh,\quad c=eg,\quad d=fh.
$$
The proof is formalized twice: once using CombinatorialGames' surreal-number implementation and once with the required surreal definitions inlined over Mathlib. The development also proves stronger structural results about factorization in Hahn-series integer parts and related generalized power-series rings.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
The source status is candidate and must not be represented as solved.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.