The Simons Foundation is putting a $15 million package of money, models and computing behind a question that has moved from laboratories into the daily life of mathematics: how should researchers test, understand and govern results produced with artificial intelligence? Announced October 15, the partnership with OpenAI and Anthropic is designed to let mathematicians set the standards for that work, rather than treating a company’s model output as a finished theorem.
What the partnership actually funds
The headline figure is easy to misread. The Simons Foundation’s announcement describes $15 million in combined funding and resources from the foundation, OpenAI and Anthropic. It does not say that $15 million will be distributed as cash grants, and it does not publish a three-way split. OpenAI separately says it is contributing $5 million; the remaining package includes the foundation’s awards and resources from both model companies, with Anthropic’s individual contribution not specified in the public announcements.
The foundation will manage and award the funding, including through an open call. The stated targets are workshops and other initiatives that help researchers evaluate AI-assisted results, learn to use new tools, exchange views and develop collective standards for responsible use. Applications for the Targeted Grants to Math+AI Institutes opportunity are open, with proposals due December 1, 2026, at noon Eastern time, according to the foundation’s notice.
OpenAI and Anthropic are not simply writing checks. They are also expected to provide models and computing resources to a selected group of researchers supported by the Simons Foundation. The Simons announcement says the support can extend beyond mathematics to basic science. That arrangement gives awardees access to capabilities that would otherwise be expensive or unavailable, while keeping the foundation in the role of program manager and grantmaker.
Why verification has become the central problem
The initiative arrives alongside a public release that makes the problem concrete. In its October 15 update, OpenAI said it was contributing $5 million after releasing a broad set of mathematical results produced by an internal frontier model. The company said it had consulted an independent advisory group at the Institute for Advanced Study while developing release practices, including protocols for revisions and citations.
OpenAI’s repository is not presented as a shelf of settled discoveries. Its README says the collection contains manuscripts at different stages of verification, that not all have Lean formalizations and that some unformalized results could have issues. That warning is central, not a footnote. A fluent proof-like document can still contain a missing case, an invalid inference or a claim whose formal statement differs from what readers think it says.
Lean changes the nature of one part of that review. It is a programming language used to express proofs so a computer can check the formal object. But formalization is not the same as proving every surrounding interpretation, and an absence of formalization is not a verdict that a manuscript is false. The practical challenge is deciding which claims to formalize, how to expose assumptions, how to reproduce the result and how to credit human contributions.
The repository as a live case study
The current repository catalogue lists 719 manuscripts organized into 372 families, with roughly 42% of top-line results formalized, according to its README. A family can contain a principal result, related arguments, consequences or alternative proofs. Those counts are a snapshot of a changing company repository, not an independent census of valid mathematics. They are useful because they show the scale of the review task and the gap between generated manuscripts and machine-checkable artifacts.
OpenAI says the collection was assembled after posing approximately 4,000 problems to the internal model and selecting outputs into result families and manuscripts. It reports that the average result used the equivalent of about three hours of ChatGPT Pro thinking compute. Both figures are company-reported descriptions of how the release was produced, not independent measures of correctness, novelty or research value.
How the support is meant to work
The foundation’s design puts shared inquiry ahead of a single “AI mathematician” narrative. Workshops can bring specialists together to inspect a result line by line, compare proof assistants with conventional peer review and decide what evidence should accompany a model-generated claim. Conferences can connect researchers who are building tools with those who must judge their outputs. Special programs can train mathematicians to use models without making model fluency a substitute for mathematical judgment.
That range is important because the bottleneck is not only compute. Researchers need time to reproduce claims, access to domain experts, support for formalization and norms for citing machine assistance. They also need a way to distinguish a model’s useful conjecture from a result ready for publication. The Simons announcement says the effort will help the community evaluate recent AI-assisted results, learn tools, share perspectives and shape standards; it does not announce one universal review protocol.
OpenAI’s own release points toward that infrastructure. The company says it is publishing formalizations as they become available, adding details about how results were obtained and exploring community-hosted alternatives for the materials. It also says future releases should improve citations, exposition and presentation. Those are editorial and verification commitments, but they remain commitments from the releasing company rather than a completed independent audit.
A community-governance test
The arrangement therefore tests whether philanthropy and industry resources can support scrutiny without allowing the suppliers of models to define success. The foundation’s president, David Spergel, said the community should drive discussions of how tools are evaluated, adopted and used. That principle will be tested in the details: who reviews applications, how conflicts are handled, whether negative findings are funded and whether researchers can publish results that complicate the companies’ claims.
Access to a company’s models may accelerate useful work, but it can also create dependence on changing products, proprietary interfaces or scarce compute. A durable program would make its methods and outputs portable enough that mathematicians can compare systems and revisit results after a model is retired. The public announcement establishes the ambition; it does not yet answer those implementation questions.
What remains unproved about the initiative
Three uncertainties should stay visible. First, the total is a bundle, so its eventual value will depend on how much is awarded in cash, how much computing is supplied and how many researchers receive access. Second, the companies’ roles are not symmetrical in the public record: OpenAI discloses a $5 million contribution, while Anthropic’s amount is not stated. Third, the repository’s manuscript count and formalization rate can change as files are added, revised or corrected.
There is also a difference between making AI-assisted mathematics easier to inspect and demonstrating that AI is reliably producing important mathematics. The independent report from The Verge frames the initiative as a response to upheaval caused by AI companies racing to solve longstanding problems and releasing large volumes of research. That context explains the urgency, but it is not evidence that the underlying results are correct.
The strongest near-term measure of success will be less dramatic than a headline breakthrough. It will be whether independent mathematicians can reproduce claims, identify errors openly, formalize meaningful portions, improve explanations and establish standards that apply beyond one company’s repository. Until those outputs exist, the $15 million initiative is best understood as an attempt to build the institutions and tools needed to evaluate an AI-shaped research pipeline.
FAQs
What is the initiative?
It is a Simons Foundation-led program backed by $15 million in combined funding and resources from the foundation, OpenAI and Anthropic. It is intended to help mathematicians evaluate AI-assisted results, learn tools, convene discussions and develop community standards. The total is not described as an all-cash grant pool.
How much is OpenAI contributing?
OpenAI says it is contributing $5 million to the initiative and will provide access to its models and computing resources for Simons-supported researchers. The public announcements do not state Anthropic’s individual dollar contribution.
Who awards the funding?
The Simons Foundation will manage and award the funding, including through an open call. Its notice says applications for the Targeted Grants to Math+AI Institutes opportunity are due December 1, 2026, at noon Eastern time. Selected researchers may also receive model and compute access from OpenAI and Anthropic.
Are the results in OpenAI’s repository verified?
Not all of them. The repository says manuscripts are at different verification stages, not all have Lean formalizations and some unformalized results could have issues. Its current catalogue lists 719 manuscripts in 372 families, with about 42% of top-line results formalized. Those figures do not establish that every remaining manuscript is wrong, or that every formalized result is independently judged important.
Why does Lean matter?
Lean allows a proof to be represented in a form that a computer can check. That can make specific formalized claims easier to audit and reproduce. It does not by itself settle the quality of a manuscript’s motivation, interpretation, novelty or informal explanation, and it does not replace human review of claims that have not been formalized.