# OpenAI Withdraws Three of 722 AI-Written Math Papers as Mathematicians' Group Urges Boycott

A sign error invalidated one proof and the two papers that depended on it, and Lean formalizations so far cover the main result of only 162 of the 722 manuscripts.

- Published: 2026-10-09T06:20:56.057Z
- Canonical: https://polylog.news/ai/2026-10-09/openai-withdraws-three-of-722-ai-written-math-papers-as-math
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [Polylog editors](https://polylog.news)

On October 6, OpenAI [published 722 manuscripts](https://tech.yahoo.com/ai/chatgpt/articles/openai-drops-722-ai-math-171537220.html) on GitHub. An unreleased internal model generated them, and they cover 372 families of related results. OpenAI [says the model attempted about 4,000 problems](https://www.edtechinnovationhub.com/news/openai-releases-722-ai-generated-mathematics-papers-as-researchers-weigh-what-comes-next), with most results costing roughly three hours of ChatGPT Pro thinking compute. The headline claims are large in scope. They include a proof of the Unique Games Conjecture, a zero-free region for the Riemann zeta function where the real part exceeds 7/8, progress on the rational Hodge conjecture for CM abelian varieties, and a resolution of the free group factor problem. Each of these is OpenAI's claim, and none has been independently verified.

The next day, OpenAI [withdrew three manuscripts](https://retractionwatch.com/2026/10/08/openai-withdraws-preprints-722-manuscripts-unsolved-math-problems/), according to Retraction Watch. One paper used +1 where its own conventions required -1. That error invalidated its argument and the construction that two dependent papers relied on. All three concerned the Hodge conjecture. OpenAI also revised 14 other manuscripts with proof repairs, corrected statements and clearer hypotheses, which brought the repository down to 719 papers. According to the repository's own catalogue, [Lean formalizations cover the main result of 162 papers](https://tech.yahoo.com/ai/chatgpt/articles/openai-drops-722-ai-math-171537220.html). The other results rest on unformalized prose that someone has to referee.

The [Association for Human Mathematics (AHM)](https://t.me/aipost/8412) criticized the release and urged mathematicians to stop working with OpenAI. The group [called the release](https://the-decoder.com/some-mathematicians-call-for-openai-boycott-after-ai-generated-proofs-flood-their-field/) "not a demonstration of scholarship, but a demonstration of power." AHM argues that OpenAI ignored an advisory group's statement that frontier labs should not test advanced open problems on internal models. Not every commentator agrees. A [Neowin opinion piece](https://www.neowin.net/opinions/mathematicians-want-openai-out-of-math-research-but-their-argument-doesnt-add-up/) argues that the boycott case is weak, and some AI researchers on X have described the reaction as an attempt by mathematicians to protect their own professional standing.

The withdrawals do not show that the corpus is worthless. They do show where the cost lies. Generating a manuscript took about three compute-hours, but refereeing a claimed proof of a major conjecture takes expert time measured in months. The formalized subset is the only part a reader can trust without that work. OpenAI benefits if the unformalized majority is read as equivalent to the formalized part, and the withdrawals are evidence against that reading.

## What this means

The constraint on machine mathematics has moved from generating proofs to verifying them, and the actors exposed are the ones who supply verification: Lean and Mathlib maintainers, journal referees, and any lab whose fundraising story depends on "solved open problems." OpenAI gains a recruiting and capital-raising narrative from the volume of results. Mathematicians control the scarce resource, which is credible adjudication, and AHM is using that control as leverage. The consensus framing treats this as a conflict between AI and human mathematicians. The more useful frame is a split between results that come with formal certificates and results that do not. The precedent is the Flyspeck project, which formalized Thomas Hales's proof of the Kepler conjecture after referees could not fully certify it, a process that took about a decade. The likelier outcome is that within months OpenAI and its competitors start releasing results that come with formal proofs in Lean or another proof assistant, and the field discounts unformalized claims. The condition is that labs keep competing on claims of reasoning capability. A confirmed independent refereeing of the Unique Games or free group factor result would prove this forecast too cautious and would shift the field faster.

## What to watch

- Whether any of the headline results, especially the claimed Unique Games proof, is refereed or fully formalized by researchers outside OpenAI. That is the first test of whether the corpus holds major results or mostly minor ones.
- Whether the share of manuscripts with Lean formalizations rises from the current 162. A rising share would mean OpenAI is converting the verification gap into a defensible asset.
- Whether journals or arXiv moderators adopt explicit policies for bulk machine-generated mathematics submissions. Such policies would determine whether this work can enter the formal literature.