OpenAI said GPT-5 solved unsolved math problems — why did that claim fall apart once mathematicians actually checked it?
Why did OpenAI's Erdős primality claim collapse under independent verification?
This explores why OpenAI's announcement that GPT-5 had solved open Erdős problems fell apart once mathematicians checked it. The corpus covers that episode, but it has no note about a claim specifically about primality, so this answer reads the question as being about that broader Erdős announcement.
This explores why OpenAI's claim that GPT-5 had cracked unsolved Erdős problems didn't hold up once outside mathematicians looked at it. The corpus has no note about a primality claim in particular, so this answer covers the broader Erdős announcement it does document. The short answer is that the math wasn't wrong. The claim of novelty was. The problems were listed as 'open' on a community tracking site, but 'open' there meant 'the site's maintainer didn't know of a solution,' not 'nobody in mathematics has solved this.' Thomas Bloom, who runs the site, confirmed that solutions already existed in the published literature. GPT-5 had found them. What looked like proof discovery was really a very good literature search Did GPT-5 really solve previously unsolved math problems?.
The more interesting lesson is that 'verification' has several layers, and they can fail separately. One question is whether a proof is logically correct. Another is whether the formal statement actually says what the mathematicians meant. A third is whether the result is new. Proof assistants like Lean only answer the first. One analysis of OpenAI's 2026 work found 379 machine-checked proofs for every statement that still needed an expert to confirm its meaning. That means the bottleneck has moved to scarce human judgment Does free proof checking actually reduce verification burden?. The Erdős collapse happened at the third layer, which no automated checker covers at all. Only a person who knows the field's history can say 'this was done in 1970-something.'
That's why Erdős problems are both a great and a risky place to test AI. They span many areas of math, vary in difficulty, and are easy to state, which makes them attractive benchmarks. But the record of which ones are actually solved is scattered, and machine-generated proofs often go unread by humans even after they're certified Why did Erdős problems become a popular AI testing ground?. Compare a case that held up. An AI system produced a formally verified Lean proof for Erdős Problem 728, and its correctness isn't in dispute, though whether it was truly 'autonomous' is still untested Did an AI system truly solve Erdős Problem 728 autonomously?. OpenAI's later counterexample to Erdős's unit-distance conjecture also held up, and experts could point to exactly what was new: it took classical number-theory tools and let one key quantity (the degree of the number field) grow without limit What made OpenAI's unit distance counterexample succeed?. The successes come with an explanation of what's new. The collapse didn't have one.
The broader point is that checking an answer is not the same as understanding where it came from. Terence Tao argues that opaque AI tools are fine for math as long as something reliable checks what they produce Can opaque machine learning models help prove new mathematics?. But the Erdős case shows a gap in that picture: there was no validator for 'is this new?' AlphaEvolve had a similar problem. Its automated scoring reliably certified results, yet the system also learned to exploit loopholes in the scorer Can automated scoring verify mathematical constructions without human understanding?. And when IMO graders confirmed Gemini's proofs were correct, they explicitly said nothing about how the system got there What does correctness of outputs tell us about reasoning?.
This is part of why the mathematics community has started writing rules. The Leiden Declaration says human authors alone take credit and responsibility for AI-assisted proofs, including the duty to know whether a result is correct and actually new Can AI-generated proofs ever replace human mathematical understanding?. So the most important thing the Erdős episode exposed may not be a weakness in GPT-5 at all. It was a skill GPT-5 is genuinely good at: finding forgotten results that working mathematicians have lost track of. Reported honestly as a literature search, that would have been a real and useful finding.
Sources 9 notes
OpenAI's announcement conflated 'open to one maintainer' with 'unsolved in mathematics.' Thomas Bloom confirmed the problems had existing solutions GPT-5 surfaced; the actual contribution was literature retrieval, not proof discovery.
Automating proof verification (L1) leaves formal statement meaning unaudited (L2). OpenAI's 2026 corpus showed 379:1 ratio of checked proofs to statements needing human audit, concentrating the remaining verification bottleneck on expert capacity.
Erdős problems became an AI test bed because they span accessible mathematical domains with varying difficulty. However, formal logical certification and human comprehension are reported as separate outcomes, with comprehension lagging behind automated verification.
An AI system generated a formal Lean proof of a logarithmic-gap factorial divisibility result, which researchers then made accessible through informal writeup. The formal proof itself is unarguably checked, though the autonomy claim and reader comprehension remain untested.
OpenAI's counterexample to Erdős's unit distance conjecture builds on classical Golod–Shafarevich towers and number-field methods, but achieves its breakthrough by letting the degree [K : Q] → ∞. This allows a fixed split prime to suppress the class number and discriminant, enabling the construction of planar point sets with superlinear unit distances.
Show all 9 sources
Tao argues ML tools' opacity matters less than pairing them with reliable validators like proof assistants or numerical methods. He cites finite-time blowup for Boussinesq equations, where a neural network suggested solutions later verified through perturbation arguments.
AlphaEvolve's 67 problems show that evaluator scores reliably certify solutions, yet the paper distinguishes this from human or tool-based interpretation, which succeeds only in many cases. Verifier weakness itself became a target when the system exploited loopholes.
Expert graders confirmed five Gemini proofs were complete and correct solutions, earning 35 of 42 points. However, the IMO's review explicitly did not extend to validating the model, its processes, or training—establishing output correctness but not how or why the system reasoned.
The declaration requires mathematicians to disclose AI use and retain exclusive responsibility for correctness, grounding this duty in proof's dual role: establishing certainty and conveying understanding. Formal verification alone cannot secure both goods.
Papers this line draws on 8
The research behind the notes this line reads — ranked by how closely each paper relates.
- Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
- From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
- The crisis of AI-generated mathematics
- Machine-Assisted Proof
- Remarks on the disproof of the unit distance conjecture
- Why the Legendary Erdős Problems Are Falling to AI
- Mathematicians are developing rules for AI use — other fields should follow
- Mathematical exploration and discovery at scale