OpenAI's 722 Math Papers: The Proofs Can Be Machine-Checked. The Statements Are Still on Us.

OpenAI’s announcement on 6 October takes about two minutes to read. It says the company is releasing “a broad range of new mathematical results produced by an internal frontier model.” It says it consulted the advisory group at the Institute for Advanced Study that I wrote about in September. And it says it is “sharing formalizations of many of the proofs in Lean.” The post gives no manuscript count. For the numbers you have to open the GitHub repository it links to, and the repository is unusually frank.

Its README says the catalogue “contains 722 manuscripts organized into 372 families.” It says the vast majority came from “an unreleased internal OpenAI model” using “three hours of ChatGPT Pro thinking compute” per result on average, and that the model “was posed approximately 4,000 problems” over the evaluation. Then it says two things the announcement states less plainly: “Not all have accompanying Lean formalizations,” and “Some of the unformalized results could have issues.”

So the question everyone is asking, whether these results are right, splits in two. The repository answers half of it in a way mathematics has never had at this scale. The other half it leaves open, and it says so in a field most people won’t scroll to.

What the Lean covers

The formal side of the release is catalogued in lean/formalization.yaml, which opens with a comment calling itself a “Catalog of papers with a formalized main result.” It lists 162 papers. That is 22% of the 722. The other 560 have no machine check of their main result at all. Measured by families instead of papers, the picture looks better: 235 of the 372 families link to a Lean page describing what was formalized. A family can have a Lean page without every manuscript in it being covered, though, so the paper count is the one to use.

How much of OpenAI's math release has a machine check Three part-of-whole bars, each its own 100 percent. Manuscripts: 162 of 722 have a formalized main result, 560 do not. Result families: 235 of 372 link to a Lean page, 137 do not. Formalization catalogue review status: unchecked for all 162 catalogued papers. Source: openai/math repository, 6 October 2026, counted 7 October 2026. OPENAI/MATH · WHAT CARRIES A MACHINE CHECK · EACH BAR IS ITS OWN 100% Manuscripts Result families Catalogue review 722 papers 372 families 162 formalized papers 162 of 722 papers with a formalized main result — lean/formalization.yaml, 6 Oct 2026 235 of 372 families link a Lean page — CONTENTS.md, 6 Oct 2026 560 of 722 papers without a formalized main result 137 of 372 families without a Lean page review: status: unchecked — lean/formalization.yaml 162 formalized (22%) 560 not (78%) 235 with a Lean page (63%) 137 without review: status: "unchecked" Counts from the repository as published 6 Oct 2026, read 7 Oct. A Lean page can cover part of a family.
The paper count is the right denominator: fewer than one paper in four carries a formal check of its main result, and the catalogue that lists those papers marks their review as unchecked.

For those 162 papers, the check means something. The Lean library is enormous: by my count, roughly 25.9 million lines across 121,734 files, about twice the size of the Fermat formalization I wrote about in September. A text search of those files finds no sorry and no admit, the two usual ways of leaving a hole in a Lean proof. That is a search, not a build, and I haven’t compiled 25.9 million lines. But OpenAI has also set the release up so that anyone with a Linux machine, the right sandboxing tools and enough compute can. Each formalized result comes with a challenge for Comparator, the Lean community’s tool that checks that a proof module proves exactly a stated theorem, using only an approved list of axioms. For the headline result, those axioms are the three standard ones (propext, Quot.sound, Classical.choice) and nothing else.

That design answers the old objection to formal proofs, that a proof assistant just moves the trust to whoever wrote the proof script. Here the proof can be as long and as machine-written as it likes. The kernel either accepts it against the challenge statement or it doesn’t.

The theorem that fits in two lines

The result getting most of the attention is result family 003, titled “The quasi-Riemann hypothesis.” The term has a standard meaning that predates this release. Bhowmik and Ruzsa, writing in 2018, use it for the assertion that the real parts of the zeta function’s nontrivial zeros are strictly less than 1, which I read in the usual sense of staying below some fixed constant less than 1. The Riemann hypothesis puts every one of them on the line \(\operatorname{Re} s = 1/2\). The quasi version asks only for a fixed vertical line short of 1 that no zero crosses. It sounds modest, and it isn’t. Every previously published unconditional zero-free region inside the critical strip that I know of, from de la Vallée Poussin’s around 1899 to the explicit regions of Mossinghoff, Trudgian and Yang in 2022, narrows toward \(\operatorname{Re} s = 1\) as you go up the strip. None of them is a half-plane.

OpenAI’s manuscript, dated 30 September, claims the half-plane \(\operatorname{Re} s > 7/8\) for zeta and for every Dirichlet L-function. A companion dated 5 October gives a different proof of the weaker 11/12. The README notes that this work was an exception to the standard procedure, and that the 11/12 write-up “was human edited for readability.”

The critical strip: classical zero-free region versus the claimed half-plane Schematic of the critical strip from real part 0 to 1, with height t increasing upward. The Riemann hypothesis line sits at real part one half. The classical zero-free region, de la Vallée Poussin around 1899, is a sliver hugging the line real part 1 that narrows as t grows. OpenAI's claimed zero-free half-plane begins at real part 7/8 and has constant width at every height; a companion proof gives real part 11/12. Schematic, not to scale in t. CRITICAL STRIP · 0 < RE S < 1 · SCHEMATIC Claimed zero-free half-plane Re s > 7/8 — OpenAI manuscript, 30 Sep 2026 Classical zero-free region 1 − σ ≥ C/log t — de la Vallée Poussin, c. 1899 height t 0 1/2 7/8 11/12 1 Riemann hypothesis: every zero on this line Claimed: no zeros right of 7/8, at any height Classical region (c. 1899): a sliver that thins as t grows Shaded band is constant width; the dark sliver at the right edge narrows with height. The 11/12 line is the companion proof.
What "quasi" means here. The claim is a fixed band at the right edge of the strip, where every earlier published unconditional region inside the strip that I know of is a sliver that thins with height.

This result is about as checkable as a frontier claim gets. The Comparator challenge for the zeta case is this:

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0

Anyone who reads Lean can read that statement quickly, along with the Mathlib definition it relies on. riemannZeta is Mathlib’s existing definition, not one written for the release. Up to Mathlib’s convention for the value at the pole \(s = 1\), the statement says what the paper’s abstract says. If the module proving it builds and Comparator accepts it, the zeta part of the headline holds, with no referee needed. Levent Alpöge, a mathematician at Anthropic, was quoted in Latent Space’s 7 October roundup praising the “quasiriemann and no Siegel zeroes” results in strong terms. That reaction makes sense if the Lean holds, and the Lean is what will settle it.

Where the trust sits

The checklist for this situation was written down eleven years ago. Thomas Hales’s proof of the Kepler conjecture was finished with Samuel Ferguson in 1998. It was not published in full until 2006, because the referees could not certify its computer calculations. Jeffrey Lagarias, describing that review, wrote that the work left the referees with “a strong degree of conviction” in the method, and Hales’s own account adds that “the proof was published without complete certification from the referees.” Hales then led the Flyspeck formalization, announced in 2003 and written up as complete in 2015. The 2015 paper that closes the Flyspeck project has a section on auditing a formal proof. It says a proof assistant “largely cuts the mathematical referees out,” and then lists what is still left for humans: run the scripts, examine the definitions to confirm “the meaning of the final theorem,” ask “were any unapproved axioms added,” and audit the system itself. The middle question, as the paper puts it, is “did the right theorem get formalized?”

The Flyspeck audit checklist against what OpenAI's repository supplies Four audit steps from Hales et al. 2015, each paired with what the openai/math repository supplies. Run the scripts to produce the theorem: Comparator challenge configs exist, and no public build report found 7 Oct. No unapproved axioms: the permitted list is propext, Quot.sound, Classical.choice. Audit the system: Lean kernel and Comparator, community tools. Did the right theorem get formalized: catalogue review status unchecked, the one step that needs a mathematician per paper. AUDITING A FORMAL PROOF · HALES ET AL. 2015 vs OPENAI/MATH 2026 AUDIT STEP (FLYSPECK, 2015) WHAT THE REPOSITORY SUPPLIES Run the scripts; get the claimed theorem No unapproved axioms added Audit the proof system itself Did the right theorem get formalized? Comparator challenge per main result; no public build report found 7 Oct Permitted: propext, Quot.sound, Classical.choice Lean kernel and Comparator (community tools) Catalogue review: "unchecked" needs a reader per paper Steps paraphrased from Hales et al., Forum of Mathematics, Pi (2017), §10. Repository state as of 7 Oct 2026.
Three of the four audit steps are mechanical. The release sets up the first two to be run and leans on community tools for the third. The fourth needs a mathematician to read each statement against its paper, and I found no public sign-off on that as of 7 October.

OpenAI’s release sets up three of the four to be run mechanically, though for the third it relies on community tools rather than doing anything itself. The fourth is where the open question is, and the repository says so itself. The formalization catalogue carries a review field, and for the whole collection it reads status: unchecked. Its automation field lists the method as agent. Its scope reads “Partial progress.” Nothing there claims more than the evidence supports. It just isn’t the reassurance some coverage took from it. Scientific American’s same-day report said many results “have already been verified in Lean” and “are therefore all but certain to be correct.” For the zeta statement above, I think that is close to fair. For a theorem about spin glasses or free group factors, whose Lean statement may need dozens of bespoke definitions, “verified in Lean” means the proof matches the statement. Whether the statement matches the mathematics is a separate check, and I could find no public sign-off on it as of 7 October.

The repository’s own Lean pages already mark where the formal coverage stops. 31 of the 235 scope documents say some part of the paper is “not included.” The quasi-Riemann page is typical. It covers the 7/8 paper and a companion paper on Landau–Siegel zeros, and says plainly: “The paper’s later applications are not included.” The alternate 11/12 proof is not among the papers it lists, so that write-up, the one the README says a human edited, stands on its own. None of this is a defect. A careful catalogue looks like this. But every one of those boundaries is a place where a reader has to compare what the paper claims with what the Lean states, and no kernel does that comparison for them.

Most of the release has no check at all

All of that concerns the 162. The other 560 manuscripts are ordinary mathematics papers by an unusual author, with no kernel behind them. The README’s warning that they “could have issues” is the right default. The pace leaves little time to find out. 369 of the 722 manuscripts are dated 23 or 24 September and 112 are dated 5 October, so a single day’s output would keep a referee reading for months. Scientific American reports that OpenAI’s spokesperson said many of the results are not yet understood by the company’s own mathematicians, and that some might have taken multiple attempts. Andrew Sutherland of MIT, quoted in the same piece, said that until the model is released and people can replicate the results, claims about one-shotting problems with a single agent should be treated “as unverified,” adding: “We should ask for receipts.”

The figure people keep repeating, that the catalogue claims to “fully solve 90 of the top 500 open problems in math,” is not an OpenAI claim. It came from a Hacker News commenter matching the catalogue against proofatlas.ai, a list ranked by having language models compare pairs of problems. It is a count of matches against a model-ranked list. It is not a count of verified results, and I’d leave it out of anything that matters.

On the evidence available today, I would split the release in three. The formalized results whose statements use standard Mathlib objects and fit on a screen, with the zeta half-plane as the clearest case, are the closest thing to settled that AI mathematics has produced. Their status should get firmer within days, since anyone with the tooling and the compute can run the Comparator challenges and publish the result. The formalized results that rest on new definitions are credible but unread, and the reading is the slow part. The 560 papers with no Lean are claims. They came from a model that has clearly gotten good at this, which is a reason to read them. It is not a reason to believe them.

Eleven years ago, the Flyspeck paper said what was left for humans after the machine had done its part. OpenAI has done its part of that list better than anyone has at this scale. What remains is the question that paper said needs a mathematician, asked once for each theorem: is this the right one?

References

  1. OpenAI (2026). Sharing AI progress in mathematics. OpenAI, 6 October 2026.
  2. OpenAI (2026). openai/math repository: README, CONTENTS.md, lean/formalization.yaml, lean/docs/003.md, lean/ComparatorChallenges. GitHub, initial commit 6 October 2026; counts (722 manuscripts, 372 families, 162 formalized papers, 235 Lean pages, manuscript dates, Lean file and line totals, sorry/admit search) are my own, from the repository as read on 7 October 2026.
  3. OpenAI (2026). The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re s > 7/8. Manuscript dated 30 September 2026; companion alternate 11/12 proof, dated 5 October 2026.
  4. leanprover. Comparator. GitHub, checked 7 October 2026.
  5. Howlett, J. (2026). OpenAI unleashes hundreds more math results upon a field already in shock. Scientific American, 6 October 2026.
  6. Latent Space (2026). AINews: Quasi-Riemann Hypothesis. 7 October 2026. Source of the Alpöge quote.
  7. Hacker News (2026). Sharing AI progress in mathematics, discussion thread, 6–7 October 2026. Source of the “90 of the top 500” comment and its proofatlas.ai matching.
  8. Bhowmik, G. and Ruzsa, I. Z. (2018). Average Goldbach and the Quasi-Riemann Hypothesis. Analysis Mathematica 44(1), 51–56. doi:10.1007/s10476-018-0105-4. Dated background for the term.
  9. Wikipedia (2026). Riemann hypothesis: Zero-free regions. Background for de la Vallée Poussin’s region (1899–1900) and the 2022 Mossinghoff–Trudgian–Yang regions; checked 7 October 2026.
  10. Hales, T. et al. (2015/2017). A formal proof of the Kepler conjecture. arXiv:1501.02155, 9 January 2015; Forum of Mathematics, Pi 5 (2017). Dated background: §1 on the 1998 proof and its review, §10 on auditing a formal proof.