OpenAI publishes 722 maths manuscripts from an internal model, with Lean proofs for some
Serguey Asael Shinder2 min readOpenAI said on 6 October that it is releasing "a broad range of new mathematical results" produced by an unreleased internal frontier model, and published them in a GitHub repository, openai/math, rather than as a single paper.
What is in the repository. According to its README, the catalogue holds 722 manuscripts organised into 372 families, each family grouping a principal result with companion arguments, consequences or alternative proofs, classified by discipline. It includes:
- PDFs and sources of the preprints, with per-manuscript citation instructions;
- a Lean library and a formalisation catalogue describing which proofs have been checked by computer. "Many, but not all" manuscripts are formalised;
- abridged summaries of the model's reasoning for 10 results, among them the irrationality exponent of π, Kaplansky's direct-finiteness conjecture in characteristic two and the isomorphism of free group factors.
How the results were produced. The model was posed approximately 4,000 problems, and the output was aggregated into families and filtered for significance. On average each result used about three hours of ChatGPT Pro thinking compute. OpenAI names two exceptions to that fixed procedure: work on a zero-free region for the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties; the write-up of the Re(s) > 11/12 zero-free region was edited by humans for readability.
What OpenAI itself flags. The collection contains results "at different stages of verification", and the README says some of the unformalised results "could have issues", to be fixed quickly. Corrections will be published as new versions, with earlier versions kept accessible. OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study on how to release the results, is looking at community-hosted alternatives to GitHub, and will fund workshops and conferences on AI-produced results. The model itself is not released; OpenAI says it is working to release it responsibly.