Source authenticated

Conway's Refinement Conjecture for Omnific Integers

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.

Exact FrontierDelta

Prior state unknown→proved

Scope and record

Occurred: Sep 3, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: site-confirmed. Publication: announcement. AI contribution: ai-co-developed. VibeMathed editorial classifications, scores, notes, relations, and dataset structure are CC BY 4.0. Source statements and linked content retain their own rights.

Canonical aliases: Conway's Refinement Conjecture for Omnific Integers · Conway's Refinement Conjecture

Confidence: Not scored

Registry verification: site confirmed · announcement · candidate

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

ChatGPT
model · ai model contributor · OpenAI

Claude
model · ai model contributor · Anthropic

Dan Abramov
human · human collaborator

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Conway's Refinement Conjecture for Omnific Integers

specialist registry · passed

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.