The Proof Machines

Machines are now closing real problems in mathematics, and a Millennium Prize problem is among the claims. What has actually been proved, what has been retracted, and why the discipline is arguing about its own future. 24 pages, 60 sources.

Summary

A field note on what artificial intelligence has actually proved in mathematics, what it has not, and why four of the six open Millennium Prize problems have attracted no machine attention at all.

Machines are now closing real problems in mathematics, and a Millennium Prize problem is among the claims. In the twelve months to September 2026 a machine-written counterexample disproved a famous conjecture of Erdos and was verified by nine mathematicians including a Fields Medallist; a model improved a longstanding bound on the Riemann zeta function; another produced the first end-to-end machine-checked proof of Fermat's Last Theorem in eleven days; and on 8 September 2026 OpenAI announced a resolution of one of the four statements the Clay Mathematics Institute accepts as settling the Navier-Stokes problem, while declining to claim the prize. This Special Report separates what has been independently verified from what has been announced, sets both against a documented record of claims that were withdrawn, and takes seriously the objection mathematicians themselves are raising about credit, verification and a finite supply of open problems.

Key findings

1. The verified core is small, and it is real An AI-generated counterexample disproved the Erdős unit distance conjecture and was rewritten and verified by nine named mathematicians, Gowers among them. That is not a benchmark score. That is a theorem.
2. Formalization is where the machines are strongest Fermat's Last Theorem was formalized end to end in eleven days, machine-checked, with no unproved assumptions. The mathematician who has spent two years on the same target confirmed it compiles, and said it adds no mathematics.
3. The retraction record is part of the evidence The single most publicized claim of the period, ten Erdős problems solved, was a literature search misread as discovery and was withdrawn within a day. DeepMind's own paper reclassifies nine of its thirteen results the same way.
4. A Millennium claim exists, and the prize rules do not care yet Clay requires publication in a refereed outlet and two further years of survival. No prize can be awarded before late 2028 at the earliest, and OpenAI has said it will not claim one.
5. The hardest problems remain untouched No system has claimed progress on Yang–Mills, Hodge, Birch and Swinnerton-Dyer, or P versus NP. Prediction markets price a Millennium solve at 82 percent by the end of 2027 against that silence.
6. Mathematicians are asking for rules, not a moratorium Nearly four thousand of them, including Scholze, Tao and Buzzard, signed a declaration holding that credit and responsibility belong to humans. The argument is about attribution and verification, not capability.

How to cite this report

The Proof Machines. FAIR Labs Frontier Series, Special Report. Fair Artificial Intelligence Research Labs, 2026. Available at https://fairlabs.ai/research/frontier-special-the-proof-machines

Topics: automated theorem proving, Lean, mathlib, formalization, Millennium Prize Problems, Navier-Stokes, Riemann hypothesis, Fermat's Last Theorem, Erdos problems, AlphaProof, AlphaEvolve, research integrity, peer review

FAIR Labs (Fair Artificial Intelligence Research Labs) is a nonpartisan 501(c)(3) research institute in Washington, DC. Its reports may be reproduced with attribution for non-commercial purposes. For interviews, briefings or data requests, use the contact form.

Related FAIR Labs reports