Week 1 after the OpenAI math dump: how it's going

On October 6, OpenAI uploaded 722 manuscripts to a GitHub repository, grouped into 372 "result families," all credited to an internal model that nobody outside the company can use. According to the README, the model was posed roughly 4,000 problems and spent, on average, the equivalent of three hours of ChatGPT Pro compute per result. The framing in the press was a new era of discovery.

Here is what the first 48 hours of that era looked like.

The scoreboard after one day

By October 7, the repository's own changelog recorded the following:

• 3 manuscripts withdrawn. A sign error in "Algebraicity of Weil classes on split abelian eightfolds" invalidated a stabilization-trace cancellation argument. Two papers built on that construction went down with it: "Algebraicity of Kuga-Satake Correspondences for K3 Surfaces" and "The rational Hodge conjecture for products of K3 surfaces."
• 14 manuscripts revised with what the changelog calls proof repairs, corrected statements, and clearer hypotheses. This includes four papers on Lipschitz heights and Ashkin-Teller currents, six on Kähler minimal model programs and abundance, and a corrected cone-equality claim in "Taming implies compatibility," which now ships with a strict-inclusion example showing the original claim was too strong.
• 13 more manuscripts updated because they cited papers in the previous group.

That is 30 of 722 manuscripts touched within a day of publication, and the count is now 719. One of the fixes is especially telling: a paper on the Birch-Swinnerton-Dyer formula had to drop a citation to a supporting manuscript that had already been removed before the release went out. The corpus was citing its own deleted scenes.

To be fair, 3 withdrawals out of 722 is under half a percent. But these are the errors found in one day, by a community that had no advance notice and, by most accounts, has not yet read the papers. Scott Aaronson's summary on October 7 was that essentially none of the proofs had been understood by any human yet. An OpenAI spokesperson conceded that this includes many of the company's own mathematicians.

"It's verified in Lean," for some value of "it"

The strongest defense of the release is the Lean formalizations. It deserves a closer look.

OpenAI's figure is that 300 of 719 top-line results, about 42%, are formalized. A count by Decrypt of the launch-day formalization catalogue found 162 of 722 papers with a computer-checked main result, about 22%. The two figures evidently count different things, which is itself a small lesson in how much weight the word "formalized" is being asked to carry.

Either way, most of the release has no machine check at all, and the README says so plainly: "Some of the unformalized results could have issues."

For the formalized portion, a passing Lean check certifies the statement as written in Lean. Whether that statement is the theorem advertised in the abstract is a separate question that humans have to answer. An early third-party review already flagged one case: family 197 (Kaplansky's direct-finiteness conjecture) carries a catalogue headline that includes a torsion-free strengthening, while its Lean scope page describes constructions involving torsion.

One more detail from an outside checker: of the 405 Comparator configurations in the repository, 404 leave the second, independent kernel switched off.

Where do you report a bug?

Nowhere in particular. The repository has GitHub Issues disabled and accepts pull requests from collaborators only. Error reports are therefore scattered across a developer forum thread, blog comment sections, social media, and Hacker News. Corrections appear when OpenAI decides to post them.

This matters because the independent advisory group convened at the Institute for Advanced Study had reportedly recommended, among other things, that results not be hosted in a repository controlled by an AI company. OpenAI says it is "exploring" community-hosted alternatives. In the meantime, the party that produced the proofs also controls the errata.

Credit where due

Not everything is going badly, and a fair accounting should say so.

• An independent rerun of the Lean proof that $\zeta(s) \neq 0$ for $\operatorname{Re}(s) > 7/8$ passed under two kernels using only the three standard axioms. The checker was careful to note that this verifies the Lean proof, not the paper.
• A third party reports extending the claimed bound $\omega \leq 2.25$ for matrix multiplication from $\mathbb{C}$ to arbitrary fields, with a Lean proof in a fork.
• A human audit of the earlier, ten-result August release found no surviving confirmed substantive error in a principal result, though one chapter drew a call for major revision.

So some of this is likely real mathematics. The trouble is that nobody can currently say which parts, and the release was structured so that finding out is everyone else's job.

The pattern

OpenAI has acknowledged that citations, exposition, and presentation need work and has promised to do better in future releases. That is a notable thing to say about 722 papers one has just published.

The asymmetry is the story. Producing each manuscript cost a few hours of compute. Checking each one costs a specialist days or weeks, and there are hundreds of them, spread across most areas of mathematics, written in a style at least one expert in the relevant field has reportedly found close to unreadable. A day-one withdrawal rate that looks small is a lower bound established by people who have barely started.

Week 1 is not over. The changelog will be worth watching.

---

Sources

1. OpenAI, openai/math README, GitHub, accessed October 8, 2026. https://github.com/openai/math
2. OpenAI, openai/math history.md, entry dated October 7, 2026 (withdrawals, fixes, formalization count), accessed October 8, 2026. https://github.com/openai/math/blob/main/history.md
3. OpenAI, "Sharing AI progress in mathematics," October 6, 2026. https://openai.com/index/sharing-ai-progress-in-mathematics/
4. OpenAI Developer Community, "First look at mathematics manuscripts from an internal frontier model at OpenAI," thread opened October 6, 2026; posts by davegoldblatt (October 7, 1:52am) and selanavot (October 7, 1:31pm). https://community.openai.com/t/first-look-at-mathematics-manuscripts-from-an-internal-frontier-model-at-openai/1403886
5. Scott Aaronson, "The Mathocalypse," Shtetl-Optimized, October 7, 2026. https://scottaaronson.blog/?p=10169
6. Decrypt, "OpenAI Says a Secret AI Model Cracked Hundreds of Open Math Problems in One Prompt. Mathematicians Want Receipts," October 2026 (162 of 722 count; Issues disabled). https://decrypt.co/380366/openai-secret-ai-model-cracked-hundreds-math-problems-one-prompt
7. Kingy AI, "OpenAI's 722 Math Manuscripts: The Results, Proofs, Compute and Costs," October 2026 (family 197 scope mismatch). https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/
8. Implicator, "OpenAI's 372 Math Results Leave Mathematicians Racing to Read the Proofs," October 2026 (spokesperson statement). https://www.implicator.ai/openai-372-math-results-mathematicians-race-to-read/
9. BigGo Finance, "OpenAI Releases Batch Solutions to 300+ Math Problems," October 2026 (advisory group recommendations). https://finance.biggo.com/news/e98aab26-4ca6-4afb-9790-66791b865a3e
10. "A Human Audit of OpenAI's AI-Generated Mathematical Proofs," arXiv:2608.14673v3, 2026. https://arxiv.org/html/2608.14673v3