OpenAI releases 722 math manuscripts and Lean proof artifacts
OpenAI shares hundreds of mathematics manuscripts while warning that formal verification coverage varies across the collection
OpenAI released a collection of AI generated mathematics on October 6, making manuscripts and supporting proof artifacts publicly available. The results came from an internal frontier model. OpenAI says it is working toward releasing that model, without announcing access or a launch date.
The repository lists 722 manuscripts in 372 families. Those families can combine a main result with companion arguments, consequences or alternative proofs. Verification is uneven across the collection. OpenAI explicitly warns that some results lack Lean formalizations and that unformalized work could contain problems.
What the catalog claims
OpenAI’s research catalog claims a proof of the Unique Games Conjecture, a zero free region beyond Re(s) = 7/8 for Dirichlet L functions including the Riemann zeta function, and a matrix multiplication exponent at most 9/4 over the complex numbers. The field restriction matters when describing that last result.
Other entries concern the rational Hodge conjecture for complex CM abelian varieties and the full BSD formula under specified Selmer corank conditions. The stated consequence for quadratic twists covers a set of density one. These are substantial claims with precise boundaries. ByteForward has not independently verified the mathematical arguments.
What reviewers can inspect
OpenAI says the model was given approximately 4,000 problems during the evaluation. The published manuscripts and families are an organized selection of outputs. Because related papers are grouped together and significance influenced selection, those totals should not be treated as a simple benchmark success rate.
The release includes ten summaries of model reasoning and estimates of computation. OpenAI puts the average result at the equivalent of roughly three hours of ChatGPT Pro thinking. That comparison describes compute used in the research process. It does not establish that a reader can reproduce each result through today’s public product.
The Lean library documentation recommends compiling small portions of the collection at a time. Separate verification instructions provide a Comparator workflow for checking a formalization. The presence of those artifacts gives specialists something concrete to inspect. ByteForward has not run those checks.
Release standards remain contested
OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence. The group’s September 29 recommendations nevertheless oppose testing advanced mathematical problems on proprietary models inaccessible to the wider community. They call for scholarly repositories independent of AI labs and support for human understanding of released results. Consultation should not be read as an endorsement.
OpenAI has committed to funding workshops, conferences and special programs aimed at understanding major AI produced results. It says details will follow. Whether those efforts help mathematicians explain and scrutinize the work will matter alongside the volume of material released.
Read the evidence in layers
The practical starting point is the exact theorem statement, its verification status and the available proof artifacts. Our recent coverage of Meta’s six mathematics papers examines another research collection through its human guidance, review and acknowledgments of earlier work.
Illustrative ellipsoid diagram by Rectas on Wikimedia Commons, released under Creative Commons CC0. Rendered on white and converted to WebP. This general geometry illustration is not a figure from OpenAI’s papers.
