AI turned out 722 math manuscripts at once. Now the scarce resource is mathematicians to read them

On October 6, 2026, OpenAI published “Sharing AI progress in mathematics” on its official blog. At the same time, it posted 722 math manuscripts written by an unreleased internal model to its GitHub repository. The next day, OpenAI withdrew 3 of them. That day's change log says 719 manuscripts remained after the withdrawals. About 42% of those had proofs confirmed by Lean, a proof-checking program. For the rest, the only way to know whether they are right is for mathematicians to read them. openai +2

OpenAI gave its model about 4,000 research problems and released the results as 722 manuscripts at once

According to the repository README, most of the results came from one shared process run on an unreleased internal model. During the evaluation period, OpenAI gave the model about 4,000 research problems and organized the results into 372 groups. The 372 is the number of problems that produced results. One result can come with several manuscripts, which is how the count reached 722. The only selection criterion in the README is a single line saying it required an appropriate level of significance. The README does not say how many of the 4,000 problems failed or exactly how the 372 were chosen. OpenAI said the compute spent per result was, on average, about what ChatGPT Pro uses when it thinks for 3 hours. github +1

OpenAI described the work as part of model evaluation. Its models now solve almost all existing math test problems, so it widened the evaluation to research problems with no known answer. Along with the manuscripts, it released some Lean formalizations, 10 summaries of the model's reasoning, compute estimates, and statistics on how many problems were attempted. github +1

Not every result followed this process. The README says the work on a zero-free region for the Riemann zeta function and the proof of the Hodge conjecture for CM abelian varieties came from outside it. It also says the Re(s) > 11/12 zero-free region manuscript was edited to be easier for people to read. The announcement doubles as a showcase for a model OpenAI has not yet released. The blog says the company intends to “responsibly release” it. github +1

A day after release, OpenAI withdrew 3 manuscripts over a calculation error and separately fixed the proofs in 14 others

The October 7 entry in the repository's change log (history.md) lists 3 withdrawals, 14 proof revisions, 13 citation-only updates, and 6 new formalizations. Retraction Watch also reported that the withdrawals came the day after release. The withdrawal notice itself, however, dates the withdrawal October 6, one day off from the change log. github +2

The withdrawals started with a manuscript titled “Algebraicity of Weil classes on split abelian eightfolds.” According to the withdrawal notice, the proof assigned a sign of +1 at one computational step when the actual sign was −1. With that single sign flipped, a value that should have been 0 came out nonzero (−2m). The theorem the proof relied on (the Eliashberg–Murphy vanishing theorem) then no longer applied. Two K3 surface manuscripts that borrowed this manuscript's construction were withdrawn along with it. The notice ends by stating that the withdrawal concerns the proof and does not mean the statement is false. It keeps a wrong proof and a wrong statement clearly apart. github +1

The 14 proof revisions have a different cause from this sign error. The change log says they were made for separate reasons, such as repairing proofs and correcting statements. github

As for who found the error first, the only confirmed account is an OpenAI spokesperson telling Retraction Watch it was found during an “audit”. Research lead Dan Roberts summed it up on X as “6 new Lean formalizations, 19 modifications, and 3 withdrawals.” The public explanations do not say how those 19 modifications map onto the change log's 14 proof revisions and 13 citation updates. Still, because the company logged its own corrections by date, outsiders can trace what changed. retractionwatch +1

Of the 719 manuscripts left, software has checked the proofs in 42%. Mathematicians must read the other 58% themselves

The change log reads “300 / 719 = ~42%.” That means 300 of the 719 manuscripts left after the withdrawals have proofs formalized in Lean. With Lean, you rewrite a proof as code a computer can read, and the program checks that each step follows logically. The 42% figure comes after the 6 formalizations added the day after release. On launch day, the README said only that formalizations existed for “Many, but not all” results, with no percentage. github +1

The remaining 58% or so have no machine verification. The README itself says, “Some of the unformalized results could have issues”. A spokesperson told Retraction Watch that “roughly 50%” of the results were released unverified. That does not match the 58% calculated from the repository's own numbers. This article goes by the repository's numbers. github +1

Opinions also split on whether OpenAI should have published before formalization was done. The spokesperson said AGMAI, an independent advisory group at IAS, had advised releasing without waiting for full formalization. Recommendation 4 of AGMAI's guidance says that if formalization would cause unacceptable delay, the formalization status should be stated clearly. But the first paragraph of the same guidance says AGMAI does not endorse AI labs testing advanced math problems on internal models, and it recommends posting results to repositories that AI labs do not control. OpenAI posted the manuscripts to its own GitHub and wrote on its blog that it is considering community-run alternatives. Cornell's Alex Townsend said OpenAI should have published the Lean-verified manuscripts first, then released the rest separately and asked for help checking them. retractionwatch +2

A separate case has raised doubts about whether Lean verification guarantees a manuscript's proof as written. Anders Hansen of Cambridge and two co-authors argue that in the Navier-Stokes proof OpenAI released in a separate repository in September, the Lean code proves a different, weaker statement than the natural-language proof. Their example: the natural-language proof works with m+4 derivatives, while the Lean code works with m+5. Their paper does not analyze the 719 manuscripts in this release. On Hacker News, others pushed back. They said the definitions used to state the final result in Lean were written by people in advance, so the final statement holds and the mismatch is only in intermediate steps. The debate is ongoing. Either way, what the program checks is the statement written in Lean. Whether that statement says the same thing as the manuscript's text is still for a person to confirm. arxiv

Mathematicians say checking these manuscripts one by one is a burden big enough to halt their own research

Hansen told New Scientist that every one of these proofs generated by large language models has to be read by a person, and that this puts an enormous extra burden on mathematicians. newscientist

Set theorist Asaf Karagila keeps a “problems” page on a personal blog, promising a bottle of whisky to anyone who solves the Partition Principle problem. Karagila describes the problem as more than 100 years old. When OpenAI announced it had solved it, people asked Karagila whether Sam Altman would be getting the whisky. Karagila's reply: “The answer to that is no”. karagila

“I am trying to finish several papers, I am supervising a number of Ph.D. students, and I have a lot of active research of my own to do. When am I supposed to sift through a badly written paper?” … “But it is the equivalent of a Denial of Service, should we want to take it seriously: stop everything else and figure this one out.” (Asaf Karagila)

Karagila did note not having looked at the Lean code. The criticism was about the quality of the manuscripts' writing, not a claim that the proofs are wrong. Karagila also wrote of not being against using AI as such. karagila

Terence Tao (UCLA) looked at the same burden from the community's side. In the past, a major proof was followed by talks, workshops, and collaborations, and through them many mathematicians came to understand it. But people who solve problems with AI often don't understand the results well enough to answer questions or give talks, so far fewer seminars and collaborations follow, Tao pointed out. mathstodon.xyz

Some critics go further. In an October 7 statement, the Association for Human Mathematics said, “Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power,” and urged mathematicians to stop working with OpenAI. MIT's Andrew Sutherland called the quick withdrawals “the responsible thing to do,” but said it will take much more to win back lost trust. ahmath +1

Even those who welcome the release acknowledge the burden. Dan Litt of the University of Toronto told Fortune “this is great for mathematics.” Litt also said that drawing real understanding out of these results will take an enormous amount of human labor, though that labor is not very different from what mathematicians have always done. In Litt's view, OpenAI does not have enough mathematicians across enough fields to understand every proof. fortune

As AI floods math with results, the scarce resource is shifting from producing proofs to people who read, check, and stand behind them

One number is missing from this release: how long it takes a person to read and check one manuscript. It is not in OpenAI's materials, and it is not in the critics' writing either. The cost of producing the proofs, by contrast, was published: about 4,000 problems, and an average of compute equal to ChatGPT Pro thinking for 3 hours per result. On the checking side, the only published number is the 300 manuscripts checked by software. The other 419 get checked only when mathematicians make the time. github +1

The day after release, 3 manuscripts were withdrawn and the proofs in 14 others were revised. Townsend expects more errors to surface. Pointing to the change log's version notes and archive links to withdrawn versions, one Hacker News user wrote, “This is what it looks like when software engineering practices meet mathematics”. The manuscripts come out first. Checking and fixing follow after publication. github +2

Tao's proposed “Math 2.0” is one answer to this shift. Tao argued that problem-solving should step back from the center of mathematics, and that exposition explaining results, along with community-building, should be valued more. OpenAI, for its part, wrote on its blog that it will fund workshops and conferences going forward. The cost of producing a proof has been published as compute. Reading that proof, finding its errors and withdrawing it, and answering questions about it still have to be paid for with each mathematician's own time. mathstodon.xyz +1

Mathematics used to prize above all the power to solve hard problems and produce proofs. Once AI released 722 manuscripts at once, more than half of what it produced was left waiting for people to read and check it. What mathematics now needs to focus on is reading and verifying proofs, explaining them to other mathematicians, and taking responsibility when errors turn up.

Further reading

openai/math change log OpenAI's dated correction record, listing the 3 withdrawals, 14 proof revisions, 13 citation updates, and the 300/719 formalization rate. github.com

AGMAI guidance: Responsible Release of AI-Generated Mathematics Recommendations the IAS advisory group issued on September 29 on testing with internal models, where to publish, and labeling formalization status. agmai.org

Terence Tao, Math 1.0 vs Math 2.0 Tao's post on why results solved by AI don't lead to talks and collaborations, and what the math community should value more. mathstodon.xyz