OpenAI Mathematics: 722 AI Manuscripts, 162 Formalized in Lean

What OpenAI released on October 6, 2026

On October 6, 2026, OpenAI published a catalogue of mathematical results produced by an unreleased internal model: 722 manuscripts grouped into 372 families, in a public GitHub repository. As of October 7, the repository's own catalogue lists 162 of those papers as having a main result formalized in Lean, a language in which a computer can check a proof. The other 560 have no formalized main result listed, and OpenAI says some of the unformalized results could have issues.

That split matters more than the headline count. A manuscript, a machine-checked proof and a result that mathematicians understand and accept are three different things, and this release contains a lot of the first, some of the second and makes no claim to the third yet.

What is in the openai/math repository

Everything sits in the openai/math repository on GitHub. A family groups related papers: a principal result plus companion arguments, consequences or alternative proofs. Each family is classified by mathematical discipline.

The ten reasoning summaries give a sense of the range. The subjects below are the titles OpenAI uses; the field labels are added here for orientation and are not a judgement on any result.

OpenAI says it will keep the public release history: corrections and revisions are recorded as new versions, earlier versions stay accessible, and each manuscript directory carries its own BibTeX block for citation.

Which model produced the results, and can you use it?

No, you cannot use it, and it has no public name. The README calls it an unreleased internal OpenAI model. The October 6 post ties it to the model behind OpenAI's Navier–Stokes announcement, which the company described in September as in training since August 28 and significantly more capable than GPT-6 Astra.

• Availability: OpenAI says it is working to release the model responsibly. There is no date, no product tier and no API access.
• Procedure: the vast majority of results came from one fixed procedure. Two exceptions are named: work on a zero-free region for the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties. One zeta write-up was also edited by humans for readability.
• Cost: on average, each result used compute equivalent to about three hours of ChatGPT Pro thinking with that model.
• Hit rate: the model was posed approximately 4,000 problems, and 372 families were published. That is roughly one family per eleven problems, but it is not a clean success rate: OpenAI filtered for significance, and some results build on earlier outputs of the same model.

Are the proofs verified? What Lean does and does not check

Some are machine-checked, most are not, and none has been through peer review according to the release. It helps to keep three levels apart:

1. A manuscript exists. True for all 722. The README states that the collection is at different stages of verification and that some unformalized results could have issues.
2. A formal proof exists. The formalization.yaml catalogue lists 162 papers with a formalized main result, covering 185 main-result declarations across 178 Comparator challenge files. The catalogue describes its own scope as partial progress.
3. Humans understand and accept it. Not claimed. The catalogue's review status reads unchecked, and its automation method reads agent.

A Lean proof is strong evidence of one specific thing: every step from the stated definitions to the stated theorem was accepted by Lean's checker. The formal library here builds on mathlib and 29 other imported libraries and tools, including community projects such as PrimeNumberTheoremAnd and carleson.

The second row is where formal proofs most often disappoint: a correct proof of a slightly different statement still passes. The third and fourth rows are not hypothetical either. When OpenAI published ten results in August, the criticism that followed, reported by Scientific American, was about credit for earlier work, a question a proof checker has no opinion on.

How to check one of the Lean proofs yourself

The repository uses Comparator, a tool from the Lean project that checks a formal proof against a fixed challenge file, so the statement being proved is pinned down separately from the proof. The README asks you to install comparator, landrun and lean4export, put them on your PATH, and run from the lean/ directory:

git clone https://github.com/openai/math.git
cd math/lean
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

Three practical notes from the repository's own documentation:

• The formalizations live in one large library. Compile small portions at a time instead of the whole thing.
• A full build can fail on Linux when vm.max_map_count is too low. The documented workaround is building Lean with the CMake option -DMMAP=OFF.
• Swap the JSON file for any other entry in ComparatorChallenges/ to check a different result.

A pass tells you the proof matches that challenge statement. Reading the challenge statement to see whether it says what the paper claims is still your job, and it is the part that needs a specialist.

How this fits with OpenAI's Navier–Stokes claim

The October release is the latest step in a sequence that started in the summer.

The Navier–Stokes post claimed that a smoothly forced three-dimensional fluid starting at rest can develop a singularity in finite time. OpenAI said the group of agents that found it ran on the order of 10,000 agents concurrently, arrived at the result about 88 hours after launch, and needed a further 17 hours for Lean formalization. It also said it does not intend to claim the prize.

Put next to that, the October batch is a different kind of effort: about three hours of Pro-level thinking per result instead of thousands of agents for days. Volume at low cost per result is the new part of this release.

What mathematicians asked for versus what OpenAI shipped

OpenAI says it shaped this release with advice from the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), an independent group hosted at the Institute for Advanced Study. The group's September 29 recommendations draw on more than 600 survey replies from mathematicians, and they open with a blunt position: the group does not endorse testing advanced problems on proprietary models and asks labs to stop. The recommendations are for the situation as it is.

The status column is an editorial reading of OpenAI's post, the README and the formalization catalogue, not of all 722 manuscripts.

The release is more inspectable than a press announcement and well short of how a mathematician would publish. The attribution row deserves the most attention, because it is the one that caused the dispute in August and the one OpenAI itself lists as unfinished.

What this means if you build products on AI

Nothing in your stack changes this week. The model is not available, and a theorem prover is not what most business software needs. What carries over is the working pattern.

• Generation got cheap; checking is the scarce part. Roughly 4,000 attempts were filtered down to 372 families, and only the Lean-checked subset comes with machine evidence. In software the equivalent gate is a test suite, a type checker, a schema validator or an evaluation set. An agent's output is not done until something other than the agent has checked it.
• A checker is only as good as the statement it checks. A proof of the wrong theorem passes Lean. Code that passes tests written against the wrong requirement ships the wrong behaviour. Writing the statement, or the spec, stays a human job.
• Volume moves the bottleneck to review. 722 manuscripts arrived faster than anyone can read them. The same thing happens when an agent opens more pull requests or drafts more reports than a team can review. Plan review capacity before you scale output.
• Disclosure is part of the deliverable. What was tried, what failed and what it cost are what let an outsider trust the result. The same applies to an AI feature you hand to a client or a regulator.

If you are scoping a chatbot, a data agent or a report-generation agent, decide what checks its output before you pick a model. That kind of build is what Netalith's AI development service covers.

The bottom line

OpenAI's mathematics release is large, cheap per result and partly machine-checked: 722 manuscripts, 162 with a formalized main result so far, from a model nobody outside the company can run. Whether the results are correct, new and properly credited will be settled by mathematicians over months, and the number to watch is how fast the formalized count and the independent reviews catch up with the manuscript count.

If you want AI output in your own product that someone can actually verify, request a free quote from Netalith and describe what you need checked.