Why Mathematicians Are Furious at OpenAI's 722 Proofs
OpenAI dumped 722 AI-written math papers on GitHub and skipped the rules its own advisers set. Mathematicians now want a boycott. Here is why, and the cost.
On October 6, 2026, OpenAI posted 722 math manuscripts written by an unreleased internal model to its openai/math GitHub repository, claiming results across 372 families of problems. Within a day the Association for Human Mathematics called on mathematicians to stop working with OpenAI. The anger is not that the AI is bad at math. It is that OpenAI tested a private model on open problems after its own advisory group asked it to stop, released hundreds of papers no human yet understands, and withdrew three of them within 24 hours.
The economics make the fight sharper. By this site’s estimate, the whole batch cost OpenAI somewhere between a few thousand and about a hundred thousand dollars of compute at public list prices. That is a rounding error next to a career spent on one problem.
Why are mathematicians mad at OpenAI?
Five complaints recur across the statements and reporting. In order of how often they come up:
- It ignored the first thing its advisers asked. OpenAI set up the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted at the Institute for Advanced Study. The group’s September 29, 2026 recommendations open by asking labs to “stop testing advanced mathematical problems on proprietary models.” OpenAI’s own repository README says the opposite is standard practice: “As part of model development, we evaluate our models on open research problems.”
- Volume over scholarship. The Association for Human Mathematics statement, guest-posted on Terence Tao’s blog on October 7, puts it bluntly: “Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power.” It adds: “Mathematicians did not ask for this work to be done,” and “We urge mathematicians to discontinue their work with OpenAI.”
- Most of it is unchecked. About 42% of top-line results (300 of 719) have Lean formalizations, according to the repo’s release history. The other 58% are prose that no one has verified. The README itself warns that “Some of the unformalized results could have issues.”
- Credit and plagiarism. The batch comes from the same model behind OpenAI’s disputed Navier-Stokes claim, as reported by TNW. NYU mathematician Tristan Buckmaster, whose own Navier-Stokes work sits at the center of that dispute, told Fortune: “I don’t think they’ve done their sort of due diligence at all.” In September, 25 Fields Medalists had already warned of “severe attribution and plagiarism questions” in an open letter, as reported by TechCrunch.
- It drains the field. Tao argued that “Problems are being solved autonomously by AI prompters” and called the mass release the end of “Math 1.0”, as reported by Fortune. Harvard’s Melanie Wood said the solutions arrive with “no human understanding” of them, per TechCrunch. Open problems are how graduate students earn careers. Clearing hundreds of them in one push, without the understanding, removes the training ground.
What did OpenAI actually release?
All figures below come from OpenAI’s openai/math README and history file, read on October 10, 2026.
| Item | Figure |
|---|---|
| Problems posed to the model | About 4,000 |
| Manuscripts at launch (Oct 6) | 722 |
| Manuscripts after withdrawals | 719 |
| Result families | 372 |
| Top-line results with Lean proofs | 300 (about 42%) |
| Families with reasoning summaries | 10 |
| Withdrawn on Oct 7 | 3 (one sign error, two papers that depended on it) |
| Revised on Oct 7 | 14 |
| Compute per result | About 3 hours of “ChatGPT Pro thinking” on average |
| Model | Unreleased internal OpenAI model, unnamed |
| License | Apache-2.0, hosted in OpenAI’s own GitHub org |
Headline claims include the symmetric and general Mahler conjectures, the irrationality exponent of π and Kaplansky’s direct-finiteness conjecture in characteristic two. Two results did not follow the standard procedure: a zero-free region for the Riemann zeta function, whose writeup was human-edited, and the Hodge conjecture for CM abelian varieties.
| Stage | Tasks remaining | Percent of candidate pool kept |
|---|---|---|
| Problems posed (internal evaluation) | 4,000 | 100% |
| Manuscripts kept (722 posted, 3 withdrawn) | 719 | 18% |
| Result families (related papers grouped) | 372 | 9% |
| Lean-formalized (top-line results) | 300 | 8% |
| Reasoning summaries (how the model got there) | 10 | 0% |
How much did OpenAI’s math proofs cost?
OpenAI has not published a dollar figure. It gives one average, three hours of ChatGPT Pro thinking per result, and no token count. The numbers below are this site’s model, not a disclosure. Treat them as an order of magnitude.
The anchor is OpenAI’s own Navier-Stokes run, which reported about 130 billion output tokens from roughly 10,000 peak agents over 88 hours (covered in detail in what the Navier-Stokes run cost). That works out to about 147,700 output tokens per agent-hour. It is a floor, because 10,000 was the peak, not the average. Three hours at that rate is about 443,000 output tokens per result. Priced at public rates for GPT-6 Astra ($50 per million output tokens) and GPT-6 Sol ($10 per million), from OpenAI’s developer pricing:
| Scope | At GPT-6 Astra output rates | At GPT-6 Sol output rates |
|---|---|---|
| One result (3 hours) | about $22 | about $4.40 |
| 372 result families | about $8,200 | about $1,650 |
| All 4,000 problems, if each ran 3 hours | about $88,600 | about $17,700 |
| Navier-Stokes full effort, for comparison | about $15,000,000 | n/a |
Three caveats push these numbers up. Inputs are not counted. “ChatGPT Pro thinking” may run several attempts in parallel. And an unreleased model may cost more to serve than today’s public ones. Even with a tenfold allowance for all three, the upper bound stays under $1 million, less than a fifteenth of the Navier-Stokes effort.
That is the commercial point under the anger. A result that costs a mathematician years costs a lab tens of dollars at list price, and the cost of being wrong lands on the people who have to check it. Three withdrawals in a day is what cheap generation and expensive verification look like together.
Did OpenAI follow its advisers’ rules?
Partly. OpenAI’s blog post said it had “drawn on” AGMAI’s advice, according to Fortune, and AGMAI itself answered only that it would “reaffirm our published recommendations on responsible release.” Set side by side, the record looks like this:
| Recommendation | Verdict | What OpenAI did |
|---|---|---|
| Stop testing on proprietary models | Not met | Posed about 4,000 problems to an unreleased model |
| Use a repository labs do not control | Not met | Hosted in OpenAI's own GitHub org |
| Name the model | Not met | Described only as an 'unreleased internal model' |
| Prompts and summarized reasoning | Partly | Reasoning summaries for 10 of 372 families |
| Time and compute cost per result | Partly | One average: 3 hours of ChatGPT Pro thinking |
| Formalize as far as possible | Partly | 300 of 719 top-line results in Lean |
| Metadata linking prose and Lean | Partly | A formalization catalogue, short of what was asked |
| Fund human understanding | Partly | Pledged workshops; AGMAI wants nonprofits to decide |
The repository question matters more than it looks. AGMAI asked for a scholarly repository with “a persistent citable identifier”, one no lab controls. OpenAI’s README says only that it is “exploring community-hosted repositories.” Until that happens, OpenAI decides what stays up, what gets revised and what gets withdrawn.
Can you trust a Lean-checked AI proof?
Not on its own. A Lean proof shows that the formal statement follows. It does not show that the formal statement matches the claim in the paper. A 2026 arXiv preprint, Navier-Stokes lost in translation (Bastounis, Circelli and Hansen), argues that translating informal math into Lean faithfully is harder in principle than any computational problem. It gives examples of mistranslation, including OpenAI’s Navier-Stokes proof: “the formalised Lean proof does not correspond to the NL proof.” The preprint has not been peer-reviewed, and its authors do not claim this disproves OpenAI’s result.
So even the 42% with Lean proofs need a human to confirm the formal statement says what the paper says. That is the slow, unpaid labor the boycott call is about.
Who is defending OpenAI?
Not everyone is angry. Dan Litt, a mathematician at the University of Toronto, told Fortune: “My view is that this is great for mathematics.” He praised the open GitHub release and OpenAI’s restrained marketing, and called worries about proof readability “overstated.” His warning ran the other way: a public sense that “AI solved math” could cut funding and steer young people away from the field.
OpenAI says it wanted the results “to push the frontier of human knowledge and enable further progress in mathematics,” and has pledged more formalizations plus funding for workshops, conferences and programs to help mathematicians work through the results, according to Fortune. It denied, regarding Navier-Stokes, that it fed its model other mathematicians’ unpublished work.
What happens next?
Watch three things. First, the history file: if withdrawals keep coming, the critics’ case gets stronger every week. Second, whether OpenAI moves the collection to a community-run repository, the cheapest concession on AGMAI’s list. Third, whether the funding pledge passes to independent nonprofits, as AGMAI asked, or stays with OpenAI.
For anyone tracking AI benchmarks, the episode is a lesson in what a “solved” claim is worth before verification. That question runs through whether AI benchmarks are reliable at all.
Frequently asked questions
- Why are mathematicians mad at OpenAI?
- OpenAI posted 722 AI-written math manuscripts at once on October 6, 2026, after its own advisory group asked labs to stop testing open problems on private models. About 58% have no formal proof, three were withdrawn within a day, and critics say the release strips human mathematicians of the open problems their careers are built on.
- How many math problems did OpenAI solve?
- OpenAI claims results in 372 families, from about 4,000 problems posed to an unreleased model. The repository now lists 719 manuscripts after three withdrawals. About 42% of top-line results (300 of 719) carry Lean formalizations. None has been peer-reviewed.
- How much did OpenAI spend on the 722 math proofs?
- OpenAI did not say. It reports about three hours of ChatGPT Pro thinking per result. Modeled from its Navier-Stokes token rate at public GPT-6 Astra prices, that is roughly $22 per result and about $8,200 for 372 families, or under $100,000 if all 4,000 problems ran for three hours.
- What is the Association for Human Mathematics boycott?
- On October 7, 2026 the Association for Human Mathematics published a statement, guest-posted on the blog of Terence Tao, calling the release "a demonstration of power" and urging mathematicians to discontinue their work with OpenAI.
- Did Terence Tao criticize OpenAI?
- Yes, according to Fortune. Tao wrote that problems are being solved autonomously by AI prompters and called for a "Math 2.0" that values exposition and community. The AHM boycott statement appeared on his blog as a guest post, without his own comment on that post.
Bottom line
Mathematicians are furious because OpenAI treated open problems as a benchmark: run a private model across 4,000 of them for a few thousand dollars, publish everything at once, fix the errors later. The math may hold up. The fight is over who does the checking, who gets the credit and who controls the record.
Sources
- OpenAI (2026). openai/math: mathematical manuscripts and supporting proof artifacts. GitHub repository and history.md. https://github.com/openai/math
- Advisory Group on Mathematics and Artificial Intelligence (2026). Recommendations on responsible release (September 29). https://agmai.org/general-sep29/
- Association for Human Mathematics (2026). AHM Statement on OpenAI’s October 6 Release of Mathematical Documents. Guest post on Terence Tao’s blog. https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-openais-october-6-release-of-mathematical-documents/
- Bastounis, A., Circelli, F., Hansen, A. C. (2026). Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs. arXiv (preprint). https://arxiv.org/abs/2610.08144
- Fortune (2026). OpenAI publishes solutions to more than 370 outstanding math challenges. Math may never be the same. https://fortune.com/2026/10/07/openai-math-controversy-solutions-370-outstanding-challenges-published-criticisms-celebration/
- TechCrunch (2026). OpenAI’s math solutions aren’t meeting the field’s standards yet. https://techcrunch.com/2026/10/08/openais-math-solutions-arent-meeting-the-fields-standards-yet/
- TechCrunch (2026). OpenAI’s feud with mathematicians is only escalating. https://techcrunch.com/2026/09/11/openais-feud-with-mathematicians-is-only-escalating/
- TNW (2026). OpenAI publishes 722 maths papers written by a model it has not released. https://thenextweb.com/news/openai-maths-722-papers-unreleased-model-github
- OpenAI (2026). GPT-6 Astra model documentation and API pricing. https://developers.openai.com/api/docs/pricing