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.
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
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.