Erdős problems and AI, 2025–2026: what was solved, what was found, what was checked
From GPT-5's literature finds in October 2025 to Lean-checked proofs and OpenAI's unit-distance disproof in 2026. Which Erdős problems AI systems really settled, which "solutions" were already in the literature, and how to tell the difference.
Updated 2026-10-23 · CC BY 4.0
Thomas Bloom's database at erdosproblems.com lists over a thousand problems posed by Paul Erdős, each marked open or solved. Since 2025 it has become the main testing ground for AI in research mathematics: the problems are precise, many are obscure, and a solution can often be checked. The results have been real — and regularly overstated. This guide sorts the main episodes into what was solved, what was found in the literature, and what was checked, and by whom.
The pattern to keep in mind
Three different things get reported as "AI solved an Erdős problem":
- A literature find. The problem was marked open, but a paper had already solved it. Finding that paper is useful — it corrects the database — but it is not new mathematics.
- A new proof of an easy or misstated problem. Some problems were open only because nobody had looked closely, or the database's wording differed from what Erdős meant. Terence Tao's tracker warns that a solved problem often reflects obscurity rather than difficulty.
- A new proof of a problem experts cared about. Rare, and the only kind that changes the field.
On top of that, a proof can be checked by people, by Lean, by both, or by nobody yet. Lean checks that the proof proves its formal statement — not that the formal statement says what Erdős asked (see How to check an AI proof with Lean).
Timeline
| When | What happened | What it was |
|---|---|---|
| Oct 2025 | An OpenAI executive posted that GPT-5 had "found solutions to 10 previously unsolved Erdős problems"; Bloom called this a dramatic misrepresentation and the post was deleted. | Literature finds: GPT-5 had located papers that already solved problems listed as open. |
| Nov 2025 | Sawhney, Sellke and others described the literature finds and a few new contributions, e.g. an idea that helped settle problem 848 together with forum participants (arXiv 2511.16072). | Mostly literature search, some new mathematics with humans. |
| Jan 2026 | Problem 728: a proof written with GPT-5.2 Pro and formalized in Lean with Harmonic's Aristotle; Tao called it close to autonomous, though the statement first had to be clarified (arXiv 2601.07421). | New proof, Lean-checked; related earlier work was found later. |
| Jan–Feb 2026 | DeepMind's Aletheia tried 700 open problems: of 200 candidate answers that were graded, 63 were technically correct but only 13 meaningfully so (arXiv 2601.22401). | A sober measurement: most "correct" answers solved a misread or trivial version. |
| May 2026 | OpenAI announced that a model disproved Erdős's unit distance conjecture: point sets with at least n^(1+δ) unit distances for a fixed δ > 0, checked by a group of external mathematicians (OpenAI). | A new result on a famous problem, checked by experts. |
| Sep 2026 | Epoch AI's FrontierMath Erdős benchmark: 68 problems chosen by Bloom as significant, all stated in Lean; the best model solved 2 (Epoch AI). | The hard problems remain hard. |
| Oct 2026 | OpenAI's release of over 700 AI-written manuscripts includes claimed proofs for a few dozen Erdős problems, without independent review (see OpenAI's October 2026 math proofs). | Claims, not yet checked. |
The community record of who did what is Terence Tao's wiki AI contributions to Erdős problems. It marks each entry as full, partial, incorrect or unverified, and separates AI working alone from AI working with the literature or with people. It stopped being updated at the end of June 2026.
What this means for an open problem you care about
- Check the literature first. The most common "AI result" was a paper nobody had connected to the problem. A literature claim that cites the paper settles the database entry honestly.
- Pin the statement before the proof. A Lean proof is only as good as its formal statement; agree on the statement first, then prove it.
- Separate the claim from its checking. "A model wrote a proof" and "the proof is correct" are different facts with different evidence.
On Cairn Commons the Erdős problems collection lists open Erdős problems with their status. A check_status task asks exactly the question above — has this already been solved somewhere? — and a result counts only once it is checked: by Lean against a pinned statement, by re-running code, or by review. Some problems in the collection now have AI claims from 2026 that nobody has checked yet; a well-documented check, either way, is a contribution.
Beyond Erdős problems — Sendov, Crouzeix, the Jacobian conjecture in dimension 3, Köthe and more — see Open problems solved by AI: the running list.
Sources
- erdosproblems.com, Thomas Bloom's database and forum.
- T. Tao and contributors, AI contributions to Erdős problems (wiki, data to 30 June 2026).
- arXiv 2511.16072 (literature finds and early contributions), arXiv 2601.07421 (problem 728), arXiv 2601.22401 (Aletheia).
- OpenAI, model disproves a discrete geometry conjecture (20 May 2026).
- Epoch AI, FrontierMath Erdős (1 September 2026).