How I Vibed a Proof of Conway’s Refinement Conjecture with AI and Lean

TL;DR

I built a multi‑agent AI laboratory that, after months of prompting, token‑heavy experimentation, and Lean formalization, generated a mechanically checked proof of Conway’s refinement conjecture for omnific integers; the proof has passed the Palomar registry and informal expert review, but it has not yet been independently verified.

What Conway’s Refinement Conjecture Says

Conway’s conjecture (1976) concerns omnific integers, the integer part of the surreal number tree. It asserts a refinement property: if (ab = cd) for omnific integers (a,b,c,d), then there exist omnific integers (e,f,g,h) such that

[ a = ef,\quad b = gh,\quad c = eg,\quad d = fh. ]

In ordinary integers this is trivial (e.g. (210 = 10\cdot21 = 6\cdot35) refines to (2\cdot5\cdot3\cdot7)). The conjecture asks whether the same factor‑reshuffling holds for the far richer omnific integers, which include infinite and infinitesimal values like (\omega), (2\omega), (\omega^\omega), and even "whole" infinitesimals such as (-\omega/7).

Overview of the AI‑Driven Workflow

The project proceeded in five weekly phases, each refining the agents, their roles, and the interaction with Lean.

1. First Week – Naïve One‑Shot Attempts

Prompted Claude to "do a breakthrough" on the conjecture.
Claude produced long, jargon‑filled prose that was incoherent and unverifiable.
Switching to ChatGPT’s “skeptical” persona yielded short, plausible lemmas but still no coherent proof.

2. Second Week – Multi‑Agent Laboratory

Downloaded Codex locally for deterministic token usage.
Spawned agents with explicit roles: PM (project manager), Math (idea generators), Red (adversarial reviewer), Random (exploratory), and Lean (formalizer).
Agents communicated via a shared “cafeteria” channel; the PM coordinated merges.
The workflow produced a large TeX corpus but no verified new results.

3. Third Week – Dead Ends and Token Exhaustion

Re‑entered Claude for Lean formalization; the model oscillated between certifying and later refuting its own claims.
The TeX stack grew to ~30 “papers”; any single mistake threatened the entire tower.
A promising‑looking global proof appeared, but a fresh audit exposed a circular dependency, confirming that no proof existed yet.

4. Fourth Week – Grounding in Reality

Shifted focus to verifying concrete errors in a peer‑reviewed reference (L’Innocente–Mantova 2024). Confirmed several typos with the authors, establishing trust in the model’s ability to spot real issues.
Burned the entire prior corpus and asked ChatGPT to salvage anything mathematically sound.
Discovered a finite‑degree primality result in the literature that, after verification, turned out to be a novel theorem.

5. Fifth Week – Consolidation and Final Proof

Built a second, isolated Lean agent to certify the novel result while a first Lean agent handled only established literature.
Introduced strict standalone folders (no internal imports) and automated audits for extra axioms, module layering, and proof size.
Generated proof‑maps (Mermaid diagrams) to visualize dependencies, enabling the model to prune unnecessary branches.
After several iterations of “have fun” prompts, the agents produced a standalone Lean certificate of the full refinement conjecture, compiled without extra axioms.

Key Technical Artifacts

Artifact	Description
GitHub repo – `gaearon/conway-refinement`	Contains the Lean source, TeX drafts, and tooling scripts.
Palomar registry entry – `PALOMAR‑2026‑09‑03‑000002`	Mechanical verification that the Lean kernel accepted the proof.
Standalone folder	Files that import only Mathlib, ensuring human‑readable statements under 500 lines each.
Proof map website – `gaearon.github.io/conway-refinement`	Interactive Mermaid diagram of the dependency tree for the proof.
Custom tooling – `subverso` attribute annotator, module‑system linter, and Lean Comparator integration	Enforces clean module layering and prevents hidden axioms.

Lessons Learned (Answer‑First)

AI can produce a mechanically verified proof of a deep open problem without the author understanding the mathematics, but the workflow requires strict engineering guardrails, adversarial auditing, and frequent “burn‑and‑rebuild” cycles.
ChatGPT proved more useful than Claude for exploratory mathematics, while Claude excelled at deterministic Lean code generation when given a concrete goal.
Separate Lean pipelines for trusted literature and speculative results prevent contamination and make audits tractable.
Human verification of low‑level errors (e.g., typos in source papers) builds confidence in the model’s output and provides a foothold for collaboration.
Proof‑map visualizations and strict module isolation dramatically improve model interpretability, allowing the agents to prune “bullshit” branches.
Token cost is enormous – roughly 40 billion tokens (≈ $40 k) for the entire run; better steering could reduce this by a factor of 5–10.

Representative Community Feedback

“The process feels like a performance‑art project where the author never really learns the math, but the models do the heavy lifting.” – m‑steffen, HN comment

“ChatGPT’s skeptical persona was far more productive than Claude’s grandiose one‑shot attempts.” – nphardon, HN comment

“The proof‑map and Mermaid diagrams helped the model see the proof shape and suggested simplifications.” – author’s own observation

Open Issues and Next Steps

Independent mathematical review – The proof has not yet been examined by experts in surreal numbers; community verification is essential.
Simplification – Current Lean code contains many auxiliary lemmas; a shorter, more conceptual proof would aid acceptance.
Generalization – The workflow could be applied to other open problems; a template repository is being prepared.
Cost reduction – Developing better prompting strategies and token‑efficient agents will make large‑scale AI‑driven mathematics more accessible.

Final Takeaway

By orchestrating multiple LLM agents, enforcing rigorous Lean formalization, and repeatedly pruning away hallucinated mathematics, I managed to produce a mechanically checked proof of Conway’s refinement conjecture. The result demonstrates that AI‑augmented theorem proving is feasible even for problems far beyond the author’s expertise, but it also highlights the necessity of disciplined engineering, adversarial auditing, and human collaboration to ensure correctness and credibility.