OpenAI Math is a public repository of 722 mathematical manuscripts and their supporting Lean proof artifacts, almost all of them written by an internal OpenAI model rather than by a person. It is aimed at research mathematicians, Lean users and AI researchers who want to read machine-written proofs and try to check them. The repository is documents and formal proofs; there is no tool to install.
What it does
It publishes the mathematical output of an unreleased OpenAI model as a browsable collection. The README describes 722 manuscripts organized into 372 families, where a family groups related papers — a principal result plus companion arguments, consequences or alternative proofs — and each family is classified by mathematical discipline.
There are four entry points:
overview.pdfdescribes the families.CONTENTS.md, the manuscript map, lists individual papers and their supporting materials.preprints/holds the PDFs, the source files, and per-manuscript citation and build instructions.lean/holds the formal proofs, withformalization.yamlas a catalog mapping formalizations to papers along with their verification configurations, plus a separate ComparatorChallenges README with additional checking instructions.
There is also a set of abridged summaries of the model's own reasoning for selected families — family 007, on ordinary two-point correlations of multiplicative functions, is one row in that table. Everything is Apache-2.0.
How it works
OpenAI frames the collection as a by-product of model development: it evaluates its models on open research problems, and expanded those evaluations after performance on its existing mathematical evaluations saturated. Some outputs build on earlier results the models produced.
The cost figures you may have heard come from the video and the channel's write-up, not from the repository: one unreleased model, roughly 4,000 problems posed to itself, about three hours of ChatGPT Pro thinking compute per problem. The README states no compute, cost or model name at all. The numbers that are the project's own are 722 manuscripts, 372 families, and the line that many — but not all — of the manuscripts have been formalized.
That split decides how much weight each item carries. A manuscript with a Lean formalization can be checked by machine, by you. A manuscript without one is a prose preprint whose only reviewer so far was a model. OpenAI says the collection includes results at different stages of verification, that it will keep adding Lean formalizations as it obtains them, and that it is exploring community-hosted repositories for the materials.
Getting started
Everything lives at github.com/openai/math, and git clone https://github.com/openai/math is the whole install. To read it you need nothing beyond a PDF viewer; the project lists no operating system, CPU, memory or GPU requirements.
To verify rather than read, you need your own Lean toolchain. The repository supplies the verification configurations in lean/formalization.yaml, instructions in lean/README.md, and the Comparator instructions for extra checking. It does not say how long a full check takes or what hardware it expects, so plan for that yourself.
On money: reading and checking are free under Apache-2.0, and no API key or subscription is involved — this is a static collection, not a tool that calls a model. The paid part is reproduction, not consumption. By the video's account each problem took about three hours of ChatGPT Pro thinking, which is a paid plan rather than the free tier, and the model that wrote these manuscripts has not been released, so nobody outside OpenAI can rerun the work exactly.
When to use it / when not
The main catch is stated in the README in plain words: not everything is formalized, and some of the unformalized results could have issues, which OpenAI says it will try to fix quickly. Treat the prose-only families as claims under review rather than settled theorems — there is no journal, no peer review, and the author cannot answer your questions.
Use it instead of just asking ChatGPT for a proof when you want a fixed artifact with a Lean formalization attached and a stated verification configuration, rather than a fresh chat answer you must re-derive every time.
Don't use it if you need peer-reviewed mathematics to cite in a publication, if you want the model or the weights behind it (neither is here), or if you were hoping for a library to import — this is a paper collection with proof scripts, not mathlib.
The repository is also brand new: it was created and pushed on 6 October 2026, and it already carries around 6,900 stars and 640 forks, which says more about attention than about how much of it has been checked.
Take this seriously if you work in one of the disciplines covered and can read a preprint critically, or if you run Lean and are willing to spend an evening building the formalizations and seeing what actually compiles. For that reader it is the most concrete thing yet published about what a frontier model does on open research problems, and the Lean half is auditable in a way that a chat transcript or a benchmark score is not. For everyone else it is a reading pile with an explicit warning label on part of it: interesting to browse, premature to cite, and worth revisiting as formalizations land.