OpenAI's 372 Math Results: What Has Actually Been Verified - Technology Org
OpenAI’s 372 Math Results: What Has Actually Been Verified So Far
Key takeaways
- OpenAI’s 6 October GitHub release now lists 719 manuscripts in 372 result families, after three papers were withdrawn on 7 October over a sign error that broke one proof and two papers built on it.
- As of OpenAI’s 7 October update, 300 of 719 top-line results, about 42%, have Lean formalisations that a computer has checked, and OpenAI warns the unformalised rest could contain errors.
- The 372 families came from roughly 4,000 problems posed to an unreleased internal model, using on average about three hours of ChatGPT Pro-level compute per result.
- Fourteen further manuscripts were revised with proof repairs or corrected statements within a day of release, and a Cornell mathematician told Retraction Watch he expects more errors to emerge.
- The Association for Human Mathematics urged mathematicians to stop working with OpenAI, while the advisory group OpenAI consulted said its role was not an endorsement of the results or the process.
The headline number is the wrong number
Most coverage of OpenAI’s 6 October maths release leads with one of two figures: 722 AI-written papers, or 372 solved problems. Neither describes what the repository holds today. After a correction on 7 October, the openai/math catalogue on GitHub lists 719 manuscripts grouped into 372 families. A family is not a problem. It bundles a main result with companion arguments, consequences or alternative proofs.
The figures that show how much of this is solid get quoted far less. About 42% of top-line results carry a Lean formalisation, meaning a computer has checked the proof step by step. Three manuscripts were withdrawn within a day. Fourteen more were repaired. And the 372 families came out of roughly 4,000 problems the model was given, a denominator that rarely reaches the headlines.
None of that makes the release small. Some prominent researchers have called it historic. But a list of 372 claims is not a list of 372 theorems, and the distance between the two is what this week has been about.
What OpenAI says it released
In its announcement of the maths results, OpenAI said the work came from an internal frontier model and was published with protocols for revisions and citations. The company shared Lean formalisations for many proofs, 10 summaries of the model’s reasoning, compute estimates and statistics on attempted problems. It put the average cost at roughly three hours of ChatGPT Pro thinking per result.
The repository’s own README is more cautious than most headlines about it. It says the results sit at different stages of verification, that not all have Lean versions, and that some unformalised results may have issues. It also flags two exceptions to the standard production method: work on a zero-free region for the Riemann zeta function, and a proof of the Hodge conjecture for CM abelian varieties. One of the Riemann write-ups was edited by humans for readability.
OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence, hosted at the Institute for Advanced Study, on how to publish. It plans to fund workshops and conferences to help researchers understand AI-produced results, and says it is working to release the model itself responsibly.
Day two: one sign error, three withdrawals
The first correction came fast. On 7 October, the repository’s version history recorded that a sign error in a paper on Weil classes on split abelian eightfolds broke a cancellation argument and a construction two other papers relied on. OpenAI withdrew all three, including one claiming the rational Hodge conjecture for products of K3 surfaces.
The same entry lists repairs to 14 other manuscripts, from fixed proofs to corrected statements and clearer hypotheses, plus citation updates in 13 more. Six new formalisations raised the machine-checked share to 300 of 719 top-line results.
Read one way, this is the process working: an error was found, flagged publicly and versioned within a day, and the withdrawn papers stay online with notices explaining the gap. Read another way, a single slip ran through three papers before outside mathematicians had time to read them. Cornell mathematician Alex Townsend told Retraction Watch, which reported the withdrawals, that the cascade did not surprise him and that he suspects more errors will turn up.
What a Lean check proves, and what it doesn’t
Lean is a programming language for writing proofs. If a formal proof compiles, every logical step from the stated assumptions to the stated conclusion has been checked by machine, which is far stronger than one referee’s careful reading. That is why the 42% figure is the most important one in the release.
It still leaves two gaps. The first is translation. Lean confirms the formal statement, not that the formal statement matches what the English paper claims. A theorem formalised with a slightly different hypothesis can pass the check while the headline claim stays unproven. The second is meaning. A machine check says nothing about whether a result is new, significant or genuinely tied to the open problem it is said to settle.
For the remaining 58% of top-line results there is no machine check at all, and human checking has barely started. Complexity theorist Scott Aaronson wrote on 7 October that no human appeared to have understood almost any of the proofs yet. His wife, Dana Moshkovitz, who has worked toward the Unique Games Conjecture for years, messaged him that the claimed proof was “so horribly written that it’s impossible to read it without AI help”. That proof, notably, is one of those with a Lean certificate.
| Figure in coverage | What it actually counts | Source | Status |
|---|---|---|---|
| 722 | Manuscripts published on 6 October | OpenAI repository at launch | Superseded |
| 719 | Manuscripts after three withdrawals | Repository history, 7 October | Current |
| 372 | Result families (groups of related papers), not individual problems | Repository README | Current |
| About 4,000 | Problems posed to the model during evaluation | Repository README | Company figure |
| 300 of 719 (about 42%) | Top-line results with Lean formalisations | Repository history, 7 October | Expected to rise |
| 3 and 14 | Manuscripts withdrawn and manuscripts revised | Repository history, 7 October | May grow |
| About 10% | Success rate on problems attempted, corrected from an earlier 5% | Scott Aaronson’s blog | Outside estimate |
| About 3 hours | Average ChatGPT Pro-equivalent compute per result | OpenAI announcement | Company claim |
The case that this is historic
Aaronson’s post on what he calls the Mathocalypse has become a reference point for the release, and he is no sceptic. He called 6 October one of the biggest days in mathematical history and listed results he said could each be the result of the year in parts of theoretical computer science, including Fourier transform and integer multiplication algorithms faster than n log n and a positive answer to a quantum computing problem he posed in 2007.
His post also shows how quickly numbers drift. He first wrote that the model had been tried on about 8,000 problems with a 5% success rate, then corrected both figures to roughly 4,000 problems and about 10% after readers pointed out the error. Some early summaries of his post still carry the old numbers. Even the corrected rate needs care, because the 372 families do not map one to one onto the problems attempted.
Others shared the sense of scale. The Decoder, collecting researchers’ reactions, quoted Alvaro Lozano-Robledo calling it possibly the most important day in the history of mathematics so far, while he also pointed to the model’s limits. The publication noted that OpenAI had aimed at the Riemann Hypothesis itself and reached only a weaker variant.
The case against: process, not just proofs
The sharpest criticism targets how the work was released. On 7 October the Association for Human Mathematics published a statement condemning the release as a show of power rather than scholarship and urged mathematicians to stop working with OpenAI. Terence Tao reshared it, which gave it wide reach, though reports differ on how far that amounts to an endorsement and he is not its author.
The association leaned on the very advisory group OpenAI says it consulted, pointing to that group’s earlier guidance that frontier AI companies should not test advanced mathematical problems on internal models. The advisory group’s own response to OpenAI’s release was carefully neutral. It said its role should not be read as a verdict on the results or as approval of how OpenAI obtained them, reaffirmed its recommendations, and left it to mathematicians to judge whether they had been followed.
Aaronson pushed back on the boycott call. He argued that open problems are there for anyone to attempt, including a company, and that the association’s members speak for themselves rather than the whole field, while still urging the maths community to keep pressure on AI firms to behave better. Futurism summed up a wider grievance among critics: the expectation that mathematicians will now do the slow work of unpacking and verifying hundreds of dense, partly unreadable manuscripts they never asked for.
The release also follows a contested September claim. OpenAI said on 8 September that an internal model had shown the three-dimensional Navier-Stokes equations can blow up in finite time. The Clay Mathematics Institute has not accepted that result, and the construction relies on a smooth external force, a case most specialists treat as separate from the version of the problem they care about.
How to read the next headline
For readers, the practical rule is simple. Treat each item in the repository as a preprint claim, not an established theorem. A Lean certificate is strong evidence that a formal statement is true, but someone still has to confirm that it is the statement being advertised. The repository’s history file is the place to watch, since OpenAI has committed to keeping every version and logging corrections there.
The bigger change is economic. Producing candidate proofs has become cheap, at about three hours of compute each by OpenAI’s account. Checking them has not. Until the model is released and outsiders can reproduce its output, or until referees work through the manuscripts one by one, the verified share of this release is the 42% a computer has checked, minus whatever the translation step gets wrong, plus whatever humans manage to confirm. That figure will move every week. The 372 will not.
