AI-Assisted Proof of Conway's Surreal Numbers Conjecture
How an amateur leveraged multiple AI models to tackle a 50-year-old math problem
1The ambitious challenge
The author, a self-described math novice, set out to test whether frontier AI models could solve an open mathematical problem. They chose Conway's refinement conjecture about surreal numbers - a 50-year-old unsolved problem in a niche area of mathematics. Surreal numbers, invented by John Conway, form a rich number system containing all real numbers, ordinals, and more, constructed through a simple recursive rule of filling gaps between existing numbers.
2Selecting the problem
After consulting Claude AI about open problems in surreal number theory, the author settled on Conway's refinement conjecture regarding omnific integers. This conjecture suggests that factorizations of these generalized integers (which include infinite numbers like ω) maintain a refinement property similar to ordinary integers. The choice was partly sentimental - 2026 marks the 50th anniversary of Conway's book on the subject.
3Initial AI approaches
Early attempts involved direct problem-solving with Claude, feeding it mathematical papers and asking for counterexamples. These sessions produced grandiose but incoherent output filled with invented terminology. The author describes these as reading like 'bad science fiction' - dramatic claims without concrete justification that couldn't be verified by human mathematicians.
4Switching to skeptical AI
Frustrated with Claude's output, the author switched to ChatGPT (particularly 'Sol') which took a more skeptical approach. This AI would critically analyze Claude's output, pointing out flaws in terminology and reasoning. While still unable to judge mathematical validity, the author found ChatGPT's restrained personality more productive for generating small, verifiable claims that built on existing literature.
5Multi-agent workflow
The project evolved into a complex system using locally-run Codex with specialized agents: some generating proofs, others checking them, and a 'cafeteria' agent facilitating communication. This allowed parallel exploration where agents could build on each other's verified results. The author managed this system without understanding the math, making decisions based on workflow patterns rather than content.
6Breakthrough moment
An unexpected insight came when reversing agent roles - having the 'red team' proof-breaker attempt creative construction. This led to productive riffing between agents, though the initial discovery was later lost and had to be rediscovered. The workflow ultimately produced a substantial TeX document and Lean formalization, though it didn't fully prove the conjecture.
7Technical challenges
The process revealed limitations in current AI systems. Claude struggled with consistency, often certifying then later finding flaws in its own work. Maintaining productive workflows required constant monitoring to prevent drift into unproductive patterns. The author developed strategies like session resetting when agents became stuck in loops of finding and fixing errors.
8Lean formalization
A crucial step was formalizing the problem in Lean, a proof assistant. This provided a way to mechanically verify aspects of the proof. The author notes that without this formalization, there would be no way to convince mathematicians to examine the work. The proof passed initial checks by the Palomar registry and received tentative validation from Lean experts.
9Surreal number construction
The proof relies heavily on properties of surreal numbers, built through Conway's recursive gap-filling rule. Starting from nothing, each step creates numbers in all gaps between existing numbers. This process, continued through transfinite steps, generates all real numbers, ordinals, and more exotic numbers like ω (infinity) and ε (infinitesimal).
10Omnific integers
The conjecture specifically concerns omnific integers - the 'integer part' of surreal numbers. These include ordinary integers but also infinite numbers like ω and combinations like ω/2. The refinement property suggests these numbers maintain factorization properties similar to ordinary integers, despite their infinite nature - a non-obvious claim Conway believed might hold.
11AI limitations revealed
The project highlighted how different AI models excel at different aspects of mathematical work. Claude showed creativity but lacked rigor, ChatGPT provided more verifiable small steps, while Codex enabled complex workflows. None could independently solve the problem, suggesting current AI's limitations in deep mathematical reasoning without human guidance.
12Future implications
While the proof remains unverified by mathematicians, the project demonstrates how AI can assist in mathematical discovery. The multi-agent approach, combining different models' strengths while mitigating weaknesses, suggests a template for future AI-assisted research. It also raises questions about credit and verification in AI-generated mathematics.