How I Vibed a Proof of Conway’s Refinement Conjecture

Quick Takeaway

Dan Abramov used Claude, ChatGPT, and Codex agents to generate, audit, and Lean‑formalize a proof of Conway’s refinement conjecture for omnific integers; the proof passes mechanical checks but has not yet been independently validated.

What Conway’s Conjecture Says

Conway’s refinement conjecture asserts that for any equality of products of omnific integers (a b = c d), there exist integers (e,f,g,h) such that:

(a = e f)
(b = g h)
(c = e g)
(d = f h)

In other words, any two factorizations of an omnific integer admit a common refinement, mirroring the elementary integer property that a product can be broken into prime factors and recombined.

The AI‑Driven Research Pipeline

1. Problem Selection

Claude was prompted to pick an open problem in surreal numbers. It chose the refinement conjecture, citing recent work by L’Innocente and Mantova that reduced the conjecture to a statement about irreducibles in (K((\mathbb{R}^{\le 0}))).
The author noted that Claude’s reduction was incomplete, but the problem remained attractive because of its sentimental link to the 50th anniversary of ONAG.

2. Early One‑Shot Attempts

Initial prompts asked Claude to “do a breakthrough.” The model produced incoherent, jargon‑heavy prose that could not be verified.
Switching to ChatGPT (referred to as Sol) yielded more modest claims, but still required extensive human vetting.

3. Multi‑Agent Laboratory (Codex)

A project‑manager (PM) agent coordinated the workflow.
Two Math agents generated candidate lemmas.
A Red agent attempted to find flaws.
A Random agent explored tangential ideas.
A Lean agent translated promising results into Lean code.
Agents communicated via a “cafeteria” chatroom, enabling cross‑pollination while preserving role boundaries.

4. Token Consumption & Cost

Roughly 40 billion tokens were processed, of which ~210 million were output.
Estimated API cost: ≈ $40 000.

Key Milestones

Week	Milestone	Outcome
1	Problem framing & initial prompting	Claude produced a vague problem statement; ChatGPT supplied a critical “skeptical” voice.
2	Laboratory setup with Codex agents	Generated dozens of draft “papers”; many contained invented terminology and logical gaps.
3	First dead‑end & failed “bootstrap” proof	ChatGPT claimed a full proof, but a fresh session exposed a circular argument.
4	Ground‑truthing via typo‑fixes	Model‑found errors in a peer‑reviewed reference were confirmed by authors, boosting confidence.
5	Burn‑and‑salvage strategy	Discarded most noisy drafts, retained a coherent result on finite‑degree primality in Hahn series.
6	Formal verification	Two separate Lean agents certified the finite‑degree result and later the full refinement conjecture.
7	Proof‑map tooling	Custom scripts generated Mermaid diagrams and an interactive web UI to visualize dependency structure.

The Final Lean Proof

The proof resides in the GitHub repository gaearon/conway‑refinement under ConwayRefinement/Standalone.
Each standalone file imports only Mathlib, ensuring a self‑contained statement.
Audits verify:
- No extra axioms are introduced.
- Imports respect the standalone policy.
- Every statement has a paired Lean proof.
A proof certificate compiled by the Lean kernel confirms the conjecture’s statement (see the linked video of the compilation).

Lessons Learned

Vibes vs. Understanding – The project succeeded without deep personal expertise, but required constant “vibe‑checking” to detect drift.
Agent Discipline – Separate Lean agents for background formalization and novel results prevented contamination of stable code.
Auditing Infrastructure – Standalone folders, module‑layering checks, and axiom linters were crucial for reviewer trust.
Human Feedback – Emailing mathematicians about typo fixes provided a reality check and a foothold for credibility.
Model Complementarity – Claude excelled at structured Lean generation; ChatGPT was better at exploratory mathematics and criticism.
Token Economics – A more guided workflow could reduce cost by a factor of 5–10.
Proof Presentation – Translating Lean code into a readable PDF remains a bottleneck; interactive proof maps helped bridge the gap.

Community Reactions (Selected HN Comments)

"This approach feels like the difference between wizardry and sorcery; the author summons powerful beings (LLMs) without fully understanding the spell." – @gbjcantab

"I’m not a mathematician. How does the ‘spawn in every gap’ rule get you beyond the rationals?" – @rlue

"The workflow mirrors a real‑world engineering process: multiple agents, adversarial testing, and continuous integration." – @spongebobstoes

"The proof is impressive, but without independent verification the math community will remain skeptical." – @patcon (linked to a professor’s review).

Open Questions

Verification – Independent mathematicians need to audit the Lean code and confirm the logical steps.
Simplification – Current proof length is large; future work may compress it using the generated proof maps.
Generalization – Can the same multi‑agent pipeline be applied to other open problems without domain expertise?
Model Alignment – How can LLM providers better support rigorous mathematical research without encouraging “hallucinated” theorems?

The author invites critique, bug reports, and discussion on the proof repository and Zulip channel.