OpenAI's math catalogue held 721 papers this week. Dana Moshkovitz, who teaches math at UT Austin, has read some of them. "The write-up is terrible. The write-up is not made for human consumption," she said1.
Moshkovitz's complaint explains why so many people are searching this week. Readers want to know whether mathematicians can check this much math. OpenAI built the catalogue by posing one unnamed internal model roughly 4,000 problems2. Checking each claim by hand takes time, because the field moves slower than the model that wrote the proofs.
A Catalogue That Keeps Growing
OpenAI's catalogue kept growing. On Oct. 26, the company added two new papers3. One claims to disprove the Exponential Time Hypothesis, a longstanding question about how fast computers can solve hard counting problems7.
OpenAI sent that claim past its own Lean checker. It asked an outside panel to examine the proof before anyone trusts it3. Computer scientists Russell Impagliazzo, Ramamohan Paturi and Ryan Williams lead that panel.
Three days earlier, on Oct. 7, a sign error forced OpenAI to withdraw three papers. Fixing it touched 14 more directly, and updating citations in 13 others brought the correction's full reach to 30 papers3. The catalogue now spans 373 result families2. Only 300 of its 719 top-line results, about 42 percent, carry a finished proof check.
Two Weeks to Check One Old Theorem
Checking math by hand still runs on volunteers. The Simons Foundation hosted a two-week Lean workshop in June 2025. Mathematicians Alex Kontorovich, Antoine Chambert-Loir and Heather MacBeth led it. Fifty-seven postdocs, graduate students and early-career researchers showed up5.
Their biggest prize was formalizing the prime number theorem, a nearly century-old result about how prime numbers thin out. Kontorovich, who teaches at Rutgers University, described the final push. "We worked for five days, eight hours a day, knocking off those goals. Once those things were done, I just put in the last step. So that proof formalization is thanks to the Simons Foundation," he said5.
Forty hours of focused team time closed out one proof the field had already trusted for decades. OpenAI's model, by contrast, spent about three hours of compute per claimed result, across 721 of them25.
A workshop needed 40 hours to close one proof; OpenAI's model averages three
Hours of work behind two kinds of math checking, a June 2025 Lean workshop and OpenAI's October 2026 catalogue
The base column is the hours Alex Kontorovich's team spent finishing the prime number theorem's Lean proof; the accent column is the average compute hours behind each of OpenAI's 721 claimed results.
The workshop figure covers one team's final push on one theorem; the repository figure averages compute time across all 721 claimed results, so the two columns measure different kinds of work.
Sources: GitHub [2]; Simons Foundation [5]. Chart by Ryan Elliott Dennis.
The numbers behind this chart
| Item | Value |
|---|---|
| Prime theorem push | 40 hrs |
| Avg. OpenAI result | 3 hrs |
Money Chases the Backlog
OpenAI and Anthropic each pledged roughly $5 million on Oct. 15. The Simons Foundation program they fund helps mathematicians check AI-assisted results. Together, the three organizations committed $15 million4. Applications for the first grants close Dec. 1.
OpenAI@OpenAIWe want to support the mathematics community in turning progress in AI into deeper human understanding and new discoveries. To support that goal, we are contributing $5 million to a new Simons Foundation initiative to help mathematicians examine, understand, and build on results… https://t.co/VLVfCujFYu
David Spergel leads the Simons Foundation. He framed the moment as a test for the field's own institutions, ahead of any single lab. "This is a moment for the mathematics community to come together," he said. "The community should be driving discussions of how these tools are evaluated, adopted and used, not any single company or institution"4.
Lean itself grew out of foundation money years before this flood arrived. Carnegie Mellon University hosts a research center built around Lean, under Jeremy Avigad. Charles Hoskinson funded it with a $20 million gift in 20215. A separate nonprofit, formed in 2023 with a $5 million gift from Simons Foundation International, now maintains the Lean software itself.
Leonardo de Moura, Lean's creator, says the tool's real value is letting strangers rely on each other's work. "I think the math community loves most that Lean enables them to work together, even with people that they never met before," he said.
Three weeks after OpenAI's bulk release, the formalized share still sits near 42 percent23. The new funding arrived; that number stayed put.
Lean has formally checked 42 percent of OpenAI's 719 top-line math results
Formalization status of the 719 top-line results in OpenAI's public math repository, as of Oct. 31, 2026
Sources: GitHub [2]; GitHub [3]. Chart by Ryan Elliott Dennis.
The numbers behind this chart
| Item | Value |
|---|---|
| Carries a finished Lean check | 300 |
| Whole | 719 |
Whether the System Can Keep Up
Kontorovich argues the volunteer system already works, just slowly. He points to his own habit of leaning on software for calculations he used to redo by hand. "I can do it by hand on paper, and there's a good chance I'll make a mistake. So I'll do it five times until I get the same answer twice," he said6.
Terence Tao teaches mathematics at UCLA. He won the Fields Medal, math's highest honor. Tao will give a public lecture on AI at this year's International Congress of Mathematicians.
He wants the field to slow down and ask what checking is for. Tao said he will explain "why it is important that the distinctively human features of our profession are not lost in this transformation, and that we are more explicitly aware of all the broader goals of mathematics, not just the ones that can be efficiently resolved by computers"6.
Both draw on the same catalogue. Kontorovich trusts the pace of volunteer work to catch up. Tao wants the field to decide what counts as finished before the backlog decides for it.
What to Do
Treat a new OpenAI math claim as a lead. Wait for a named mathematician outside the company to check it by hand or in Lean. Call it unfinished until then.
Readers tracking a specific claim should bookmark OpenAI's own history log. It recorded the Oct. 7 withdrawals and the Oct. 26 additions within days of each change.
Watch the Dec. 1 grant deadline for a second signal. A jump in the formalized share after that date would matter. It would show Simons Foundation money reaching the checkers, ahead of the provers.
By the Numbers
- 721 papers: OpenAI's public math catalogue, organized into 373 result families, as of this week2.
- 42 percent: the share of its top-line results carrying a finished Lean proof check2.
- 4,000 problems: how many an unnamed internal OpenAI model answered to build the collection2.
- 57 researchers: postdocs, grad students and early-career academics at a June 2025 Simons Foundation Lean workshop5.
- 30 papers: withdrawn, revised or re-cited in one Oct. 7 correction batch, after a sign error forced three retractions3.
- $15 million: the combined pledge from OpenAI, Anthropic and the Simons Foundation to help check AI math claims4.
- 2 new papers: added Oct. 26, including a claimed disproof now before an outside panel of three computer scientists3.
- Dec. 1: the deadline for the first grant applications under the Simons Foundation's new math-and-AI program4.
What to Watch
Watch the formalized share in OpenAI's own catalogue. It sat near 42 percent through three weeks of new work. A jump past that line would show checking capacity itself growing, past the funding meant to grow it.
An independent panel is reviewing the Exponential Time Hypothesis claim. It will show whether three computer scientists can clear one result before OpenAI's model writes the next one.
Sources
- Geoff Brumfiel, "AI is shaking up the field of mathematics. But what comes next?" NPR, Oct. 21, 2026, https://www.npr.org/2026/10/21/nx-s1-5995392/ai-is-shaking-up-the-field-of-mathematics-but-what-comes-next
- OpenAI, openai/math repository (README), GitHub, accessed Oct. 31, 2026, https://github.com/openai/math
- OpenAI, openai/math repository (history.md), GitHub, accessed Oct. 31, 2026, https://raw.githubusercontent.com/openai/math/main/history.md
- Simons Foundation, "Simons Foundation Launches $15M Effort To Help Mathematicians Navigate AI Era," Oct. 15, 2026, https://www.simonsfoundation.org/news/simons-foundation-launches-15m-effort-to-help-mathematicians-navigate-ai-era/
- Yen Duong, "From Trust to Verification: Lean's Impact on Mathematics," Simons Foundation, June 23, 2026, https://www.simonsfoundation.org/2026/06/23/from-trust-to-verification-leans-impact-on-mathematics/
- Yen Duong, "AI Will Be Top of Mind at ICM, Math's Biggest Conference," Simons Foundation, May 4, 2026, https://www.simonsfoundation.org/2026/05/04/ai-will-be-top-of-mind-at-icm-maths-biggest-conference/
- Wikipedia contributors, "Exponential time hypothesis," Wikipedia, accessed Oct. 31, 2026, https://en.wikipedia.org/wiki/Exponential_time_hypothesis
