Summary
OpenAI’s public repository catalogues 722 mathematical manuscripts in 372 families, produced mostly with an unreleased internal model. The company says the results are at different stages of verification, and many—but not all—have Lean formalizations.
OpenAI’s public GitHub repository catalogues 722 mathematical manuscripts, grouped into 372 families, along with supporting proof materials. The company says the work was produced mainly by an unreleased internal model as part of evaluations on open research problems. It also cautions that the collection contains results at different stages of verification.
The release is a research catalogue rather than a single mathematical result. Its manuscripts cover different mathematical disciplines, and a family can bring together a principal result, related arguments, consequences or alternative proofs. OpenAI directs readers to an overview of the families and a manuscript map for navigating the collection.
How the collection was assembled
OpenAI says it expanded its evaluations after model performance on its existing mathematical evaluations had saturated. Over the course of the evaluation, the model was posed approximately 4,000 problems. The company reports that each result used an average of three hours of ChatGPT Pro thinking compute with the unreleased model. It says the outputs were grouped into families and manuscripts, with significance requirements applied in deciding what entered the catalogue.
OpenAI describes this as the procedure behind the vast majority of the results, not every item. It identifies exceptions that include work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties. The README also says that the writeup for the region Re(s) > 11/12 was human-edited for readability.
Verification varies across the manuscripts
Many, but not all, manuscripts have Lean formalizations. Lean is a proof assistant: a formalization encodes a mathematical argument in a system whose checker can verify that proof against its formal rules. The repository includes a Lean library and a catalogue of formalizations, with instructions for further checking.
OpenAI says some results do not yet have formalizations and that unformalized work could contain issues. That distinction matters when interpreting the catalogue: a manuscript’s presence in the repository is not the same as a Lean-checked proof. The company says it plans to add formalizations as they are obtained, while preserving earlier public versions and recording corrections and revisions in later ones.