OpenAI AI Math: 3 Papers Withdrawn, ~42% of Results in Lean

TL;DR

• On Oct. 6, 2026, OpenAI published a GitHub repository of mathematical manuscripts produced by an unreleased internal model; its release-day README listed 722 manuscripts in 372 families, a count Retraction Watch also reported. The repository now lists 719.
• The repository’s history entry dated Oct. 7 lists three withdrawn manuscripts: a sign error broke a key step in one paper, and two others depended on its construction. Fourteen more were revised (proof repairs, corrected statements, one citation fix). OpenAI’s notice says the withdrawal concerns the proof, not whether the statement itself is false.
• About 42% of the top-line results (300 of 719) have Lean formalizations, per the same log. Set against the independent IAS advisory group’s Sept. 29 recommendations, the release includes reasoning summaries, average compute and the number of problems tried; the post and README do not name the model, and prompts appear only as excerpts in 8 of the 10 reasoning summaries.

What happened

OpenAI’s post “Sharing AI progress in mathematics,” dated Oct. 6, announced a wide set of new results “produced by an internal frontier model” and pointed readers to a GitHub repository, openai/math. GitHub’s metadata shows the repository was created at 21:47 UTC that day. OpenAI says it consulted the independent Advisory Group on Mathematics and Artificial Intelligence (AGMAI) at the Institute for Advanced Study and drew on its public recommendations for the release.

The repository’s README says the catalog now groups 719 manuscripts into 372 families; a family may include a principal result, companion arguments, consequences or alternative proofs. It says the model was posed roughly 4,000 problems over the evaluation, and that the average result took about three hours of ChatGPT Pro thinking compute on that model. Exceptions to that fixed procedure include a zero-free region for the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties. One writeup, the Re(s) > 11/12 zero-free region, was edited by people for readability.

According to Retraction Watch, OpenAI announced the withdrawal of three manuscripts on Oct. 7.

What the repository shows

1. The withdrawal log. The repository keeps a dated history file. Its entry dated Oct. 7 says a sign error in “Algebraicity of Weil classes on split abelian eightfolds” invalidates a stabilization-trace cancellation argument, and with it the construction two other papers relied on. All three were withdrawn; their notices are dated Oct. 6, and the change reached the public repository in a pull request merged at 05:20 UTC on Oct. 8 (10:20 p.m. Oct. 7, Pacific time):

• The paper with the error: Algebraicity of Weil classes on split abelian eightfolds
• A dependent paper: Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
• A second dependent paper: The rational Hodge conjecture for products of K3 surfaces

2. What the error was. The withdrawal notice in the first paper’s folder explains it. The proof gave each “reverse stabilization trace” a sign of +1, so adding m of them seemed to bring a signed double-point count of −m to zero. With the orientations accounted for, each trace counts −1, and the total becomes −2m, not zero. A cancellation theorem the proof invokes at that step (attributed to Eliashberg and Murphy) needs a count of exactly zero, so the notice says the oriented-surgery and embedded-brane construction that follows is unsupported, and the paper does not establish its claimed algebraicity theorem. The notice adds that the withdrawal “does not assert that the mathematical statement is false,” and links an archived copy of the pre-withdrawal PDF.

3. The other fixes. The same entry lists 14 manuscripts revised with proof repairs, corrected statements, clearer hypotheses and dependencies, and one fix to an obsolete citation. They span four topic groups (Lipschitz heights and Ashkin–Teller currents, Kähler minimal model programs, taming and hypersymplectic deformation, and incompressible box transport) plus a citation change in an exact Birch–Swinnerton-Dyer paper. Another 13 manuscripts were updated to cite the revised editions of companion papers, changing references and version dates. OpenAI also added 6 formalizations and 5 supporting additions, which the log says brings formalized top-line results to 300 of 719, about 42%; the release-day README gave no percentage. The pull request that pushed the update notes that Lean builds were not run for that synchronization. The README warns that “some of the unformalized results could have issues.”

4. OpenAI’s comment. A spokesperson told Retraction Watch that the company found the errors during an audit and that the company will work to correct errors promptly and “withdraw papers if no fixes can be found.” The spokesperson also said AGMAI had advised against holding the release until “full formalization,” and, in Retraction Watch’s account, that roughly 50% of results went out unconfirmed; that figure and the repository’s 42% formalization share are not described on the same basis.

The release against the advisory group’s checklist

AGMAI published “Responsible Release of AI-Generated Mathematics” on Sept. 29. For results that people do not yet understand, it asks labs to take a set of steps at release and afterward. The table puts selected steps next to what OpenAI’s post and repository say. It records what the documents state; it is not a judgment of whether a recommendation was met.

AGMAI recommendation (Sept. 29)	What OpenAI’s post and repository state
Deposit results in a repository the lab does not control, with persistent identifiers	Results are in OpenAI’s own GitHub repository; OpenAI says it is “continuing to explore other community-hosted alternatives”
Publish the model’s name	The model is described only as an unreleased internal model
Publish the prompts used	No prompts in the post or README; 8 of the 10 reasoning summaries include a section of “Original prompt (excerpts)“
Publish a summarized chain of thought	Abridged reasoning summaries for 10 result families
Publish time taken and estimated cost	An average: about three hours of ChatGPT Pro thinking compute per result
Formalize proofs as far as possible, or state their formalization status	Lean formalizations for 300 of 719 top-line results (about 42%)
Say how many comparable problems failed	Roughly 4,000 problems posed over the evaluation
Explain how exactly AI came to be used	The README describes one fixed procedure for most results and names exceptions
Search the literature and cite related prior work	OpenAI says that for future releases it will improve the papers’ citations and exposition
Fund human understanding through nonprofit institutions	OpenAI says it will fund workshops, conferences and special programs, with details to come

AGMAI’s own statement on Oct. 6 said its advisory role is neither a verdict on the results’ impact nor “an endorsement of the process” OpenAI used. It called the release “the beginning, not the completion” of the work of human understanding, and said it is up to the mathematical community to judge how far the recommendations were followed.

Background

This release follows OpenAI’s Sept. 8 post proposing a solution to the Navier–Stokes problem, one of the Clay Mathematics Institute’s seven Millennium Prize problems. According to Fortune, OpenAI said the new batch includes progress, but not full solutions, on three more of the Millennium Prize problems. Retraction Watch reports that more than 8,000 researchers endorsed a group’s concerns about how the Navier–Stokes announcement was handled, including a lack of time for “a proper writeup” and for citing earlier work.

Reactions to the release and the withdrawals were mixed. Andrew Sutherland of MIT told Retraction Watch that acting quickly was “the responsible thing to do,” while adding that regaining trust “will take a lot more than that.” Alex Townsend of Cornell told Retraction Watch that OpenAI should have first announced “the manuscripts that were lean verified” and asked for help checking the rest. On Oct. 6, the day of the release, Terence Tao of UCLA argued in a Mastodon post quoted by Fortune that problems are being solved by “AI prompters” who do not understand the output well enough to engage with the field.

For OpenAI’s other recent releases, see our report on GPT-6 in free ChatGPT and its system card and our DevDay 2026 roundup. More AI coverage is in AI & Semiconductors.

What could go right

• The repository records changes in public: the README says corrections are recorded as new versions, with earlier versions kept accessible, and the withdrawn papers link to their archived originals.
• OpenAI says it will keep adding Lean formalizations; the Oct. 7 update added 6, and the README now states about 42% (the release-day README gave no percentage).
• OpenAI says it will fund workshops, conferences and special programs on understanding AI-produced results.

What could go wrong

• The README itself says unformalized results “could have issues,” and Townsend told Retraction Watch he suspects more errors will be found.
• The producing model is unreleased. OpenAI’s post says it is “working to responsibly release” it, and AGMAI said equitable access to powerful research tools is “essential” to mathematicians’ freedom to pursue their own questions.
• Dependencies between papers can spread an error: one sign took two other manuscripts with it, and fixes to 14 other papers forced citation updates in 13 more.

FAQ

Q Why did OpenAI withdraw three math papers?

A A sign error in "Algebraicity of Weil classes on split abelian eightfolds" broke a cancellation step in its proof, and two other papers relied on that construction. The repository's history entry dated Oct. 7, 2026, lists the three withdrawals (the notices themselves are dated Oct. 6), and OpenAI says the withdrawal concerns the proofs, not whether the statements are false.

Q How many of OpenAI's AI math results have Lean formalizations?

A The repository's Oct. 7 history entry puts it at 300 of 719 top-line results, about 42%, formalized in the Lean proof language. The repository's formalization manifest lists its review status as "unchecked," and the pull request that added the latest formalizations says Lean builds were not run for that update.

Q Which model produced OpenAI's math results?

A OpenAI's post and README describe it only as an unreleased internal frontier model. The README says each result used about three hours of ChatGPT Pro thinking compute on average.

Q What is AGMAI?

A The Advisory Group on Mathematics and Artificial Intelligence, based at the Institute for Advanced Study, published recommendations for releasing AI-generated mathematics on Sept. 29, 2026. It said on Oct. 6 that its advisory role is not an endorsement of how OpenAI obtained its results.