# OpenAI Drops 722 Math Manuscripts from an Unreleased Model — 162 Lean-Checked

Times of AI Desk · 2026-10-07 · Research

[https://timesof.ai/2026/10/openai-math-722-manuscripts-372-families](https://timesof.ai/2026/10/openai-math-722-manuscripts-372-families)

> OpenAI published a GitHub repository of 722 manuscripts in 372 result families from an unreleased internal model. About 4,000 problems were posed; each result averaged roughly three hours of ChatGPT Pro thinking. The formalization catalogue lists 162 papers with a Lean-checked main result. The rest carry OpenAI's own warning that some unformalized work could have issues. AGMAI asked for model, prompt and compute per result; OpenAI is publishing averages and artefacts, not prompts, and says it is not bound by the recommendations.

OpenAI just moved AI mathematics from showcase proofs to industrial volume — and left the field to referee hundreds of claimed results from a model nobody outside the company can run.

On **October 6**, OpenAI published **[openai/math](https://github.com/openai/math)**: **722 manuscripts** grouped into **372 families** of related results, produced by an **internal model it has not released**. The README says the model was posed about **4,000 problems** during the evaluation, and that each result used on average the equivalent of about **three hours of ChatGPT Pro thinking**. Work on a **zero-free region for the Riemann zeta function** and a proof of the Hodge conjecture for CM abelian varieties did not follow that fixed procedure; the zeta write-up was human-edited for readability. OpenAI's accompanying post says it consulted the IAS-hosted [Advisory Group on Mathematics and AI (AGMAI)](https://timesof.ai/2026/09/openai-mathematics-advisory-group), will fund workshops on AI-produced results, and is "working to responsibly release the model."

## What the repo actually contains

- **722 manuscripts / 372 families** — OpenAI's framing is that results "resolve or make substantial progress" on open questions; AGMAI, via The Verge, characterises the release as solutions to "**hundreds** of open questions." Attribute both.
- **162 papers with a formalized main result**, counted from `lean/formalization.yaml` (catalog header: "papers with a formalized main result"; recount before reprinting — the repo says formalizations will keep landing).
- **10 abridged reasoning summaries**, including the irrationality exponent of π, Kaplansky's direct-finiteness conjecture in characteristic two, and the Mézard–Parisi formula.
- An explicit README warning: "**some of the unformalized results could have issues.**"

This sits on top of earlier OpenAI math drops: a Lean-checked [Navier–Stokes blowup proposal](https://timesof.ai/2026/09/openai-navier-stokes-lean) and the [ten Astra-era advances](https://timesof.ai/2026/08/openai-ten-advances-mathematics-astra). Those were showcase scale. This is a catalogue.

## Claims vs checks

**Scientific American** reports that claimed results include the **four-dimensional Kakeya conjecture** and **progress toward the Riemann hypothesis**. Those specifics are Scientific American's reading of the manuscripts; we did not re-inspect those PDFs. The Riemann work in the README is a **zero-free region / progress**, not a proof of the hypothesis.

An OpenAI spokesperson told Scientific American that **almost every result came from a single prompt to a single agent**, though some may have taken several attempts, and that OpenAI's own mathematicians do not yet understand many of them. That single-agent claim is a spokesperson statement with a caveat, not a README fact.

**AGMAI** recommended disclosing the **model, exact prompt and compute behind each result**. OpenAI is publishing **average compute and some statistics**, not prompts. The spokesperson said OpenAI is **not bound** by the recommendations.

Mathematicians quoted in Scientific American split: **Andrew Sutherland** (MIT) treats one-shot claims as unverified until the model is released; **Daniel Litt** (Toronto) called the release good for mathematics.

## The trade

A single unreleased model produced several hundred claimed results at a reported average cost of about three hours of Pro-level compute each. That is a capability signal about whatever OpenAI ships next — and a stress test of how a field absorbs artefacts faster than it can referee them. About a fifth of the manuscripts (162 of 722) have a machine-checked main result. The rest carry OpenAI's own warning. "Solved hundreds of open problems" is OpenAI's and AGMAI's characterisation, not an independent verdict.

## Limits

- Model, per-result prompts and per-result compute are **withheld**.
- Formalization count **162** is a point-in-time recount of `lean/formalization.yaml`; the catalogue is designed to grow.
- Kakeya / Riemann manuscript specifics = **Scientific American's reading**, not our PDF audit.
- **372 families** are related-result groups, not a count of solved problems.

## Sources

- [OpenAI: Sharing AI progress in mathematics (October 6, 2026)](https://openai.com/index/sharing-ai-progress-in-mathematics/)
- [OpenAI (GitHub): openai/math](https://github.com/openai/math)
- [OpenAI (GitHub): lean/formalization.yaml](https://github.com/openai/math/blob/main/lean/formalization.yaml)
- [Scientific American: OpenAI unleashes hundreds more math results (October 6, 2026)](https://www.scientificamerican.com/article/openai-unleashes-hundreds-more-math-results-upon-a-field-already-in-shock/)
- [The Verge: OpenAI drops another batch of mathematical breakthroughs (October 6, 2026)](https://www.theverge.com/ai-artificial-intelligence/1005004/openai-math-release-github)
- [Times of AI: OpenAI Navier–Stokes Lean (September 8, 2026)](https://timesof.ai/2026/09/openai-navier-stokes-lean)
- [Times of AI: OpenAI Mathematics Advisory Group (September 21, 2026)](https://timesof.ai/2026/09/openai-mathematics-advisory-group)
- [Times of AI: OpenAI ten advances / Astra (August 1, 2026)](https://timesof.ai/2026/08/openai-ten-advances-mathematics-astra)