# Conway's refinement conjecture — Dan Abramov got AI to write a Lean proof

> A month of free time and roughly $40,000 of tokens, spent turning three chatbots into a machine-checked proof.

- Org: Dan Abramov
- Date: 2026-09-18
- Category: showcase, article, repo
- Source: https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/
- Canonical page: https://ai-tldr.dev/releases/gaearon-conway-refinement-proof/

## In short

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.

## What it is

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 it works

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 it matters

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 it's for

formal-methods people and anyone testing agents on long tasks

## Try it

https://github.com/gaearon/conway-refinement

## Links

- [Blog Post](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/)
- [Lean Proof Repo](https://github.com/gaearon/conway-refinement)
- [HN Discussion](https://news.ycombinator.com/item?id=49755024)