Dan Abramov · 2026-09-18 · notable
Conway's refinement conjecture — Dan Abramov got AI to write a Lean proof
Dan Abramov spent a month and about 40 billion tokens steering Claude, ChatGPT and Codex until they produced a Lean 4 proof of Conway's refinement conjecture. He says no mathematician has checked it yet.
A month of free time and roughly $40,000 of tokens, spent turning three chatbots into a machine-checked proof.
What is it?
Conway's refinement conjecture is the target: if ab = cd for omnific integers, then there are further integers e, f, g, h with a = ef, b = gh, c = eg and d = fh. Dan Abramov, who is not a research mathematician, worked on it for about five weeks of free time and published the result as a Lean 4 development in the repository gaearon/conway-refinement, released under Apache-2.0.
How does it work?
Abramov split the work by model. Claude handled Lean formalization when the goal was already unambiguous, ChatGPT did the novel mathematical thinking and coordination, and Codex's Goals feature helped manage sessions. He built custom tooling to visualise the proof structure and leaned on Mathlib, the community mathematics library. The run consumed roughly 40 billion tokens, of which about 210 million were output and over 95% were cache reads, which he estimates at around $40,000 at current API prices.
Why does it matter?
Lean gives a hard answer to the usual worry about AI-generated mathematics: the compiler either accepts the proof or it does not, so hallucinated steps cannot survive. Abramov's account is a detailed record of what that costs in practice and where each model helped, which is more useful to anyone planning similar work than a benchmark score. He is careful about the claim: the proof passed the Palomar registry's mechanical checks as PALOMAR-2026-09-03-000002, but he writes that it has not been independently verified by mathematicians.
Who is it for?
formal-methods people and anyone testing agents on long tasks
Try it
https://github.com/gaearon/conway-refinement