OpenAI releases 722 AI-generated mathematics papers as researchers weigh what comes next
OpenAI has published hundreds of mathematical manuscripts produced by an unreleased AI model, opening a much bigger debate over how AI-generated research should be checked, understood and incorporated into mathematics
OpenAI has released 722 mathematical manuscripts produced by an internal frontier AI model
OpenAI has released a collection of 722 mathematical manuscripts generated by an internal frontier AI model, covering hundreds of research problems across mathematics and theoretical computer science.
The collection is organized into 372 groups of related results and includes proofs, alternative arguments, consequences and supporting material. Many of the results also include formal proofs written in Lean, a programming language that allows mathematical arguments to be checked computationally.
OpenAI says the work emerged from testing its internal models on open research problems after performance on its existing mathematics evaluations began to plateau.
Around 4,000 problems were presented to the model during the evaluation process. OpenAI says the average result used computing resources equivalent to roughly three hours of ChatGPT Pro thinking.
The scale of the release makes it considerably different from a typical AI benchmark. Rather than measuring whether a model can answer a fixed set of questions, OpenAI is publishing work that is intended to enter the mathematical research process itself.
But the company is also explicit that publication does not mean every result has already been fully verified.
The repository contains work at different stages of checking, and OpenAI says some manuscripts that have not yet been formalized in Lean could contain errors. Corrections and revisions will be recorded while earlier versions remain available.
From solving problems to publishing research
OpenAI first outlined its approach to releasing AI-generated mathematical results in September, when it said it was working with mathematicians on how such work should be presented responsibly.
The company said it wanted to improve transparency around AI-generated mathematics by publishing supporting information alongside the results, including formal proofs where available, reasoning summaries and details about the computational resources used.
Ten abridged summaries of the model’s reasoning have also been published for results spanning areas including number theory, complexity theory, spin glasses, operator algebras and mathematical physics.
OpenAI says it plans to fund workshops, conferences and other programs focused on understanding significant mathematical results produced by AI.
It is also working towards releasing the model responsible for the research, although that model is not currently publicly available.
Mathematicians say publication is only the beginning
The release has been discussed with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study.
The group was formed after OpenAI approached several mathematicians about creating an external advisory board. The academics instead established an independent organization that can advise any AI company working on systems likely to affect mathematical research.
Its members include mathematicians from institutions including Cambridge, Oxford, Stanford, Harvard, Berkeley, the Institute for Advanced Study, EPFL and Imperial College London.
Following OpenAI’s release, the group described it as an important event for mathematics, while stressing that its involvement should not be interpreted as an endorsement of the results or of the way they were produced.
The group says making the work public is only the start of the process.
Human mathematicians will still need to examine the arguments, understand how the results fit with existing research and determine their significance.
It also warns against a future in which the role of mathematicians becomes largely one of interpreting discoveries generated inside AI companies.
Researchers, it argues, need the freedom and resources to formulate their own questions, pursue their own approaches and investigate areas that have not been selected by frontier AI labs.
Why verification matters
Mathematical proof is an unusual test for increasingly capable AI systems because an answer can be impressive without necessarily being correct.
Formal verification provides one route towards addressing that problem.
Lean allows proofs to be represented in a form that a computer can check line by line against mathematical rules, reducing reliance on a reader simply trusting an AI-generated argument.
OpenAI has included formalizations for many, although not all, of the manuscripts and says further Lean proofs will be added as they become available.
The company has also committed to keeping previous versions accessible when papers are corrected, creating a public history of changes to the work.
For the mathematics community, the next stage is likely to be slower than the initial release.
Hundreds of papers now need to be read, challenged, verified and placed within existing mathematical knowledge before the significance of the collection becomes clear.
OpenAI says it wants its models to help extend human knowledge rather than simply perform well on existing evaluations.
With 722 manuscripts now public, mathematicians have a sizeable test of what that looks like in practice.