# I used AI to prove a 50-year-old math conjecture > A programmer spent a month and billions of tokens getting frontier models to solve Conway's refinement conjecture in Lean. - Title: I used AI to prove a 50-year-old math conjecture · Overreacted - Summary: A programmer spent a month and billions of tokens getting frontier models to solve Conway's refinement conjecture in Lean. AI can prove novel mathematics… - Keywords: conway's conjecture, surreal numbers, john conway, lean, formal verification, claude, chatgpt, mathematical proof, ai mathematics, omnific integers, theorem proving, palomar registry - Source: Overreacted — https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture - Read time: 3 min - Topics: conway's conjecture, surreal numbers, john conway, lean, formal verification, claude, chatgpt, mathematical proof, ai mathematics, omnific integers, theorem proving, palomar registry ## The absurd challenge A self-described math noob decided to use AI to solve an open mathematical problem. The target: Conway's refinement conjecture, posed 50 years ago. ## What surreal numbers are Surreal numbers contain all real numbers, all infinitely large ordinals like omega, and unholy combinations like 75 plus omega times 3 plus 1 over omega. ## Born from a single rule Surreals spawn from one rule: take all numbers so far, then birth a new number in every gap. Apply forever and you get every real, every ordinal, and more. ## Conway's last standing conjecture The conjecture claims omnific integers have a refinement property: if ab equals cd, there are integers e, f, g, h with a equals ef, b equals gh, c equals eg, d equals fh. ## One-shotting failed spectacularly Early attempts to just tell Claude to solve it produced impressive-sounding word salad with invented terminology and dramatic claims that couldn't be verified. > The stage-1 obstruction of C* is not rigid. With designed resonance, arithmetic-progression offsets making the window equations honest Toeplitz systems ## Enter the skeptic Switching to ChatGPT with a critical personality helped. It called out Claude's bullshit and produced smaller, more verifiable claims in plain language. ## Building a laboratory Multiple AI agents were assigned different roles: a PM driving toward the goal, math agents finding breakthroughs, a red agent finding flaws, and a Lean agent formalizing work. ## The first dead end The workflow produced a giant TeX document and a pile of Lean, but didn't close the conjecture. The stack grew to almost thirty papers, full of nonstandard terminology. ## A circular proof ChatGPT came close to declaring Conway solved, but a fresh session found the proof was circular. Honest verdict: we do not have a proof. > i do want you to be honest btw. if you can't strictly salvage it then we need to stop and understand why ## Finding real ground To verify the work, the focus shifted to finding mistakes in peer-reviewed papers. Mathematicians confirmed several typos and small flaws were real, building confidence. ## Burning it all down Starting from scratch, ChatGPT audited the pile of papers. Only 10 to 15 percent contained mathematics worth preserving. The rest was thrown away. > The real failure is epistemic, the drafts manufacture a large private theorem literature, then cite it as established before its load-bearing results have been independently verified ## A novel result emerges Buried in the papers was one coherent interesting result: the finite-degree part of the principal ring admits a direct proof that it's a polynomial ring. ## Separating stable from risky Two Lean agents worked separately: one certified peer-reviewed papers, the other worked on novel results. This prevented experimental work from tangling with accepted mathematics. ## Making proofs legible Converting Lean to readable math was exceedingly difficult. The model kept using strange terminology and hallucinated shortcuts, producing slop no matter how many reviews. ## Stripping out the nonsense All non-standard naming was stripped from Lean code and replaced with letters. A fresh context then chose new names based on a map of accepted terminology. ## The final breakthrough After asking if they were circling, ChatGPT proposed using Cantor-Bendixson rank to create a multiplicative filtration. The idea checked out and was formalized in Lean. > are we circling? ## Conway's conjecture proved Twelve hours after the final push, the theorem compiled. Conway's refinement conjecture, the original target, was kernel-checked for the first time. > Unchanged Conway now compiles as the standalone proof certificate. This is the first point where the actual target, not an intermediate restriction, is kernel-checked ## The token bill The project consumed around 40 billion tokens, of which 210 million were output. At current API pricing, this would cost roughly $40,000. ## Key takeaway AI can prove novel mathematics when combined with formal verification, but requires constant human steering to avoid drift into nonsense.