From Bad Sci-Fi to Machine-Checked Proof: A Layperson's Month-Long Assault on Conway's Conjecture
Take the number 210. It factors as 10 × 21, and also as 6 × 35. Split 10 into 2×5 and 21 into 3×7, regroup as (2×3) and (5×7), and you get 6 and 35. The same 210 is really four numbers being rearranged underneath. For ordinary integers, this is so obvious it isn't worth stating.
What John Conway asked in 1976 was: does this still hold for his own system of numbers?
Fifty years later, on September 18, 2026, a machine-checked Lean proof was posted by Dan Abramov, a software developer who calls himself a "math noob" in his write-up.
What Counts as an "Integer"
To understand the conjecture, you first need surreal numbers.
Conway's system grows from a single rule: lay existing numbers on a line, and generate a new number in every gap between adjacent numbers — with "leftmost" and "rightmost" counting as gaps. Day one has one gap, producing 0. Day two produces −1 and 1. Day three produces −2, −1/2, 1/2, 2. This continues endlessly, packing the reals, the ordinals, and all sorts of strange hybrids into a single binary tree.
The "integer part" of the surreals is called the omnific integers. They include ordinary integers like 3 and −5, but also infinite quantities like ω, 2ω, ω×ω, ω^ω, and −ω/7. On the tree, you find them by looking at paths: all-left, all-right, or changing direction exactly once after infinitely many steps.
Conway's refinement conjecture says: if ab = cd, then there exist e, f, g, h such that a = ef, b = gh, c = eg, d = fh. In the 210 example, this means any two factorizations admit a common refinement.
Conway believed the omnific integers have enough structure to preserve this property. The question stayed open until the factorization theory of L'Innocente and Mantova (*Advances in Mathematics*, 2024, doi:10.1016/j.aim.2024.109513) reduced it to a question about generalized power series: whether every irreducible element with infinite support in K((ℝ^≤0)) is prime. When Abramov picked the topic, Claude told him the problem "had been perfectly reduced."
He later found that statement was wrong — the actual proof required far more than that reduction.
Five Weeks, From Tangled Mess to a Machine
The project took about a month. The process is more informative than the result, because it exposes the full failure modes of "doing math with AI."
- Week 1: Directly asking models to prove the conjecture or find a counterexample. Abramov describes the output as bad science fiction — full of invented terminology and dramatic claims.
- Week 2: Running Codex locally, building a multi-role agent lab (project manager, several math agents, a red-team agent hunting for flaws, a random free-exploring agent, and a Lean formalization agent). Key Codex features: periodic goal reminders per session, and inter-session messaging. A "cafeteria" agent forwarded every message to everyone. The result: a huge TeX document and some Lean code, no proof.
- Week 3: First dead end — see below. The project paused for about a week.
- Week 4: "Burn it all down" — pivoting to auditing existing literature and certifying finite-degree results in Lean.
- Week 5: Separating the Lean audit chain, hardening a
standalonedirectory, and getting the final theorem to compile. - No imports beyond Mathlib — not even the project's own code.
- Every
Foofile paired with aFooProoffile, pinning each statement to its actual proof. - Audit checks: no extra axioms, import compliance, statement–proof pairing.
- Statements under 500 lines — human-readable by mathematicians.
- ~400 billion total tokens, ~210 million output tokens
- Over 95% cache reads
- Both Claude and ChatGPT 20x Pro subscriptions maxed out every week
- ~$40,000 at current API prices
- Author estimates 5–10× cheaper with better guidance
The Night It Claimed "Solved"
Week 3 featured a textbook failure. ChatGPT came close to declaring the conjecture resolved, citing a file called working_direct_cantor_bootstrap.md that claimed a complete solution. Abramov had a fresh session attack it; hours later, the new session admitted it contained circular statements. ChatGPT's final verdict: "we don't currently have a proof." Subsequent checks found similar logical flaws in earlier "papers," invalidating all of their claimed results.
That week the document count ballooned from about thirteen to nearly thirty — any single error invalidates everything downstream. Lean formalization lagged badly, with none of the project's own results certified. The project stalled for a week.
"Burn It All Down" Saved the Project
Back in week 4, Abramov changed direction: instead of attacking the conjecture, audit the existing drafts for errors.
He did two things. First, he had models review the drafts — one fresh session's answer is quoted in the original: "No file in this folder currently provides a credible proof of Conway's conjecture... the real failure is epistemic — the drafts manufactured a large body of private theorem literature, then cited it before its load-bearing results had been independently verified."
Second, he emailed mathematicians to verify typos the models flagged. Results were mixed: several corrections were confirmed real; several flagged issues turned out to be misunderstandings without Lean backing; several "novel" model claims were judged correct but unhelpful.
This audit round produced one strong new result: the finite-degree part of the principal ring is a polynomial ring. Abramov and human mathematicians confirmed its novelty, and it was subsequently certified in Lean.
When asked to self-assess its output structure, the model estimated: roughly 10–15% contained mathematics worth keeping, 35–45% was normal mathematics but not a contribution, and 40–50% was "bullshit" — towers of grand theorems, invented labels, and conditional assumptions presented as progress.
The Anti-Drift Wall
Week 5 was about audit infrastructure — possibly the most transferable part of the project. The standalone directory enforced:
Two Lean agents were split: one only certified upstream prerequisite papers; the other certified the novel finite-degree primality result, running in an isolated worktree and forced to build only on upstream-accepted work. The latter's task was kept secret from the former. In the previous lab, a single Lean agent doing both mixed immature abstractions with accepted mathematics.
Tooling included Lean Comparator, TauCeti review rubrics and axiom checkers, Verso Blueprint, and modular layered audits.
One small change helped readability enormously: marking "important" theorems with a special attribute in the Lean source and auto-generating Mermaid proof-structure diagrams. His conclusion: models can't optimize what they can't see. If you want simpler proof shapes, make the shapes visible — and conversely, models can't ignore what they see, so strip out terminology you don't want.
A Month, 400 Billion Tokens
A repeatedly validated observation on model分工: Claude is strong at writing Lean given a clear, unambiguous target; ChatGPT is on average better at thinking about new mathematics and noticeably better at coordination and goal persistence. Abramov's answer: "use both."
How Far Has Verification Actually Gone?
This is the part that needs to be stated most clearly.
| Item | Status | |---|---| | Palomar registry mechanical check | Passed — entry PALOMAR-2026-09-03-000002, version 1 | | People familiar with Lean and the field | Believe the statement looks correct | | Independent mathematical verification | Not completed | | Author's stance | Explicitly invites refutation | | Premise | Proof assumes no bugs in the Lean kernel |
Abramov's own words: "my proof has not been independently verified by mathematicians," while adding that he has "fairly good reason to believe the proof is correct, and I sincerely invite others to refute it."
He also left one easily missed self-correction: Claude's original claim that the problem "had been perfectly reduced" was wrong.
What It Cannot Yet Tell Us
For context: the past week's public discussion of AI in mathematics has centered on OpenAI's Navier–Stokes event — roughly 10,000 concurrent agents, ~2.7 million messages, ~130 billion output tokens, a result in 88 hours plus 17 hours of Lean formalization. Terence Tao commented on Mastodon: "Flag captured, ball in the net, problem solved — at the cost of the lost experience, insight, collaboration, and placement of new goals."
Abramov's project differs in one key respect: no fleet deployed. One person, one month, one local agent lab, and a machine-checkable proof at the end.
What this project actually answers is a different kind of question: how far can someone with zero domain knowledge get by outsourcing "verification" to Lean? The answer comes in three parts. He did obtain a proof while knowing almost none of the mathematics. The models drifted repeatedly and could not organize engineering work on their own. And he believes his own role could have been filled better by a dedicated meta-agent managing the others — one that could tell when they were spinning in circles and when they needed encouragement.
His judgment: as the low-hanging fruit gets picked, the niche of the "clueless dedicated amateur" may shrink again. He is explicit that the highest-value use of AI remains in the hands of mathematicians themselves.
Which leaves the open question: if a project's success hinges on the author's ability to see that the models are spinning, and to decisively burn two dozen drafts in week three — does that judgment belong to mathematical ability, or to 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.)