On October 6, 2026, OpenAI posted 722 mathematical manuscripts to github.com/openai/math. It describes them as produced by "an unreleased internal OpenAI model" and grouped into 372 result families covering problems such as the Unique Games Conjecture, cases of the Hodge conjecture, Birch–Swinnerton-Dyer and the irrationality exponent of π. A day later OpenAI withdrew three papers and repaired 14, which leaves 719 in the current CONTENTS.md. The release came a month after OpenAI's disputed September Navier-Stokes announcement. It drew a boycott call from the Association for Human Mathematics and an unusually fast public review effort.
This matters to builders because it is the largest public test so far of AI-generated research at scale, and of the verification stack around it. The question is what a builder can actually trust: a GitHub listing, a Lean certificate, or an expert's reading. The newsroom's question was what independent mathematicians conclude about specific manuscripts. Two weeks in, the answer is that only a handful of manuscripts have been examined in depth, and those checks have found both serious advances and concrete errors.
What we checked
- What do independent mathematicians conclude after examining specific manuscripts and their proofs? partly confirmed. Verdicts on individual manuscripts exist but are few and mixed. Dana Moshkovitz says the Unique Games proof holds up but is poorly written. A sign error led to three Hodge-related papers being withdrawn. Experts found the tiling and black-hole papers either novel but unpublishable, or too vague to check. An arXiv paper shows the Lean code for the Navier-Stokes claim proves weaker inequalities than the written proof. No systematic review of the collection exists. [5][3][7][6][4]
- Does the repository itself establish that the manuscripts solve or advance major open problems? refuted. The README describes the material as 'results at different stages of verification' and warns that 'Some of the unformalized results could have issues.' It reports that about 42% of top-line results are formalized in Lean (300 of 719, according to history.md). A listing in the repository is a claim, not proof that a problem has been solved. [1][3][2]
- Does a Lean formalization settle correctness of the corresponding manuscript claim? refuted. Bastounis, Circelli and Hansen show that the Lean code for the Navier-Stokes claim does not match the natural-language proof. Johan Commelin says some formalizations appear to prove weaker statements than the papers claim. A passing Lean check verifies only the statement as written in Lean. [6][7][8]
What we found
- OpenAI makes only limited claims about its own verification. The README says the collection contains 'results at different stages of verification,' that roughly 42% of top-line results are formalized, and that 'Some of the unformalized results could have issues.' The model was posed about 4,000 problems, at an average of about three hours of ChatGPT Pro thinking compute per result. Reasoning summaries were released for only 10 results. [1][2]
- OpenAI's own changelog records a cascading error. On October 7 it withdrew three manuscripts, including 'The rational Hodge conjecture for products of K3 surfaces,' because a sign error invalidated a cancellation argument and a construction that two dependent papers relied on. It repaired 14 more, including one on a Birch–Swinnerton-Dyer formula, and states that 300 of 719 top-line results are now formalized. A spokesperson told Retraction Watch that roughly 50% of results were released unconfirmed on the advice of its advisory group. [3][4]
- The most positive manuscript-level verdict so far is on the Unique Games proof. Dana Moshkovitz, a leading researcher on the conjecture, wrote in a comment on Scott Aaronson's blog that 'The Unique Games Conjecture is true,' while calling the writeup poorly written. Aaronson also wrote that 'no human has understood just about any of these proofs yet.' [5]
- Lean certificates are not the same as correct papers. Bastounis, Circelli and Hansen (arXiv:2610.08144) argue that autoformalization can mistranslate a proof, and they show that the Lean code for OpenAI's Navier-Stokes claim does not match its natural-language proof. Quanta quotes Mathlib's Johan Commelin as saying that some formalizations appear to prove weaker statements than the papers claim, though he had not confirmed this himself. [6][7]
- Assessments in other fields are mixed. According to Quanta, Chaim Goodman-Strauss found novel ideas in a 3D aperiodic tile paper but said it was far from publishable form. Mihalis Dafermos called several black-hole papers too vague to check, and Daniel Litt suggested treating the papers as 'raw data.' Jeremy Avigad said the release 'includes major advances.' [7]
- Public review is hard to do through the repository itself. Decrypt reports that the repo has Issues turned off and has never accepted a pull request, and that OpenAI published no prompts. That falls short of the IAS advisory group's September 29 recommendation to disclose prompts, model name and compute for every result. Decrypt also reports that only 162 of 722 papers have a Lean-formalized main result. That is a different unit from OpenAI's 42% of top-line results, and the gap shows how much the coverage figure depends on what is counted. [8]
- Earlier OpenAI math claims show how slow and partial auditing is. A human audit of ten results OpenAI announced on August 1 (arXiv:2608.14673) found no confirmed substantive error in a principal result. But review depth varied, one chapter drew a request for major revision, and the authors stopped short of a full reconstruction of the proofs. [9]
What it means
Treat openai/math as a large set of strong but unrefereed candidate results, not as 372 solved problems. For any result you want to rely on, whether to cite it, build on it or use it as a benchmark, check three things separately. First, does it have a Lean artifact? Second, does a human confirm that the Lean statement matches the claimed theorem, rather than a weaker version? Third, has a named domain expert reconstructed the argument? So far only a few results, such as the Unique Games proof, have reached the third stage. Also track history.md, because results that depend on other results can fail together, as the three Hodge-related papers did.
For teams building AI-for-math or automated-research systems, the lesson is about engineering. Checking that a formal statement matches the claimed theorem is now the bottleneck, more than proof search itself. Ship formal statements alongside readable specifications, record which results depend on which, publish prompts and compute per result, and open a channel for errata. OpenAI's release shows that producing hundreds of plausible results is now possible. Its corrections show that without those controls, a large release spreads errors faster than reviewers can find them.
Still open
- How many of the roughly 419 unformalized top-line results will survive expert review, and how many more withdrawals will follow?
- How many existing Lean formalizations prove weaker statements than their manuscripts claim? No systematic audit has been published.
- Will OpenAI release prompts, per-result compute and the model, as the IAS advisory group recommended, so the results can be independently reproduced?
- Do the remaining Hodge results, including the CM abelian varieties claim, and the π irrationality-exponent claim withstand specialist scrutiny?