Mathematicians Put OpenAI to the Test: Only One of 30 Number Theory Papers Verified in Lean
In the week after October 6, 2026, the mathematical community faced something entirely new: a single release with hundreds of claimed solutions to open research problems — and a field with limited capacity to check them. The burden of proof has now shifted from those claiming the results to those expected to verify them.
What Actually Happened
OpenAI published a database of claimed proofs for a long list of open problems in mathematics and computer science. Exactly how many results are included remains unclear: Globes and New Scientist report 722 studies, TechCrunch 719 manuscripts, and The New York Times 377 findings. The numerical context suggests the sources are partially referring to different units — studies, manuscripts, and findings — but none of the figures can be established as "correct" from the available coverage. The results span, according to The New York Times, algebra, number theory, theoretical computer science, mathematical logic, and topology, and were published on Tuesday, October 6, using what the paper describes as "a more advanced model that has not been released."
At the same time, according to Globes, Amnon Shashua announced that his company doubleAI has solved the longest path problem in graph theory — a problem the company claims has stood unsolved for 38 years — at a cost of under $2,000, using a new algebraic formula said to raise a constant from 4/3 to 1.6. All of these figures come from Shashua's post on X and have not been independently verified.
The release came a little over a month after OpenAI announced a solution to a problem derived from the Navier–Stokes equations — a controversial release that the mathematical community said breached established norms. It is against this backdrop that mathematicians are now reacting.
What Is Actually Claimed to Be Proven
Despite the headlines in the coverage, the Riemann Hypothesis is not claimed to be solved. OpenAI puts forward, according to Globes, a proof of a weaker version, called the "Quasi-Riemann Hypothesis" — described as a significant step toward one of mathematics' greatest mysteries. Among the other results are a proof of the irrationality of Catalan's constant, a version of Hilbert's tenth problem concerning rational solutions, and progress on Nagata's and Goldfeld's conjectures.
New Scientist reports one of the most striking cases: mathematician Francis Johnson, who has worked for 25 years on Wall's D(2) problem, expressed astonishment that it should have been solved. OpenAI declined to name the model behind the findings, stating only that it was an "internal frontier model," according to New Scientist.
How Verification Is Supposed to Work — and Where It Breaks Down
Formal verification in mathematics normally proceeds via Lean, a proof-assistant language in which machine-checkable proofs can be verified "beyond reasonable doubt," as New Scientist puts it. The chain is: natural-language proof, formal translation into Lean, then expert review and peer evaluation.
OpenAI's release breaks at several points in this chain:
- According to TechCrunch, only 10 of 719 manuscripts included the model's chain of thought — that is, the actual reasoning the machine performed.
- 42 percent of the proofs had not undergone Lean formalization at all.
- Number theorist Kevin Buzzard at Imperial College London told New Scientist that the release contained 30 articles relevant to his field, but that only seven seemed impressive, and only one was formally verified in Lean. The remaining, unformalized results must, according to Buzzard, wait for expert checking.
A separate problem is documented by researchers at the University of Cambridge and King's College London in an article titled "lost in translation": at least two discrepancies between the natural-language proof and the Lean code behind OpenAI's Navier–Stokes-derived solution. Their conclusion is that such autoformalized proofs should not be trusted without peer review. It is worth noting: the discrepancies do not disprove the solutions, but they show that the translation from a linguistic argument to machine-checkable code can itself be error-prone.
The Advisory Group That Asked for Exactly What OpenAI Did
OpenAI said it had consulted an advisory group of elite mathematicians — AGMAI, a nine-member group affiliated with the Institute for Advanced Study — to avoid the controversy from the Navier–Stokes release. The group issued guidelines at the end of September 2026. According to TechCrunch, the group's first request was to "stop testing advanced mathematical problems on proprietary models." OpenAI's release explicitly states that the company evaluates its proprietary models on open research problems in mathematics — that is, exactly what the group asked it not to do.
In addition, 25 winners of the Fields Medal, mathematics' most prestigious prize, have written an open letter warning against turning research problems into benchmarks for demonstrating model power. The argument is that "mass production" of solutions gives the field no time to engage deeply with the ideas or to attribute prior work.
The Missing Level of Human Understanding
Terence Tao, one of the world's most influential mathematicians and a repeated OpenAI critic, wrote after the release on social media that problems are being solved autonomously by "AI prompters who are not interested in the broader field itself once the original goal is 'solved,' and who do not understand the AI results well enough to answer questions about the result, give talks, or otherwise interact with the rest of the community," as TechCrunch reports.
Harvard professor of mathematics Melanie Wood put it to TechCrunch this way: there is "no human understanding of them at the time of publication, and now the work begins." The point is not that the results are necessarily wrong — but that mathematics as an intellectual tradition rests on someone actually understanding and being able to explain a proof, not just on the hardware having produced a text.
What Remains Unresolved
Several factors mean that neither OpenAI's nor doubleAI's results can be treated as established mathematics:
- None of the proofs has been independently verified. Lean formalization is missing for 42 percent of the manuscripts, and even where it exists, the Cambridge/King's College findings have shown that it can deviate from the natural-language proof.
- OpenAI has not named the model, only described it as an internal frontier model, which makes independent reproduction of the results harder.
- doubleAI's claims about the longest path problem — the cost of under $2,000, the constant improvement from 4/3 to 1.6, and 38 years of unsolved status — rest exclusively on Shashua's post on X, as Globes has reported, and have no primary source documentation in the coverage base.
- OpenAI's comparison of compute costs — on average around three hours of ChatGPT Pro per solution in the new release, versus 10,000 agents and millions of dollars for Navier–Stokes — is a company claim reported via Globes, not an independent finding.
It should also be said that all knowledge of this matter in this report comes from secondary coverage — TechCrunch, New Scientist, Globes, and The New York Times — without OpenAI's database, the AGMAI guidelines, the Fields letter, or Shashua's post being directly available for verification.
What It Will Take for This to Count as Mathematics
It is tempting to read this story as a battle between fast AI and slow academia. But the criticism from the field is more precise: mathematics does not distinguish between finding an argument and certifying it. Lean formalization without discrepancies, named models, published chains of reasoning, and release practices that give the field time to digest and credit work — these are the criteria that Buzzard, Wood, Tao, the Fields Medalists, and AGMAI point to in practice. Until some of them are met, the most accurate statement is that OpenAI has published hundreds of claims, not hundreds of proofs.