OpenAI posted 722 math manuscripts, how many are verified?
OpenAI's math manuscripts went from 722 to 719, and Lean covers 300 of 719. The 372 bundles, 4,000 problems and 242 guides each count a different unit.
Here are the numbers from the coverage: 722 manuscripts, 719 after retractions, 372 result bundles, about 42% with Lean formal proofs, about 4,000 problems given to the model, and 3 hours per result. The trouble is that once these numbers sit side by side in one paragraph, what each one is a share of gets erased. That is why nobody can answer “how many of the 722 are verified?” with a single number.
On Oct 6 (UTC), OpenAI, the maker of ChatGPT, uploaded 722 math manuscripts written by an internal model to the GitHub repository openai/math in one go, under the Apache-2.0 license. This article is a record of reopening the repository’s README, the results list CONTENTS.md, history.md and the Lean folder on Oct 27 and checking the denominator behind each number. Three weeks after release, the repository’s history is still one update entry from Oct 7, and the last commit (Oct 12) was a single setting that automatically locks conversations on new pull requests. It has 15,525 stars and 1,821 forks, so attention is high, but the manuscripts and the Lean code have not changed since Oct 7.
Oct 7, when the denominator became 719
The first denominator changed the day after release. A single sign error in the manuscript “Algebraicity of Weil classes on split abelian eightfolds” broke the stable trace-cancellation argument, and two manuscripts that reused that construction (the Kuga-Satake correspondence for K3 surfaces and the rational Hodge conjecture for products of K3 surfaces) no longer held either, so 3 manuscripts in total were retracted. The retracted manuscripts keep the reason and a link to the previous version.
The 14 revised manuscripts are 6 on Kähler minimal models, 4 on Lipschitz heights, 2 on tame deformations, 1 on box transport and 1 on the BSD formula. The revision to the BSD formula manuscript fixed an outdated sentence that cited an auxiliary manuscript that had already been removed. This episode teaches two lessons about reading the numbers. One is that from now on every ratio has 719 as its denominator, not 722. The other is that manuscripts in the same bundle cite one another, so errors spread in a chain. Whichever manuscript you read, first look at which earlier result it depends on.
An OpenAI spokesperson said the error was found in an internal check. Professor Andrew Sutherland of MIT called the retraction responsible behavior but said it was not enough to win back trust, and Alex Townsend of Cornell said such chain errors are not surprising and he expects more to turn up.
372 counts topics and 719 counts papers
The second number, 372, is not a count of manuscripts. The README calls the unit that groups related manuscripts a “family” and explains that one bundle can hold a main result together with auxiliary arguments, corollaries and alternative proofs. Counting manuscripts per bundle in CONTENTS.md gives an average of 1.9 per bundle, but the distribution is heavily skewed to one side.
The figure below counts the same data with two denominators. The upper bar shows the 372 bundles by bundle size, and the lower bar divides the 719 manuscripts inside those bundles by the same size categories.
Figure 1. 55% of bundles are single-manuscript, but by manuscripts those bundles are only 29%. Bundles of 5 or more are 6% of bundles but 23% of manuscripts
Bundles with just one manuscript are the most common at 205, and there are 22 bundles of 5 or more that hold 162 manuscripts between them. The largest bundle covers logarithmic abundance on compact Kähler spaces (no. 034) with 14 manuscripts, followed by self-avoiding walks on the honeycomb lattice (no. 237) and the spacetime Penrose inequality (no. 260) with 13 each. Reading it as “result bundles on 372 topics” is closer to reality than “722 achievements,” and it is also worth remembering that a few large bundles inflate the manuscript count considerably.
Folder names end with a version date. The dates of the 717 that could be read are spread from Sep 10 to Oct 7, with 547 (about 76%) clustered on Sep 23-27. A folder date cannot be assumed to be the writing date, but it does show that the 722 manuscripts uploaded at once were not all made on the same day and instead piled up over several weeks.
The numerator and denominator of 42%, and four Lean numbers
Lean is a proof tool in which a computer checks every step of a proof, and having a formal proof attached is the strongest basis for the word “verified” in this release. history.md states the ratio as “top-level results 300 / 719, about 42%.” The numerator is top-level results and the denominator is the number of manuscripts. The README itself says the collection mixes results at different stages of verification and that unformalized results may contain problems.
Figure 2 draws the 722 slots at release time, one slot per manuscript. Green is the 300 with Lean attached, gray is the 419 without, and red is the 3 retracted.
Figure 2. Of the 719 in the denominator, 300 have Lean and 419 do not. The numerator 300 is the update log’s value copied as it is
Gray is well over half. The 42% figure is not wrong, but “42% are verified” and “58% are not verified” state the same fact from opposite directions, and headlines usually use only the first.
The Lean-related numbers in the same repository are not a single one. Each file counts a different thing, and the values I counted directly for this article are below.
| Number | Where it was counted | What it counts |
|---|---|---|
| 300 / 719 | The last sentence of history.md |
Top-level results that are formalized; the denominator is the manuscript count |
| 242 | Lines in CONTENTS.md that link a Lean guide |
Bundles with a guide, out of 372 bundles |
| 200 | comparator_config entries in lean/formalization.yaml |
Check configurations registered as main results (189 without duplicates) |
| 173 | sources entries in the same file |
Manuscripts listed in the catalog |
Whichever number you cite, give the file and line as well so readers can count the same value again. The catalog file itself marks its status scope as “partial,” the formalization method as agent, and the review status as “unchecked.” You can count every number above yourself with the commands below, which only download files and read them on screen, installing and changing nothing.
U=https://raw.githubusercontent.com/openai/math/main
curl -s $U/CONTENTS.md | grep -c '^\*\*[0-9][0-9][0-9]\.' # 372 bundles
curl -s $U/CONTENTS.md | grep -c '^ \[' # 719 manuscripts
curl -s $U/CONTENTS.md | grep -c 'lean/docs/' # 242 bundles with a guide
curl -s $U/history.md | grep -o '[0-9]* / [0-9]* = ~[0-9]*%' # 300 / 719 = ~42%
curl -s $U/lean/formalization.yaml | grep -c 'comparator_config' # 200
curl -s $U/lean/formalization.yaml | grep -c '^ - title' # 173The 242 bundles with a guide only indicate that some Lean formalization exists, and do not mean the whole bundle passed machine checking. A guide records how far the formalized statements reach, and that scope is often narrower than the manuscript’s title.
A correct proof can still prove a different statement
Passing Lean does not mean the manuscript’s claim is verified. The machine checks whether a proof is correct, but it does not know whether the statement being proved means the same thing as the manuscript’s claim. That is why the repository uses Comparator, an open-source verification tool from the Lean community. Before a person or a model submits a solution, the verifying side fixes the statement (the challenge file) first, and then checks in a sandbox that the solution file proves the same statement. The check runs in several stages. The two files are compiled in an isolated environment, the modules are extracted and the challenge statement and the solution statement are compared, the check looks for axioms outside an allowlist, and finally the Lean kernel must approve the proof again.
You can look at what a challenge file looks like. The 7/8 result for the Riemann zeta function is a representative one.
import Mathlib
namespace OAI
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
{s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
sorry
end OAIhs is the assumption that the real part of the complex number s is greater than 7/8, and the conclusion is that the zeta function’s value is not 0. sorry is the blank that says the proof lives in the solution-side file. The paired config JSON lists only the name of the module that holds the solution and three allowed axioms (propext, Quot.sound, Classical.choice). The one thing a human has to judge is whether these three lines mean the same as the manuscript’s claim.
Now look at the distance between the headline and this statement. The manuscript’s title is “quasi-Riemann hypothesis,” and the bundle description also says it resolves that. But what the formalized statement confirms is that the Riemann zeta function and all Dirichlet L-functions have no zeros in the region where the real part is greater than 7/8. The Riemann hypothesis says all zeros lie on the line with real part 1/2, so the zero-free region would have to reach right up to just right of 1/2.
Figure 3. Between the formalized zero-free region (above 7/8) and the region the Riemann hypothesis requires (above 1/2), the band from 0.5 to 0.875 is empty
The red band is the region this result does not cover. The auxiliary manuscript in the same bundle gives a different proof for the 11/12 region, which is a narrower region and so weaker than 7/8. The guide 003.md states the scope more narrowly still. Later applications of the manuscript are not part of the formalization, the constant c for Landau-Siegel zeros is not given a value, and real roots are only pushed inside 1 − c/log q rather than excluded across the whole interval (0, 1).
The same distinction shows up in other guides. Put three documents side by side and the formalized statement carries more conditions than the headline.
| Bundle | Headline | Formalization scope stated in the guide |
|---|---|---|
| No. 130 Fourier transform | Exact transform faster than n log n | Formalizes separately a subsequence result in which the cost per coefficient becomes as small as desired over infinitely many lengths, and a uniform result for all lengths. States that the subsequence result makes no claims about all lengths, coefficient size, condition number or bit complexity |
| No. 107 Matrix multiplication | Exponent at most 9/4 | ω ≤ 9/4 over the complex numbers, ω < 2.371054886006746 over all fields. This is arithmetic complexity counting additions, subtractions and multiplications, unrelated to bit complexity or practical crossover sizes |
| No. 102 Unique Games | Proof of the conjecture | Formalizes a deterministic polynomial-time reduction from binary 3SAT to Unique Games instances (value at least 1 − ε if satisfiable, at most δ if not) |
Gaps like this have also been confirmed outside this repository. In a paper posted to arXiv on Oct 6 (2610.08144), Alexander Bastounis (King’s College), Fabian Zircelli and Anders Hansen (Cambridge) cited the Navier-Stokes blow-up proof OpenAI announced in September as a case where AI-translated Lean code does not match the original natural-language proof. Reports say the two disagree in two places, and in one of them the code proves a weaker estimate than the paper. The authors did not claim the original proof is right or wrong, and they point out that even with machine verification, human review is still needed. This case concerns a separate announcement, not a manuscript in openai/math, but it shows from the same angle why a person has to check that statement and code agree.
To run the check yourself, put comparator, landrun and lean4export on your PATH on Linux, then run lake update, lake exe cache get and lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json in that order from the lean/ folder. The library is bundled into one large unit, so the README advises building small parts at a time instead of compiling everything at once, and on Linux the build can fail if vm.max_map_count is low. The repository’s Lean toolchain is version 4.34.1, and Comparator was merged into Lean core starting with 4.35.0.
From 4,000 problems to 372 bundles, the filter ratio is not a success rate
The production process the README describes is one line. Most results were made with the same procedure: the same internal model was given open research problems and used about three hours of ChatGPT Pro-level thinking compute per result on average, and the number of problems posed to the model was about 4,000. The output was organized into bundles and manuscripts and filtered by requiring “an appropriate level of importance,” and what remains is today’s 372 bundles and 719 manuscripts.
Dividing 372 by 4,000 gives about 9% (the editors’ calculation), but this cannot be read as a success rate. The denominator is the number of problems posed to the model, and the numerator is the number of bundles that passed OpenAI’s own importance criterion, so it mixes problems it failed to solve with problems it solved but discarded for falling short of the bar. The 3-hour average is also a per-result average according to the README, so multiplying it by 4,000 to get total compute is not correct.
The README also lists exceptions to the fixed procedure. The work on the zero-free region of the Riemann zeta function and the proof of the Hodge conjecture for CM abelian varieties were not made with this procedure, and the manuscript for the zeta zero-free region Re(s) > 11/12 result was edited by a human for readability. Condensed summaries of the model’s reasoning are attached to only ten bundles, and the model name and prompts are not in the repository. So outside researchers cannot recreate the same results, and Professor Sutherland said, in effect, that it is better not to settle the claim that it was solved in one shot until the model is public and others can reproduce it.
Five Millennium Problems and the distance to the list
The 372 bundles include many named hard problems. Following the bundle descriptions seen earlier, a few of them are: no. 003 the zero-free region 7/8, no. 102 the Unique Games Conjecture, no. 157 a counterexample to Hadwiger’s conjecture (including fractional coloring), no. 004 the negative solution of Hilbert’s tenth problem over the rationals, no. 032 the Hodge conjecture for CM abelian varieties, and no. 109, which claims multiplication of n-bit integers faster than n log n. All of these are claims made in OpenAI’s manuscripts, and of them 003, 102 and 157 have Lean guides while 109, 004 and 032 do not.
The list itself answers the question “were the Riemann hypothesis or the Navier-Stokes equations solved?”
| Millennium Problem | Closest result in the list | Scope of the claim |
|---|---|---|
| Riemann hypothesis | 003 | Zero-free region with real part above 7/8 (the hypothesis is the 1/2 line) |
| Birch and Swinnerton-Dyer conjecture | 002 | Elliptic curves whose Selmer group corank is 0 or 1 (combined with no. 006, a density-1 set of quadratic twists) |
| Hodge conjecture | 032 | Limited to CM abelian varieties |
| Navier-Stokes | 376 | A construction that makes a flow with external forcing perform universal computation |
| P versus NP | Not applicable | Not in the list (Scott Aaronson also noted this in his post) |
No. 376 is not about whether smooth solutions exist. It is a construction in which, starting from rest and applying external forcing, particles in the flow can be made to tell you whether a Turing machine halts. It shares a name with the Millennium Problem but asks a different question.
Six weeks from the declaration to the follow-up post
The argument over the denominator began just before the release. On Sep 11, “Serious Misalignments of AI in Mathematics,” reportedly signed by Fields medalists and others, was posted on Terence Tao’s blog. Its point is that rushing out solutions leaves out explanation, new methods and citations, so mathematics cannot absorb them. On Sep 21, the Advisory Group on Mathematics and AI (AGMAI), hosted by the Institute for Advanced Study (IAS), launched, and its 9 members said they are unpaid and have no decision-making authority over AI companies. On Sep 29, it published guidelines for AI labs releasing mathematical results, reflecting more than 600 survey responses.
Figure 4. The sequence around the release. The spacing between points is equal regardless of the gaps between dates
On release day, Oct 6, AGMAI issued a statement that its role is not to judge the impact of results, and on Oct 25 it posted a follow-up saying that the work of understanding after release should be led by the community and advising labs not to hand results to particular mathematicians in advance.
Reactions split into welcome, caution and opposition. In his Oct 7 post, Scott Aaronson called it one of the great days in the history of mathematics while noting that hardly anyone has understood the results, and said he knew of no direct practical application. Levent Alpöge judged it the most meaningful moment in the history of mathematics but also acknowledged that researchers whose projects were pre-empted could be harmed. Melanie Wood of Harvard pointed out that at the time of release no human understanding of the results existed, and Michael Harris said he would not read these manuscripts. The Human Mathematics Association characterized uploading about 700 files at once as a show of power rather than scholarship and urged mathematicians to stop collaborating. Notably, many of these objections are less about whether the proofs are right than about whether the proofs are understood.
AGMAI’s Sep 29 guidelines are often used as the yardstick for this release. Since the group said whether the guidelines were followed is for the community to judge, the table below is not a verdict but a comparison of each guideline item with the facts confirmed from the repository and reports.
| Guideline item | Facts confirmed from the repository and reports |
|---|---|
| Effort to improve citation and exposition | Each manuscript folder has citation BibTeX and build instructions. Whether prior work is cited sufficiently is an issue where criticism has been raised |
| Post in a repository the lab does not control | Currently a repository in OpenAI’s organization. The README says it is looking into a community-hosted repository |
| Disclose the model, prompts, reasoning records, number of attempts and compute | The model name and prompts are not provided. The 3-hour average, about 4,000 problems and reasoning summaries for ten bundles are disclosed |
| Lean formalization where possible | 300 / 719 (about 42%); the README says more will keep being added |
| Problem selection method and number of attempts | About 4,000 problems and importance-based selection are described in the README |
| Funding to support understanding | OpenAI was reported to have said it would support workshops, conferences and programs |
What the repository says on Oct 27
Gathering what can be read in the repository now, in order of denominator: of the 722 manuscripts released, 719 remain, they sit in 372 bundles, and 55% of bundles have a single manuscript. The share with Lean formal proofs is 300 / 719 per the update log, and the catalog states that formalization is partially complete and that human review is not yet marked. Even among the 242 bundles with a guide, the formalized statements were the parts carrying more conditions than the manuscript title.
The README says it will keep adding formalizations as it gets them, and promises to record retractions and revisions as new versions while keeping earlier versions open. So when you cite a manuscript, use the BibTeX in its folder and write the version date as well. A manuscript with the same title but a different date is a different version, and a retracted manuscript has its reason and an archive link in the folder’s README. If you are told that a result in this repository is “verified,” the fastest order of checks is to find the number in CONTENTS.md, see whether a lean/docs document with the same number exists, and if so read whether the statement in its Scope section means the same as the headline, then check history.md for the retraction and revision dates of that manuscript and of the earlier results it depends on.
