AI Proves Open Problems
Since January 2026 AI systems are credited with settling open questions: Erdős problems, the unit-distance conjecture (May), a Riemann-zero bound (company-reported) and a claimed forced Navier-Stokes blow-up (unverified).
Open in the interactive tree →Until recently computers helped with proofs only as calculators; in 2026 AI systems supply ideas and complete proofs themselves, which human experts then check. Terence Tao cautions that many open Erdős problems are easier than their age suggests, because few people ever seriously attacked them. Even so, some results had resisted experts for decades.
As of October 2026
January 2026: Erdős problem 728 was solved with GPT-5.2 Pro and Harmonic's Aristotle (checked in Lean), regarded as the first Erdős problem solved near-autonomously by AI with no prior literature found. 20 May 2026: OpenAI announced a disproof of Erdős's planar unit-distance conjecture of 1946, with point sets that have polynomially more unit distances than the square grid; nine external mathematicians verified and shortened the proof. 10 August 2026: an internal Claude version raised the proven share of simple zeta zeros on the critical line from about 41.6% to above 67% (checked by Anthropic's Alpöge and Furman; shorter proof by Lamzouri, arXiv 2609.02882). 8 September 2026: OpenAI's forced Navier-Stokes blow-up (see that node).
Open steps
- Triage of open-problem lists High AI leverageSweep curated lists such as the Erdős problems for entries already solved in the literature or within reach of current models, and rank the rest by tractability.
- Search for extremal constructions High AI leverageUse evolutionary code search to improve bounds in combinatorics and geometry (Ramsey numbers, point sets, packings), where a better example is itself a checkable proof.
- Review pipeline for long machine proofs Medium AI leverageSet up independent expert and Lean checking for proofs of 100+ pages, including whether the formal statement matches the claim; the unit-distance proof needed nine reviewers.
- Human-readable versions of AI proofs Medium AI leverageTurn machine-found proofs into short arguments that show the idea and transfer to related problems; the zeta-zero result was later shortened by human authors.
Where AI could help
High AI leverage. Open problems with checkable answers fall fastest; the limits are choosing problems that matter and expert verification.
- Run agent swarms on catalogued open problems and bound tables, with Lean or exact verifiers on every claim
- Evolutionary code search for extremal constructions and counterexamples
- Automatic novelty checks against the literature before experts spend time
- Triage queues that route promising results to human reviewers
Shown so far
- In January 2026 GPT-5.2 Pro solved a tightened form of Erdős problem 728, Harmonic's Aristotle formalized it in Lean, and Terence Tao estimated only 1 to 2 percent of open Erdős problems are this easy for current AI. source
- In August 2026 Anthropic reported that an internal Claude research model proved that about 67.2% of the non-trivial zeta zeros lie on the critical line (previous record 41.6%), with a Lean formalization, according to the company. source
- A March 2026 preprint reported that AlphaEvolve raised lower bounds for nine classical Ramsey numbers, for example R(3,13) from 60 to 61 and R(4,16) from 170 to 174. source
Prerequisites
- Formal Proofs (Lean, Rocq)2005-2026
- AI Wins Math Olympiad Gold2025