How I Vibed a Proof of Conway's Conjecture
A self-described math noob spent a month and $40k in AI tokens to prove a 50-year-old mathematical conjecture—without understanding the math—by treating AI agents like a distractible engineering team and using Lean as ground truth.
Read Original Summary used for search
TLDR
• The winning workflow: Math agents generate ideas slightly ahead of Lean agents that verify them—close enough to catch mistakes fast, far enough to allow exploration
• "Burn it down" twice: Deleted everything and salvaged only what survived adversarial review, cutting through 30+ AI-generated "papers" of impressive-sounding nonsense to find one real result
• Terminology discipline saved the project: AI models drift into inventing vocabulary ("drift fuel," "resonance-necessity conjecture"); solution was forcing them to use only terms from actual papers
• Multi-agent coordination with roles: PM, Math agents, Red team (finding flaws), Lean agents (verification), with intentional separation between stable and experimental work
• The proof is Lean-certified and uses a Cantor-Bendixson rank filtration that previous approaches missed, but cost ~40 billion tokens ($40k at API pricing)
In Detail
The author set out to prove Conway's refinement conjecture—a 50-year-old open problem about surreal numbers—using frontier AI models despite having no mathematical expertise. The conjecture states that omnific integers (the integer part of Conway's surreal number system, including infinities like ω) have a refinement property: if ab = cd, you can break a and b into pieces that recombine into c and d.
The breakthrough came from treating AI like a poorly-managed engineering team that needs constant supervision. Early attempts failed spectacularly: Claude would generate grandiose nonsense ("The stage-1 obstruction of C* is not rigid...drift fuel exists"), while letting agents work unsupervised produced 30+ "papers" of invented terminology and circular reasoning. The solution was a multi-agent laboratory with strict roles: a PM coordinating work, Math agents exploring ideas, Red agents finding flaws, and crucially, Lean agents providing formal verification. The winning pattern kept Lean slightly behind the math work—close enough to verify within hours, preventing the house-of-cards problem where unverified claims pile up.
Two "burn it down" moments saved the project. Each time, the author deleted everything and asked fresh AI sessions to salvage only what survived critical review. This cut through the impressive-sounding slop to find real mathematics: a novel result about polynomial rings that became the foundation for the final proof. The proof uses Cantor-Bendixson rank to create a multiplicative filtration—an approach the AI discovered after being told to "just have fun" with existing results. The final proof is Lean-certified with standalone statements that only import community-maintained libraries, making it reviewable by humans. The cost: ~40 billion tokens ($40k at API pricing), though the author estimates it could be done 5-10x cheaper with better steering and actual mathematical insight.