About 42% of the top-line results in OpenAI's new math collection are formalized in Lean, according to the repository's own README. The rest are claims waiting on human readers. That number gets lost under the Riemann headlines, so this article sorts out what "verified" covers in this release and what it does not.
OpenAI published the collection on October 6, 2026, from an internal model nobody outside the company can use. I worked from the README, reporting by Qz, Gadget Review and FourWeekMBA, and a YouTube breakdown of the release. I did not check any proof myself. Nearly all readers can't.
What OpenAI Published on October 6
The launch coverage says 722 papers grouped into 372 families, spanning number theory, algebraic geometry and more. A family is a principal result plus companion arguments, consequences or alternative proofs. The README says the model was posed about 4,000 problems, and each kept result used roughly 3 hours of ChatGPT Pro thinking compute on average.
Two results got special handling. The README names the Riemann zeta zero-free region work and a Hodge conjecture proof for CM abelian varieties as exceptions to the standard procedure. It also says the write-up for a related Re(s) > 11/12 result was edited by humans for readability.
OpenAI is direct about the status. The README says the results sit at different stages of verification, not all have Lean formalizations, and some unformalized results could have issues. Fixes are promised "quickly." No dates are given for either the fixes or further Lean files.
What Lean Checks, and What It Does Not
Lean is a proof assistant. A small kernel accepts or rejects each logical step. Its creator Leonardo de Moura has described the appeal in a university talk abstract: with a machine-checked proof, "you do not need to trust the author."
That is a strong guarantee about logic. It is a narrow one about everything else. Gadget Review points out that Lean confirms formal steps compile from stated premises, but cannot confirm novelty, significance, or that the problem was framed correctly. A Lean file proves the statement someone wrote into it. A reader still has to confirm that statement matches the claim in the paper's title.
Human checking has its own record. Terence Tao verified an AI-supplied proof by hand rather than formalizing it earlier this year, which I covered in my breakdown of Tao's Bernstein paper. That was one inequality. The OpenAI release is hundreds of papers.
The Riemann Result Is a 7/8 Half-Plane, Not the Hypothesis
The headline paper is titled "The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re s > 7/8." It runs about 200 pages and is dated September 30, per a Japanese write-up of the release. The result says no nontrivial zero of the zeta function has a real part above 7/8. The Riemann hypothesis says every one of them sits exactly at 1/2.
Those are different claims. The term "quasi-Riemann hypothesis" is used in the literature for a zero-free half-plane beyond some bound below 1, as the American Institute of Mathematics notes. Some outlets still wrote that the hypothesis itself was proven. It was not.
A third-party summary says the 7/8 result has a Lean formalization in the catalogue. That is the best-supported claim in the release. The repo also contains a scope-of-formalization document for it, and I have not read it. What exactly Lean covers there is worth checking before anyone repeats "machine-verified Riemann."
Limit 1: Only Part of the Collection Has a Lean Proof
Three figures circulate for "how much is Lean-checked." They measure different things, so they do not contradict each other.
| Measure | Figure | Source |
|---|---|---|
| Top-line results formalized | About 42% | OpenAI README |
| Families with a linked Lean page | 235 of 372 | FourWeekMBA count of CONTENTS.md |
| Papers with a formalized main result | 162 of 722 (22.4%) | FourWeekMBA count of lean/formalization.yaml |
A family can have a Lean page while some of its companion papers have none, which is why 235 families and 162 papers can both be true. The two FourWeekMBA counts are one outlet's reading of repo files, not OpenAI statements. The repo's formalization catalogue is the place to confirm them.
Limits 2 and 3: No Model Access, No Prompts
The model is unreleased. Mathematicians cannot rerun a result to see whether it reproduces. MIT's Andrew Sutherland, as relayed in the YouTube breakdown, says the one-agent, one-prompt claims stay unverified until the model is out. OpenAI promises a "responsible release" but gave no date.
A September 29 advisory group at the Institute for Advanced Study, which includes Fields Medalists Timothy Gowers, Martin Hairer and Edward Witten, asked labs to disclose the model, prompts, reasoning, time and cost, and to use computer-checked proofs and storage no AI company controls. Qz reports OpenAI followed the recommendations except one: it will keep testing frontier problems on proprietary models.
What OpenAI did share: 10 reasoning summaries, the average compute, and the problem count. What it did not, per the video: prompts and per-result costs. The repository is also hosted by OpenAI. The README says it is exploring community-hosted options, with no timeline.
My Take
Read the README, not the headlines. It says some results could have issues. That sentence is more useful than any of the 722 titles.
The Lean numbers are decent for a first drop. About 42% formalized on day one is not nothing. But a formalized main result and a verified paper are different objects, and the gap between them is where the arguments will happen.
A proof without a Lean file should be read as a draft.
- The Riemann paper claims a zero-free region for Re s > 7/8. The hypothesis itself is unproven.
- OpenAI's README puts Lean coverage at about 42% of top-line results.
- Lean checks logic, not significance or whether the formal statement matches the claim.
- The model, the prompts and per-result costs are not public.
FAQ
Did OpenAI solve the Riemann hypothesis?
No. The paper claims no nontrivial zeros exist with real part above 7/8. The hypothesis requires all of them to sit at 1/2.
What is the quasi-Riemann hypothesis?
It is a weaker statement: the zeta function has no zeros in a half-plane beyond some bound below 1. OpenAI's paper sets that bound at 7/8.
What does Lean-verified mean for an AI-written proof?
A computer accepted every logical step of a formal statement. It does not say the result is important or that the formal statement matches the paper's claim.
Are OpenAI's math papers peer reviewed?
Nothing in the release indicates that. The files sit in a preprints directory on GitHub, and OpenAI says unformalized results could have issues. Independent checking has only started.
Conclusion
The release is real, public and checkable in part. The Lean files can be run today by anyone with the repo. The rest depends on mathematicians reading hundreds of papers without access to the model that wrote them. If a lab publishes 700 proofs and only a minority arrive with a machine check, who does the checking, and how long should everyone else wait before citing the rest?
0 Comments