OpenAI's Math Repo Holds 722 Manuscripts, and Its Own Catalogue Formalizes a Fraction of Them
How to read openai/math: start with the papers that have a machine-checked main result, run Comparator yourself, and treat the rest as leads
The repository at the top of Trendshift's momentum board this morning contains no code you would ship. openai/math is 722 mathematics manuscripts, written almost entirely by a model OpenAI has not released, posted on October 6 and sitting in first place on Trendshift the next morning.
The headline number is 722. The more useful number is buried in a YAML file in the lean/ folder, and it is a lot smaller.
What OpenAI actually published
The announcement describes "a broad range of new mathematical results produced by an internal frontier model," and the README fills in the shape. The model was posed about 4,000 problems over the course of an internal evaluation. The 722 manuscripts that came out group into 372 families. On average, each result used "the equivalent compute of roughly three hours of ChatGPT Pro thinking."
The README is candid about the exceptions. "The vast majority of results were obtained with the same procedure," it says, and it names the work that was not, including a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties. The write-up for the Re(s) > 11/12 zero-free region was "human edited for readability."
It is just as candid about verification. "Many, but not all, of the manuscripts have been formalized," and "some of the unformalized results could have issues. We will endeavor to fix any such issues quickly." OpenAI also says it drew on advice from the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study about how to release the results. That is advice on the release, not a review of the proofs.
The license is Apache-2.0. There are no tagged releases. PDFs and sources live under preprints/.
The number in the catalogue
Open lean/formalization.yaml. A comment at the top says it is a "Catalog of papers with a formalized main result." When I read it this morning, it listed 162 source papers and 185 main results, each main result pointing at a Comparator configuration, a Lean declaration and a file.
162 out of 722 is about 22%.
That is not a scandal. The README says formalizations will be added "as we obtain them," and the catalogue's own scope field reads "Partial progress." Two other fields are worth reading before you cite anything: automation lists one method, agent, and review has a status of unchecked. The formalizations were produced by agents, and the catalogue does not claim anyone has reviewed them.
The catalogue may lag the README's "many." It is still the only list in the repository that tells you which manuscripts have a machine-checkable claim behind them. For a reader, that makes it the table of contents that matters.
What Comparator gives you
Each formalized result points at a JSON file under lean/ComparatorChallenges/. Comparator describes itself as "a trustworthy judge for Lean proofs." The setup is simple. A challenge module holds the theorem statement with no proof. A solution module holds the same statement with a proof attached. Comparator checks that the solution proves exactly the challenged theorem, using only the axioms the config permits (the README's example config lists propext, Quot.sound and Classical.choice).
The repo's challenge README gives the commands, run from lean/:
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json
You need comparator, landrun and lean4export on your PATH. The Lean README also warns that building the full library on Linux can fail when vm.max_map_count is set low, and gives workarounds.
Here is the part that makes this worth an afternoon. Comparator moves trust from OpenAI to a small file you can read. Its README lists its assumptions, and the first is that the challenge file and its imports "are controlled by you or trustworthy." If you read the challenge statement, agree it says what the paper claims, and the check passes, you no longer need to trust the model, the manuscript or the company. You need to trust Lean's kernel and your own reading of one theorem statement.
Why a fifth is still a lot
It would be easy to read 22% as a failure. I read it the other way.
A machine-checked main result is the strongest form of evidence mathematics has. A referee can miss a gap in a forty-page argument; Lean's kernel does not get tired on page thirty. If even a large share of those 162 papers hold up once someone confirms the statements match the prose, that is a body of checked work produced at a pace no human group could match.
The catch is the order of operations. The model produced the manuscripts first and the formal checks are catching up. That is the reverse of how a careful mathematician works, and it means the unchecked pile will keep growing faster than the checked one unless the formalization agents speed up. For a reader, the practical consequence is simple: the boundary between "checked" and "claimed" is the most important line in this repository, and OpenAI has drawn it for you in one file.
Put this into practice
If you want to use this release for anything beyond a headline, here is the order I would work in.
1. Start from the catalogue, not the folder. Pull lean/formalization.yaml and filter the sources list to your field. Those are the manuscripts with a machine-checkable main result. Everything else in preprints/ is unverified by OpenAI's own description.
2. Read the challenge statement before the paper. Open the JSON config for a result, find its challenge module, and read the theorem statement. If the statement is weaker than the paper's abstract, you have learned the most important thing about that manuscript in five minutes.
3. Run Comparator on one result. Pick a single config and run the three commands above. Budget for the Mathlib cache download and the build. One clean pass on your own machine is worth more than any number of stars.
4. Treat unformalized manuscripts as leads. They may be right. Some are probably excellent. But the README tells you some "could have issues," so cite them as "an OpenAI manuscript claims" and not as a result.
5. Watch the catalogue, not the announcement. Formalizations will be added over time. A simple diff of formalization.yaml each week tells you what moved from claim to checked.
Honest limitations
My count of 162 papers and 185 main results comes from one read of the catalogue on October 7. It will change as OpenAI adds formalizations, and the README's "many" may already describe work that has not reached the YAML.
A passing Comparator check proves that a Lean proof matches a Lean statement. It does not prove that the statement captures what the paper's prose claims. That gap is real, and only a human who knows the field can close it. The review: unchecked field is OpenAI saying the same thing.
I have not built the full library or run a Comparator check on every result. I have read the configuration, the schema and the tool's own documentation, and I am describing what they say.
The three-hour figure is an average of compute on an unreleased model, expressed in ChatGPT Pro terms. It is not a price, and you cannot reproduce it.
And the repository is an output dump, not a research process. You get the manuscripts and 10 reasoning summaries, not the 4,000 prompts or the misses. The 722 survivors tell you what the model got to; they do not tell you how often it failed.
Read it like a referee
The release invites two lazy readings. One treats 722 as a count of new theorems. The other dismisses the whole thing as unverified AI output. Neither survives a look at the lean/ folder. OpenAI has shipped a pile of claims with a small, checkable core and the tools to check it.
So check it. Pick one result in your field, read its challenge statement, run Comparator, and see what holds. That is how a repository full of machine-written math turns into something you can actually cite.
Sources: openai/math README, openai/math formalization catalogue, Comparator challenges README, leanprover/comparator, OpenAI announcement, Trendshift.
Medium metadata
- Title: OpenAI's Math Repo Holds 722 Manuscripts, and Its Own Catalogue Formalizes a Fraction of Them
- Subtitle: How to read openai/math: start with the papers that have a machine-checked main result, run Comparator yourself, and treat the rest as leads
- Tags: OpenAI, Mathematics, Lean, Artificial Intelligence, Open Source
- Canonical: fervorai.dev