What's in OpenAI's math release, and what checking it would take

In short

1. Where Lean applies, trust moves from the proof to the statement. Comparator checks each Lean proof against a challenge statement using only the standard axioms. What is left for a person is whether that statement says what the paper claims.
2. “Has Lean” does not mean the headline is checked. 245 families have a Lean scope note, but only 223 cover the headline result. OpenAI’s own notes say so for the rest.
3. Expect errors. The titles include results that would each be among the most important of the decade, in manuscripts dated across 45 days. 3 manuscripts were withdrawn the day after the first release.
4. Risk is concentrated. 388 of 721 manuscripts build on other manuscripts in the release. The six that the most others depend on sit in one cluster, and 5 of those six have no Lean backing.
5. Review is expensive. A conventional expert read comes to roughly 78 expert-years in the mid case of a deliberately simple model.

What was released

The release groups 721 current manuscripts into 373 result families across 17 fields. 205 families are a single manuscript; the largest has 14. Together they run to 34,795 pages and 18,051,031 words, a median of 502 words per page. Most manuscripts are 10–49 pages long (461 of 721), and 21 run past 150.

Theoretical computer science has the most families (41). Probability and statistical mechanics has the most pages: 7,232 across 29 families.

The manuscripts are dated between September 10 and October 25, 2026. 446 of them carry a date in the three days from September 23 to 25.

Releases so far

Source: history.json. Withdrawn counts are cumulative.

How much a machine has checked

For a Lean-backed family, OpenAI ships a challenge statement and a proof. Comparator then checks that the proof proves exactly that statement, using only the axioms its configuration allows. A static scan of the library finds nothing that would undercut this:

Source: lean.json. These are static scans; nothing was compiled and Comparator was not run.

Coverage is the harder question. OpenAI publishes a scope note for each formalization, and those notes sort the families into four groups: 149 with the headline result formalized, 74 with the headline formalized but side results excluded, 22 where only a partial or supporting result is formalized, and 128 with no Lean at all. Among the 54 landmark families, 17 have no Lean.

The statement is now the thing to check

Once Comparator accepts a proof, trust comes down to whether the challenge statement means what the paper claims. Statements vary enormously. Irrationality of Catalan’s constant (family 005) is a 7-line statement over Mathlib, backed by 539,808 lines of proof. The disproof of the Exponential Time Hypothesis (378) needs 160 lines because it defines its own machine model and CNF encoding, and that model is what a reviewer has to audit. The median Lean-backed family has a 74-line statement.

The proof is almost always far longer. In the median family it is about 338 times the length of the statement, and in 195 of 245 families it is at least 100 times.

The outlier on the right is the Hodge conjecture for CM abelian varieties (032), formalized in the October 26 update. Its challenge theorem is short, but it imports a statement library adapted from the community HodgeConjecture project, so the statement a reader must trust is 33,436 lines, the largest in the catalogue (the next is 17,381). The proof is 147,367 lines.

Formalized does not always mean the headline

OpenAI’s scope notes are candid about this. Five of the 22 partial families were read in full; in each, the note itself says the Lean statement is weaker than the paper’s claim.

Why to expect errors

The landmark titles include:

• 378 Disproof of the Exponential Time Hypothesis
• 103 Derandomization of logarithmic space: L=RL=BPL
• 102 The Unique Games Conjecture and optimal approximation thresholds
• 288 Kadison's similarity conjecture
• 287 All nonabelian free group factors are isomorphic
• 304 The Hilbert–Smith conjecture in every dimension
• 004 Hilbert's tenth problem over ℚ

Any one of these would be a major result. Together they amount to decades of ordinary progress, written up in manuscripts dated across 45 days. Long unrefereed manuscripts usually contain errors, and this release has already had some. On October 7, the day after the first release, OpenAI withdrew 3 manuscripts after a sign error in “Algebraicity of Weil classes on split abelian eightfolds” broke two papers that depended on it. One of them was “The rational Hodge conjecture for products of K3 surfaces”; family 032 now covers CM abelian varieties only. 27 current manuscripts carry version notes, and 70 families are disproofs or counterexamples by their titles.

Some of this is already being handled in the open. For the ETH disproof, OpenAI says an independent group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams will examine the proof.

Prior work matters too. Family 074 includes “The Kakeya maximal conjecture in three dimensions”. Hong Wang and Joshua Zahl proved the Kakeya set conjecture in three dimensions in 2025, so the manuscript’s new content is the stronger maximal-function statement, and a reviewer’s first job is to separate what is new from what is known.

How the results depend on each other

Counting citations between current manuscripts, through OAI: keys and repository URLs, gives 595 links. 388 of 721 manuscripts cite at least one other manuscript in the release, none of them refereed. The longest chain runs through 10 manuscripts.

The most depended-on manuscripts all sit in one cluster: Iitaka subadditivity, abundance and minimal models (families 033, 034 and 036). Each has 29–30 manuscripts building on it, directly or through others, and 5 of the six have no Lean backing of their own. Family 033 does have headline Lean, through a different manuscript.

1. 30Projective Hodge lines and ordinary Iitaka subadditivityFamily 033 · cited directly by 2No Lean for this manuscript
2. 29Log abundance in characteristic zeroFamily 034 · cited directly by 16No Lean for this manuscript
3. 29Orbifold and logarithmic Iitaka subadditivityFamily 033 · cited directly by 7No Lean for this manuscript
4. 29Minimal models and Mori fibre spaces for generalized log canonical Q-pairsFamily 036 · cited directly by 5No Lean for this manuscript
5. 29The reverse logarithmic Kodaira inequality and additivityFamily 033 · cited directly by 2Lean-backed
6. 29Logarithmic Kodaira dimension and whole-fiber variationFamily 033 · cited directly by 1No Lean for this manuscript

Source: papers_summary.json (top_hubs). The count is transitive dependents.

What review would cost

A simple model puts the expert time for a conventional read at 66,680 hours in the low case, 124,619 in the mid case and 182,569 in the high case. At 1,600 hours per expert-year, the mid case is about 78 expert-years. These are planning numbers, not measurements; the model is in the method section.

One family distorts the per-family figures. The model charges statement lines linearly, so Hodge for CM abelian varieties (032) becomes the most expensive family at 5,771 mid-case hours, about 4,012 of them for its statement audit. That probably overstates it: most of those lines are human-written definitions adapted from an existing project, not model output.

Where to look first

The priority score rewards significant results, results other families build on, and results Lean does not already cover, and divides by the hours a review would take. A high score means a cheap check that settles a lot. The table starts with the 25 highest; filter or sort it to explore the rest.

Source: families.json. Dependents counts the families that build on it, directly or through others. Hours are the mid case.

Method, judgment calls and limits

The analysis reads the repository at commit 7ef5c0cc5: each family’s linked main PDF, the manuscripts’ TeX and bibliography files, the Lean library and its scope notes. It measures size, field mix, Lean coverage, citation structure and estimated review cost. It does not check whether any proof is correct.

Judgment calls

• Landmark tier. A hand-picked list of 54 families whose problems are widely known outside their subfield. This is subjective. Named means the title mentions a conjecture, problem, hypothesis, question, a person’s name or a counterexample. Technical is everything else.
• Lean status. A phrase match on OpenAI’s scope notes, corrected by hand: families 107, 125 and 325 were false positives, and 229 and 290 were added as gaps. Expect a few families to be misfiled.
• Review hours. Pages × 1, 2 or 3 hours per page (low, mid, high) × a density factor (words per page over the median, clipped to 0.7–1.5) × reviewers (3 for landmark, 2 for named, 1.5 for technical) × a discount for Lean-backed papers (0.5 headline, 0.7 side results excluded, 0.9 partial). Add statement-audit time of statement lines ÷ 25 × reviewers. One expert-year is 1,600 hours.
• Priority. 1000 × tier weight (10, 3 or 1) × (1 + 0.5 × families built on it) × unverified share (1 for no Lean or partial, 0.5 for side results excluded, 0.25 for headline) ÷ mid-case hours.
• Disproofs are identified by title, so the count of 70 is approximate.

Limits

• Comparator was not run and nothing was compiled. The zero counts for sorry, axioms and unsafe code come from static scans with comments stripped.
• Reference counts come from .bib files, which can include unused entries. Citations inside the release count only OAI: keys and repository URLs.
• Chain lengths are lower bounds. Companion papers often cite each other, and the analysis cuts each such cycle where it finds it.
• Page counts use each family’s linked main PDF.
• Dates come from directory names, which are write-up or release dates, not dates of discovery.

Sources and attribution

The source repository, openai/math, is published under the Apache-2.0 licence. This page links to it at a fixed commit and does not rehost any manuscript. Quotations from scope notes are verbatim and link to the file they come from. The figures are as of the October 26, 2026 release and will drift as OpenAI updates the repository.

Corrections are welcome: email me.