OpenAI published 722 mathematics manuscripts written by an unreleased internal model on October 6, 2026, grouped into 372 results across 17 fields, with Lean proofs for the main result of 162 papers. The claims include a zero-free half-plane for every Dirichlet L-function, the Mahler conjectures, a counterexample to Kaplansky’s zero-divisor conjecture and the isomorphism of the free group factors. OpenAI’s announcement opens: “We’re releasing a broad range of new mathematical results produced by an internal frontier model.” The papers sit in a public GitHub repository under Apache 2.0. This page reads the announcement, the repository’s README, its 41-page overview catalogue and its Lean formalization list, as of the evening of October 6, 2026.
On this page · 6 sectionsOpen
OpenAI published 722 mathematics manuscripts from an unreleased internal model on October 6, 2026, grouped into 372 result families across 17 fields, in a public GitHub repository under Apache 2.0.
The model was posed about 4,000 problems after OpenAI’s existing math evaluations saturated; OpenAI kept the results it judged significant and grouped related papers into families.
Lean formalizations cover the main result of 162 papers, including the zero-free half-plane Re(s) > 7/8 for Dirichlet L-functions, the symmetric Mahler conjecture and a Kaplansky zero-divisor counterexample.
Each result used about three hours of ChatGPT Pro thinking on average, OpenAI says, and the repository adds 10 abridged summaries of the model’s reasoning.
Claims without a Lean proof yet include the isomorphism of the free group factors, the irrationality exponent of pi being 2 and Hilbert’s tenth problem over the rationals; the README warns unformalized results could have issues.
The model is not public and the papers sit on OpenAI’s own GitHub, two points the Advisory Group on Mathematics and AI asked labs to change; OpenAI says it is working on both.
§ 01What OpenAI released
The repository holds manuscripts, a catalogue and proof files rather than one paper. Its README says how the model got there: “We expanded these evaluations after performance on our existing mathematical evaluations saturated.” Over the evaluation the model was posed about 4,000 problems; OpenAI kept the results it judged significant and grouped related papers into families.
| Item | Count or detail |
|---|---|
| Released | October 6, 2026, OpenAI announcement and GitHub repository |
| Model | Unreleased internal OpenAI model |
| Manuscripts | 722 |
| Result families | 372, across 17 fields |
| Problems posed | About 4,000 |
| Compute per result | About three hours of ChatGPT Pro thinking, on average |
| Papers with a Lean-formalized main result | 162, per the repository’s formalization catalogue |
| Reasoning summaries | 10 abridged summaries of the model’s reasoning |
| License | Apache 2.0 |
On cost, the announcement says: “The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking.” The README names two exceptions to the fixed procedure, work on a zero-free region for the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties, and says the write-up for the Re(s) > 11/12 zero-free region “was human edited for readability”.
§ 02Where the results fall
We counted the families under each field heading in the overview catalogue. Theoretical computer science, combinatorics and algebraic and complex geometry lead; mathematical logic has the fewest.
| Field | Result families |
|---|---|
| Theoretical computer science | 40 |
| Combinatorics | 37 |
| Algebraic and complex geometry | 36 |
| Number theory | 31 |
| Probability and statistical mechanics | 29 |
| Differential geometry | 29 |
| Mathematical physics | 25 |
| Operator algebras | 19 |
| Algebra | 18 |
| Topology | 18 |
| Real and complex analysis | 16 |
| Partial differential equations | 16 |
| Convex and metric geometry | 15 |
| Group theory | 14 |
| Dynamical systems and ergodic theory | 12 |
| Functional analysis | 11 |
| Mathematical logic | 6 |
§ 03The headline claims, and what is checked
The catalogue states each result as proved. A Lean formalization means a computer has checked the formal statement against the formal proof; it does not by itself show that the formal statement says exactly what the paper says, or that the result is new. The README is direct about the rest: “Some of the unformalized results could have issues.”
| Family | Claim as stated in the catalogue | Lean main result in the catalogue |
|---|---|---|
| 003 | Every Dirichlet L-function, including the Riemann zeta function, is zero-free in Re(s) > 7/8 | Yes |
| 087 | The symmetric and nonsymmetric Mahler conjectures, in every dimension | Yes, for the symmetric case |
| 196 | A counterexample to Kaplansky’s zero-divisor conjecture | Yes |
| 197 | Kaplansky’s direct-finiteness conjecture fails, even without torsion | Yes, characteristic two and odd characteristic |
| 287 | All nonabelian free group factors are isomorphic | Not yet |
| 017 | The irrationality exponent of pi is exactly 2 | Not yet |
| 004 | Hilbert’s tenth problem over the rationals has a negative answer | Not yet |
The remaining 560 papers without a formalized main result sit in the same repository; OpenAI says it “will continue to update this repository with Lean formalizations as we obtain them”. Readers checking a single claim should open its family in the manuscript map, where each paper links to its PDF and citation file.
§ 04How the release answers the advisory group
Two weeks earlier, the independent Advisory Group on Mathematics and Artificial Intelligence, hosted at the Institute for Advanced Study, published its guidelines for releasing AI-generated mathematics (September 29). They open with a request to labs: “we ask them to stop testing advanced mathematical problems on proprietary models”. OpenAI says it consulted the group and drew on those recommendations. The release follows several of them: problem counts, compute estimates, reasoning summaries and Lean files are published. Two points are still open by OpenAI’s own account. The model is not public; OpenAI says it is “working to responsibly release the model that produced these results”. And the papers sit on OpenAI’s own GitHub; OpenAI writes that it is “continuing to explore other community-hosted alternatives for this release which meet the committee’s guidelines.”
OpenAI also commits money to the reading: “We will be funding a series of workshops, conferences, and special programs around the understanding of major results produced by AI”. This is its second public batch: an earlier repository, openai/ten-proofs, held ten results, and our record of its Navier-Stokes claim covers the September episode.
§ 05What we are watching
- Independent checks. The first mathematician write-ups on individual families, starting with the zero-free half-plane and the free group factors.
- More Lean files. How fast the 162 formalized papers grow toward 722.
- A community-hosted copy. Whether the papers move to a repository OpenAI does not control, as it says it is exploring.
- The model itself. OpenAI’s release plan for the model that produced the results.
§ 06Sources
- OpenAI, “Sharing AI progress in mathematics”, October 6, 2026: openai.com
- OpenAI mathematics repository (README, overview catalogue, manuscript map, Lean catalogue): github.com/openai/math
- Lean formalization catalogue: lean/formalization.yaml
- Advisory Group on Mathematics and Artificial Intelligence, “Responsible Release of AI-Generated Mathematics”, September 29, 2026: agmai.org
- OpenAI ten-proofs repository: github.com/openai/ten-proofs
Q1What did OpenAI release on October 6, 2026?
OpenAI published 722 mathematics manuscripts produced by an unreleased internal model, grouped into 372 result families across 17 fields. They sit in the public GitHub repository openai/math under the Apache 2.0 license, with an overview catalogue, Lean formalizations and 10 reasoning summaries.
Q2Are OpenAI's math results verified?
Partly. Lean formalizations cover the main result of 162 papers, which means a computer checked the formal proof of the formal statement. The other 560 papers have no formalized main result yet, and the README warns that some unformalized results could have issues.
Q3Did OpenAI prove the Riemann hypothesis?
No. The catalogue claims a zero-free half-plane Re(s) > 7/8 for every Dirichlet L-function, including the Riemann zeta function, which it calls the quasi-Riemann hypothesis. The Riemann hypothesis itself concerns Re(s) > 1/2. The 7/8 result has a Lean formalization in the catalogue.
Q4Which model produced the results?
An unreleased internal OpenAI model. OpenAI says the average result used about three hours of ChatGPT Pro thinking and that it is working to responsibly release the model.
Q5What is the Advisory Group on Mathematics and AI?
An independent group hosted at the Institute for Advanced Study that published guidelines for releasing AI-generated mathematics on September 29, 2026. OpenAI says it consulted the group; the guidelines ask labs to stop testing advanced problems on proprietary models.