A developer used AI agents to prove an open math conjecture

Dan Abramov, a programmer with no research background in mathematics, spent about a month using AI to produce a proof of an open conjecture and then formalized it in Lean so a computer could check it. The conjecture comes from John Conway and concerns omnific integers, the whole-number part of surreal numbers. In plain terms it asks whether a factoring property that holds for ordinary integers also holds in this stranger number system. Abramov did not solve it by hand. He built a workflow where different models played different roles: ChatGPT for structured mathematical exploration, which he found more skeptical, and Claude for writing the Lean formalization, with Codex running a local multi-agent setup to manage the passes.

The numbers are striking. The project burned through about 40 billion tokens, most of them cached reads, at a rough cost of $40,000 in API fees. Progress came not from one clever prompt but from finding a real intermediate result, which he calls finite-degree primality, that anchored the rest of the work. For the final check he ran two Lean agents in parallel, one verifying the known prerequisites and one proving the new part independently.

The proof is not yet confirmed by mathematicians. It passes mechanical checks in the Palomar registry, and a few people who know Lean and the field think the statement looks right, but Abramov is careful about this and openly invites anyone to find the flaw. As he puts it, assuming the proof does not rely on a bug in the Lean kernel, it is probably legitimate.

Why it matters

This is a concrete data point on where AI-assisted math stands: a non-expert can now push a real conjecture to a machine-checkable proof, but the cost is high and human verification still decides whether it counts. If you work in formal methods or research, the workflow, not the headline, is the part worth studying.