On September 18, 2026, software developer Dan Abramov — who calls himself a "math noob" — published a machine-checked Lean proof of Conway's refinement conjecture, a question John Conway posed in 1976 about the integers of his surreal number system.
The conjecture
Take the number 210. It factors as 10 × 21 and also as 6 × 35. Split 10 = 2 × 5 and 21 = 3 × 7, regroup to get 6 = 2 × 3 and 35 = 5 × 7. For ordinary integers, any two factorizations admit a common refinement — so obvious it hardly seems worth stating.
Conway asked whether the same holds for omnific integers, the integer part of the surreal numbers. Surreal numbers grow from a single rule: place existing numbers on a line and generate a new number in every gap, including the leftmost and rightmost gaps. Day 0 yields 0; day 1 yields -1 and 1; day 2 yields -2, -1/2, 1/2, 2; and so on endlessly, absorbing the reals, the ordinals, and stranger creatures into one binary tree. Omnific integers include ordinary integers like 3 and -5, but also ω, 2ω, ω × ω, ω^ω, and -ω/7.
The refinement conjecture states: if ab = cd, then there exist e, f, g, h with a = ef, b = gh, c = eg, d = fh — i.e., every two factorizations share a common refinement.
Prior work by L'Innocente and Mantova (*Advances in Mathematics*, 2024, doi:10.1016/j.aim.2024.109513) reduced the problem to whether every irreducible element with infinite support in the generalized power series ring K((ℝ^≤0)) is prime. Abramov initially believed Claude's claim that the problem was "perfectly reduced" — he later found this was wrong, and the real proof required far more.
Five weeks, from mess to machine
- Week 1: Fed papers as TeX to models and asked them to attack the conjecture directly. Output, in Abramov's words, read like bad science fiction — invented terminology and dramatic assertions.
- Week 2: Deployed Codex locally and built a multi-agent lab: a project manager, several math agents, a red-team agent hunting flaws, a free-roaming random agent, and Lean agents. Codex's Goals feature periodically reminded each session of its objective; sessions could message each other, with a "cafeteria" agent broadcasting every message to all. No proof resulted.
- Week 3: ChatGPT nearly declared the problem solved based on a file named
working_direct_cantor_bootstrap.md. A fresh session later admitted the file contained circular statements; ChatGPT's verdict was "we currently don't have a proof." Earlier "papers" were invalidated too. The project paused for about a week. - Week 4: Abramov "burned it all down" and pivoted to auditing existing literature. One session's diagnosis, quoted in the post: no file in the folder gave a credible proof of Conway's conjecture; the real failure was epistemological — the drafts created a large private theorem literature and cited load-bearing results before independent verification. He emailed mathematicians to check claimed typos: some corrections were confirmed, some flagged issues were misunderstandings, and several "novel" claims were correct but unhelpful. The audit yielded a strong new result — the finite-degree part of the principal ring is a polynomial ring — confirmed as novel by human mathematicians and certified in Lean.
- Week 5: Audit infrastructure: the Lean work was consolidated into a
standalonedirectory with strict rules — no imports beyond Mathlib (not even the project's own code), everyFoofile paired with aFooProoffile pinning statements to actual proofs, checks for extra axioms and import compliance, and statements under 500 lines so a human mathematician can read them. Two Lean agents were separated: one certified only upstream prerequisite papers; the other (task kept secret from the first) certified the novel finite-degree result in an independent work tree. Tooling included Lean Comparator, TauCeti review rules and axiom checker, Verso Blueprint, and layered module audits. Important theorems were tagged with a special attribute to auto-generate Mermaid proof-structure diagrams, exposing detours on the "mathematical spine." - Palomar registry mechanical check: passed (entry PALOMAR-2026-09-03-000002, version 1); interactive proof map at https://gaearon.github.io/conway-refinement
- People familiar with Lean and the field consider the statement looks correct
- Independent verification by mathematicians: not yet done
- Abramov: "My proof has not been independently verified by mathematicians," while adding he has "fairly good reason to believe the proof is correct and sincerely invites others to try to refute it." The proof also assumes no bugs in the Lean kernel.
Abramov's takeaway: models can't optimize what they can't see. Want a simpler proof shape? Make the model *see* the shape. Conversely, models can't ignore what they see — strip out unwanted terminology.
Cost: one month, 40 billion tokens
Roughly 40 billion tokens total (~210 million output tokens), over 95% cache reads, saturating both Claude and ChatGPT 20x Pro subscriptions weekly — about $40,000 at current API prices. Abramov estimates better steering could have cut the cost 5–10x. His repeated observation: Claude excels at writing Lean given a clear, correct target; ChatGPT is on average better at thinking about new math and noticeably better at coordination and staying on goal. His answer: use both.
Verification status
What this does and doesn't show
The news cycle's attention went to OpenAI's Navier–Stokes effort (~10,000 concurrent agents, ~2.7 million messages, ~130 billion output tokens, 88 hours to a result, 17 hours of Lean formalization), with Terence Tao commenting on Mastodon that "the flag has been captured, the ball is in the net, the problem is solved — at the cost of the lost experience, insight, collaboration, and where new goals would have been."
Abramov's project is different: no fleet, one person, one month, one local agent lab, and a machine-checkable proof. What it demonstrates: someone with essentially no domain knowledge, outsourcing verification to Lean, can push a result through — but models drift repeatedly and cannot organize the engineering work themselves. Abramov thinks his own role could have been filled by a dedicated manager agent that notices when agents are going in circles. He also predicts that as low-hanging fruit disappear, the niche of the "clueless dedicated amateur" may shrink again, and that mathematicians themselves remain where AI delivers the most value.
The open question: if success depended on the author recognizing when models were spinning and decisively burning twenty-plus drafts in week three, is that judgment mathematical ability or engineering management? There is no measured answer yet.
References
1. Dan Abramov, *How I Vibed a Proof of Conway's Conjecture*, overreacted.io, 2026-09-18. https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/ 2. Interactive proof map: https://gaearon.github.io/conway-refinement (Palomar registry entry PALOMAR-2026-09-03-000002, version 1) 3. S. L'Innocente, V. Mantova, *A factorisation theory for generalised power series and omnific integers*, Advances in Mathematics, 2024. doi:10.1016/j.aim.2024.109513 4. LavX News, *Developer Uses AI to Prove 50-Year-Old Conway Conjecture*, 2026-09-18. https://news.lavx.hu/article/developer-uses-ai-to-prove-50-year-old-conway-conjecture 5. Malay Mail / AFP, *Math's midlife crisis: AI solves in four days what stumped mathematicians for a century*, 2026-09-18 (interviews with Terence Tao, Steven Strogatz, Mohammed Abouzaid, et al.)