# OpenAI publishes 722 math manuscripts from an unreleased model, with Lean proofs for part of the set

The release covers 372 result families drawn from about 4,000 attempted problems, and its own repository warns that results without formal proofs could contain errors.

- Published: 2026-10-07T06:04:58.881Z
- Canonical: https://polylog.news/ai/2026-10-07/openai-publishes-722-math-manuscripts-from-an-unreleased-mod
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [OpenAI News](https://openai.com/index/sharing-ai-progress-in-mathematics)

OpenAI on October 6 [released new results on open mathematics problems](https://openai.com/index/sharing-ai-progress-in-mathematics) produced by an internal frontier model it has not released. The company published 722 manuscripts, grouped into 372 families, on GitHub under an Apache-2.0 license. The release includes a library of proofs formalized in Lean, the proof assistant that checks each step by machine. [Interesting Engineering reports](https://interestingengineering.com/ai-robotics/openai-largest-math-release-lean-proofs) that the model attempted roughly 4,000 problems across pure mathematics, theoretical computer science and mathematical physics.

The important detail for verification is coverage. Lean formalization covers "many, but not all" of the results, and the repository warns that unformalized results could contain errors. [One independent count](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) of the repository's Lean scope pages matched 235 of the 372 families, about 63%. That figure counts families with associated Lean documentation. It does not count fully checked theorems. Even a complete Lean proof only verifies the formal statement, so a reviewer still has to confirm that the formal statement matches the claim in the paper. The same analysis says each accepted result used about three hours of ChatGPT Pro thinking compute on average.

The release follows OpenAI's [September claim](https://openai.com/index/navier-stokes-solution/) of a solution to the Navier-Stokes Millennium Prize Problem. With that claim the company announced a mathematics advisory group hosted by the Institute for Advanced Study. [NPR reported](https://www.npr.org/2026/09/22/nx-s1-5968588/openai-navier-stokes-problem-mathematicians-learn-little) that mathematicians said they had learned little from that result. Early reaction to this release has been [skeptical about refereeing capacity and credit](https://startupfortune.com/openai-drops-722-ai-math-proofs-and-mathematicians-are-not-impressed/). No group of human referees can review 722 manuscripts quickly, and mathematician Terence Tao has warned that machine-generated proofs can appear correct while containing subtle errors.

What is verified is narrow. Any Lean file that compiles against the stated definitions is a checked proof of that formal statement. The significance, novelty and correctness of the remaining results are OpenAI's assertions until mathematicians review them.

## What this means

Lean is the mechanism that turns a capability claim into a cheap check. A lab that ships formal proofs moves the burden of verification from human referees to a type checker. That favors labs with large reasoning-compute budgets and teams that write autoformalization tooling. The exposed parties are human-refereed journals and benchmark makers whose fixed problem sets cannot measure research-level output. Investors already priced in strong benchmark results in math. The new element is volume: hundreds of claimed results produced at a disclosed compute cost per result. The common view treats the count as the headline. The more informative number is the share of results that are formally checked and also judged non-trivial by working mathematicians. The closest precedent is DeepMind's AlphaProof work at the 2024 International Mathematical Olympiad. That work was trusted because its proofs were formal, and the debate moved quickly to whether the problems were representative. The likelier outcome is that within months the field will settle on formal coverage as the required standard for credit on AI-generated math claims. Unformalized claims will be widely discounted, and other labs will publish their own formal-proof results to compete. One development would prove this read wrong: if referees find serious errors in the Lean-checked subset because statements were misformalized. Credibility would then shift back to human review.

## What to watch

- The first independent referee reports on the unformalized manuscripts. Their error rate will show whether OpenAI's results without formal proofs are reliable.
- Whether the Institute for Advanced Study advisory group publishes a review process or a list of results it considers significant. That would turn a vendor's claims into results the field itself endorses.
- Whether Google DeepMind or Anthropic answer with their own formally verified research-level results. That would show research-level math has become a front in the competition among labs.