OpenAI's 372 math results outrun the people who must check them
OpenAI published 372 families of math results from an unreleased model on Oct. 6, more than mathematicians have yet been able to check or understand. Each claim now waits on human readers, who must work without the prompts OpenAI chose not to publish.
The Board Room · Leadership desk
Bar comparison of OpenAI's 719 top-line math results as of Oct. 7: 300, about 42%, had proofs a computer checked in Lean; 419 had no Lean proof.
OpenAI's 719 top-line results, as of Oct. 7 In results
| Item | Value | Claim |
|---|---|---|
| Proof checked in Lean | 300 results | 3 |
| No Lean proof | 419 results | 28 |
What happened
- The batch includes a claimed proof of the Unique Games Conjecture, which UT Austin complexity theorist Dana Moshkovitz had worked toward for years.
- An OpenAI spokesperson said many of the results are not yet understood by the company's own mathematicians.
- OpenAI released average compute figures and 10 reasoning summaries, short of the per-result disclosure an Institute for Advanced Study advisory group requested on Sept. 29.
Why it matters
- What it limits constraint While the model stays internal, nobody outside OpenAI can rerun a single-agent claim, and MIT's Andrew Sutherland treats every such claim as unverified until the model is released.
- What it costs cost The cost of review falls on academic groups that did not produce the work, starting with researchers at UT Austin and the Simons Institute who are rushing to read the manuscripts.
- What it sets up precedent OpenAI has agreed to work with the Institute for Advanced Study without pledging to stop testing on open problems, so its next release will be judged against the Sept. 29 guidelines.
Next story · Product · Oct 8
OpenAI's math proofs fall short of a Princeton panel's verification standardsConfirmed3 publishers
The cost of producing a result fell sharply between OpenAI's two releases. The September Navier-Stokes work used a swarm of 10,000 AI agents and millions of dollars in computing [9]. For the October batch, a company spokesperson said nearly every result came from a single prompt to a single agent, though some may have taken several attempts [19]. Reading the output got no such reduction. Each family can bundle a main proof with supporting arguments, consequences or alternative proofs [8], so the catalogue runs to 719 manuscripts, nearly two per family [17].
Machine checking covers part of that load. Lean lets a computer check every step of a proof [4], but 419 top-line results still had no Lean proof as of Oct. 7 [28]. A passed check is also narrower than understanding. Few people have understood the proofs, including those a computer has verified, implicator.ai reported [5]. Scott Aaronson, a UT Austin researcher, wrote on his blog that "it also appears that no human has understood just about any of these proofs yet; the race to do so has just started" [6].
Dana Moshkovitz's attempt to read the Unique Games proof shows what that race involves. "It feels like something written by someone who's on psychedelics," she wrote in texts Aaronson published [14]. "Basically the paper is so horribly written that it's impossible to read it without AI help," she wrote [15]. She asked an AI model to pull together claims scattered across the paper [16]. The stakes are concrete. If the conjecture holds, Max Cut and a long list of other optimization problems are NP-hard even when the target is only slightly better than what semidefinite programming already gives [18].
OpenAI traded checkability for publication speed. The Institute for Advanced Study's advisory group had asked on Sept. 29 for the model name, prompts, reasoning summary, time and computation cost of each result [11]. Without the prompts, I think no outside reader can separate what the model contributed from what the person prompting it supplied. Tristan Buckmaster, a New York University mathematician, raised that problem with the New York Times, saying people prompting the models could be giving them information that helped them reach results [20]. "There's likely to be a bunch of results where they take someone's work and then take it to completion," Buckmaster said [21].
The Association for Human Mathematics has taken the hardest line, urging mathematicians to stop working with OpenAI [27]. The strongest case for that position is the institute's own warning that proprietary models risk "creating a two-tier system where labs outrun the rest of the field, effectively alienating the mathematical community from its own discipline" [23]. A boycott has a cost too. It pulls readers away from a backlog in which most top-line results lack even a machine check [28].
Two timelines run here. This month's question is whether specific proofs, the Unique Games claim first, survive human reading. The decade's question is the one the institute's statement set out: "It is now the case that AI can output mathematical arguments in situations without the human who prompted it being able to understand the arguments, verify them, or take responsibility for them" [22].
What to watch
- Whether the Lean-checked count rises beyond 300 of 719, and whether a human-written account emerges of whether the Unique Games proof holds.
- Whether OpenAI publishes the prompts or releases the model, the step that both Sutherland's standard and the IAS guidelines point to.
- The terms of OpenAI's work with the Institute for Advanced Study, including whether outside mathematicians get access to the model.
Clarity's read
What the record supports and how the coverage leans. The claims behind it follow.
Reality
- Evidence50
- Adoption
- Not scored
- Hype gap+45
- Incentives65
- Confidence60
Perspective Coverage
3 publishers- Builder
- Builder 32%
- Operator
- Operator 38%
- Investor
- Investor 30%
Claim ledger
Ranked by verification strength, evidence, and original report placement.
- [1]
At 6 p.m. EDT on Oct. 6, 2026, OpenAI posted 372 families of mathematical results from an unreleased internal model.
- [2]
OpenAI published over 370 mathematical results across topics such as algebra, theoretical computer science and mathematical logic.
- [3]
As of Oct. 7, 300 of the 719 top-line results, about 42%, had proofs a computer had checked in Lean.
- [4]
Lean is a programming language that lets a computer check every step of a mathematical proof.
- [5]
Few people have yet understood the proofs, including ones a computer has checked.
- [6]
Scott Aaronson, a UT Austin researcher, wrote on his blog on Oct. 7: "it also appears that no human has understood just about any of these proofs yet; the race to do so has just started."
- [7]
Many of the results were not yet understood by OpenAI's own mathematicians, a company spokesperson said.
- [8]
A family groups papers about a related result and can include the main proof, supporting arguments, consequences or alternative proofs; the catalogue lists 719 manuscripts.
- [9]
On Sept. 8, 2026, OpenAI announced a result involving the Navier-Stokes equations that used a swarm of 10,000 AI agents and millions of dollars in computing resources.
- [10]
Researchers at UT Austin and the Simons Institute in Berkeley were rushing to study the manuscripts.
- [11]
The Institute for Advanced Study advisory group's Sept. 29 guidelines requested the model name, prompts, reasoning summary, time and computation cost for each result.
- [12]
OpenAI published average compute and 10 reasoning summaries but no prompts, short of the Sept. 29 guidelines from the Institute for Advanced Study's advisory group.
- [13]
The release includes a claimed proof of the Unique Games Conjecture; Dana Moshkovitz, a complexity theorist at UT Austin, had worked toward proving it for years.
- [14]
"It feels like something written by someone who's on psychedelics," Moshkovitz wrote in texts published by Aaronson.
- [15]
"Basically the paper is so horribly written that it's impossible to read it without AI help," Moshkovitz wrote.
- [16]
To read the AI-written proof, Moshkovitz asked an AI model to pull together claims scattered across the paper.
- [17]
The catalogue holds nearly two manuscripts per result family.
- [18]
If the Unique Games Conjecture holds, a long list of optimization problems including Max Cut are NP-hard even when asking only for an answer slightly better than semidefinite programming already gives.
- [19]
An OpenAI spokesperson said nearly every Oct. 6 result came from a single prompt to a single agent, and that some results might have taken multiple attempts.
- [20]
Tristan Buckmaster, a New York University mathematician, told the New York Times that mathematicians prompting AI models to solve equations could be providing information that helped the model get to the result.
- [21]
"There's likely to be a bunch of results where they take someone's work and then take it to completion," Buckmaster said.
- [22]
"It is now the case that AI can output mathematical arguments in situations without the human who prompted it being able to understand the arguments, verify them, or take responsibility for them," a statement from the Institute for Advanced Study read.
- [23]
"The use of proprietary internal models by AI labs to do mathematical research risks creating a two-tier system where labs outrun the rest of the field, effectively alienating the mathematical community from its own discipline," the group wrote.
- [24]
OpenAI announced it would work with the Institute for Advanced Study to give "mathematicians a voice in how we move forward".
- [25]
OpenAI did not indicate that it would stop testing its AI models with advanced mathematical problems.
- [26]
MIT's Andrew Sutherland called single-agent claims unverified until the model is released.
- [27]
The Association for Human Mathematics urged mathematicians to stop working with OpenAI.
- [28]
As of Oct. 7, 419 of the 719 top-line results had no Lean proof.
Sources
3 independent publishers whose own reporting we read for this story.
- exponentialview.comight mean for the future of human knowledge
1 article · October 10, 2026
- implicator.aiOpenAI's 372 AI Math Results Leave Mathematicians Racing
1 article · October 8, 2026
- theguardian.comOpenAI’s release of mathematical findings draws concerns from experts
1 article · October 7, 2026
Topics and entities
Topics
- AI research disclosure norms
- AI for Mathematics
- Formal proof verification
Entities
- OpenAI
- Simons Institute for the Theory of Computing
- Association for Human Mathematics
- Navier-Stokes Equations
- Institute for Advanced Study
- Unique games conjecture
- Scott Aaronson
- Tristan Buckmaster
- Lean
- Andrew Sutherland