722 OpenAI Math Papers, 300 Results Formalized, No Referee's Verdict Yet

If you have seen one number about OpenAI's new math papers, it is probably 42%, which at least one headline presented as the share that cleared Lean checks. That is not what it measures. It counts results that have a machine-checkable proof attached at all, and nothing in the other 58% has failed. Most of it simply has not been tested yet.

On Tuesday, Oct. 6, 2026, OpenAI posted a public GitHub repository, openai/math, holding 722 manuscripts "produced by an internal OpenAI model" that the company has not released. They are grouped into 372 "families" of related results across 17 subjects. By the next day three manuscripts had been withdrawn and 14 revised, and the catalogue now lists 719. Those 719 papers are not one claim but three tiers of confidence, flattened by most headlines into one.

The 42% comes from the repository's change log, which states it as a sum: "This brings the total percentage of top-line results formalized to 300 / 719 = ~42%."

Flip it around: by OpenAI's own count, 419 top-line results have no formalization. The README concedes that "Some of the unformalized results could have issues," and an OpenAI spokesperson told Retraction Watch that roughly 50% of the results were released unconfirmed. Nothing flunked. More than half the work is, for now, preprints in all but name.

A Lean file checks the statement it was given

There are three levels of "checked" here. The first is the manuscript: a proof in ordinary mathematical prose, unrefereed. Fluent is not the same as correct.

The second is Lean, a programming language for proofs, in which software checks every logical step with no room for a hand-waved "clearly." Anyone who has watched a chatbot botch a simple mechanical task knows why a checker that cannot be persuaded is worth a lot.

But Lean only certifies the statement someone typed in, which may be narrower than the paper's claim. OpenAI's own scope notes say so. For a paper on the irrationality exponent of pi, the note reads: "The paper's convergence consequence for the Flint–Hills series is outside this selected statement." Its checking instructions, built around a tool called Comparator, warn that some setups "verify supporting results, not the corresponding papers' main theorems."

Thomas Bloom, who runs erdosproblems.com, found the same gap. On Problem 3 (arithmetic progressions, a 198-page PDF), the Lean challenge file "has only the statement of Erdős' conjecture … and not the stronger quantitative bound claimed above. The actual Lean code appears to prove the weaker bound." On Problem 120, the Erdős similarity problem, the proof was formalised only "in the special case when q=1/2."

The catalogue file, lean/formalization.yaml, labels its scope "Partial progress.", its automation method "agent" and its review status "unchecked." Machine-made, in other words, and unreviewed by humans. A preprint on arXiv that has not been peer reviewed, by Alexander Bastounis, Fabian Circelli and Anders C. Hansen, argues that "Lean verification of AI autoformalisation does not guarantee correct natural language proofs." Their example is OpenAI's earlier Navier-Stokes proof, where "the formalised Lean proof does not correspond to the NL proof," NL meaning the natural-language paper.

The third level, human refereeing, is what journals and the Erdős database ultimately rely on. It has barely begun.

One sign, three papers

The withdrawals show how fragile the first tier is. The trouble began in "Algebraicity of Weil classes on split abelian eightfolds." According to OpenAI's withdrawal notice, the proof gave each "reverse stabilization trace" a sign of +1 when the correct sign is −1. A count the argument needed to be zero came out as "−2m ≠ 0." The Eliashberg–Murphy theorem it invoked "requires zero signed double-point count, so its hypothesis is not met."

One flipped sign, in other words, meant a theorem the proof relied on did not apply. Two papers built on the same construction fell with it: "Algebraicity of Kuga–Satake Correspondences for K3 Surfaces" and "The rational Hodge conjecture for products of K3 surfaces." Each notice adds that "This withdrawal concerns the proof; it does not assert that the mathematical statement is false." The pre-withdrawal PDFs remain archived.

Family 032, in algebraic and complex geometry, launched as "The rational Hodge conjecture for CM abelian varieties and products of K3 surfaces." Its title now ends at "CM abelian varieties," and the sentence about K3 surfaces is gone. Family 032 has no Lean scope note.

OpenAI also revised 14 other manuscripts with "proof repairs, corrected statements, clearer hypotheses and dependencies," among them six on Kähler minimal model programs. That makes 17 of the original 722 papers withdrawn or substantively revised within about a day, and 13 more were updated to cite the revised editions. Research lead Dan Roberts announced the update on X, with his own tally of 19 modifications.

We've updated our GitHub math repo with 6 new Lean formalizations, 19 modifications, and 3 withdrawals. The repo now has ~42% top-line results formalized. We will continue to update the repo with new formalizations and with any errata we notice.

— Dan Roberts (@danintheory) October 8, 2026

Alex Townsend, an associate professor of mathematics at Cornell University, told Retraction Watch the cascade did not surprise him and that he suspects more errors will surface. His objection is about order, not effort:

"Given the skepticism of AI in the mathematics community, I think that OpenAI should have announced the manuscripts that were lean verified first. They could have made a separate announcement for the other ones and ask for help verifying them. This would have been more clear to the community and general public."

Alex Townsend, associate professor of mathematics, Cornell University

A release sorted by confidence tells readers where to look. A single undifferentiated one treats every paper as the same kind of object.

Combinatorics is checked; algebraic geometry mostly isn't

They are not, and the difference tracks the subject. A Daybreak Wire count of the repository's per-family Lean notes finds them for 242 of 372 families, or 65.1%. It counts any Lean work, partial ones included, so it maps where checking effort went rather than measuring correctness, and it differs from OpenAI's 300 of 719.

Where OpenAI's math has Lean checking, by field

Combinatorics and theoretical computer science together have notes for 67 of 77 families, about nine in 10. Algebraic geometry and topology have 11 of 54, about one in five.

The first cascade of errors landed in an unformalized algebraic-geometry family, in almost the least-covered field. That is an observation, not proof Lean would have caught the sign. But a reader should weigh an algebraic-geometry claim here differently from a combinatorics one.

The Erdős problems sit at the well-checked end. Bloom's Oct. 8 post, updated on Oct. 9, says the repository makes "significant claims relevant to 25 Erdős problems," up from 23 after a reader flagged one he had missed and he found another himself. Of those, "21 out of the 25 proofs have been formalised in Lean," which is 84%, about double the repository-wide rate. The PDFs total 1,347 pages, about 54 per problem. Four are unformalized, per Bloom's problem-by-problem list:

• Problem 172, Hindman's conjecture.
• Problem 181, the Ramsey number of the hypercube, with a 172-page PDF.
• Problem 821, on totient values.
• Problem 1083, distinct distances in higher dimensions, at 103 pages.

Bloom says he has "not yet looked at in any serious way any of the proofs" or checked that the formalisations compile. As of Oct. 9, his site's page for Problem 181 still describes Tikhomirov's bound as "the current best bound." Still, he is bullish:

"These papers are, at a glance, very poorly written, in the usual AI fashion. I expect that the vast majority of them are (a) correct yet (b) capable of being substantially simplified and improved given expert attention."

Thomas Bloom, erdosproblems.com

And even so, he wrote, "none of these should be viewed as 'closing the problem', in that people do not need to work on it anymore." That is how to hear "solved" in any headline here: a model says it has a proof, which would settle the question if correct. Melissa Lee of Monash University wrote in The Conversation that some papers claim advances on the Riemann hypothesis and the Birch–Swinnerton-Dyer conjecture, each a US$1 million Millennium Prize problem, and that not all formalisations are implemented correctly.

The anger in mathematics predates this release. On Sept. 8, OpenAI announced a claimed Navier-Stokes result, and Tristan Buckmaster of NYU and Levent Alpöge alleged it had used their ideas, which OpenAI denied. On Sept. 11, Fields medalists published "A Severe Misalignment of AI in Mathematics," warning that "the push by AI companies to solve mathematical problems as a benchmark is detrimental to the science of mathematics." It launched with 25 names and now lists 28, including Terence Tao.

On Sept. 29, a week before the release, the Advisory Group on Mathematics and Artificial Intelligence, hosted at the Institute for Advanced Study, published the advisory group's release guidelines. They ask that results go to repositories "not controlled by any AI lab," that "As far as possible, a proof released by an AI lab should be formalized" or else have its formalization status "clearly stated," and that labs disclose how many problems models "tried and failed to solve."

OpenAI's record against that is mixed. The papers went to its own GitHub repository, though it says it is "continuing to explore other community-hosted alternatives." The formalization rate was stated precisely only on day two. It did say the model "was posed approximately 4,000 problems," roughly one result family per 11 attempts, though the two do not map one to one. The group, which OpenAI consulted, stressed its role was not "an endorsement," and added:

"This release is the beginning, not the completion, of the process of human understanding and the incorporation of the work into mathematical knowledge."

Advisory Group on Mathematics and Artificial Intelligence, Oct. 6 statement

A group calling itself the Association for Human Mathematics was blunter on Oct. 7: "Mathematicians did not ask for this work to be done."

"Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. We urge mathematicians to discontinue their work with OpenAI and to return to a vision of science that centers human understanding."

Association for Human Mathematics, statement

Dan Litt, a mathematics professor at the University of Toronto, told Fortune, "My view is that this is great for mathematics," while warning that extracting understanding will take "a huge amount of human labor." Both camps agree somebody has to do the reading.

To judge a single claim yourself:

• Find the paper's family and check for a Lean scope note.
• Read whether that note covers the main theorem or only a "selected statement."
• Check history.md for revisions or withdrawals of the paper or anything it depends on.
• For Erdős problems, compare Bloom's note with the problem's page on erdosproblems.com.

Each withdrawal notice says the withdrawal "does not assert that the mathematical statement is false." That sentence was written for three papers, but it describes hundreds: claims neither confirmed nor refuted, waiting for a reader. And the people expected to do that reading are the ones saying they never asked for the work.