OpenAI Posts 722 Math Papers From an Unreleased Model

OpenAI has put a mathematics department’s worth of output on GitHub in one go. On Tuesday evening it published openai/math, a repository of 722 manuscripts grouped into 372 “families” of related results, all produced by an internal model the company has not released. According to the repository’s README, the model was posed roughly 4,000 research problems during evaluation, and each result took on average about three hours of ChatGPT Pro thinking compute. OpenAI says it widened these open-problem evaluations because the model had saturated its existing maths benchmarks.

The scale is new, but so is the ambition of the claims. Earlier this year the headlines were about single problems: OpenAI’s Erdős unit-distance disproof in May and the ten decade-old problems it attributed to Astra in August. Last week Meta said Muse Spark helped crack five open problems. The new catalogue instead lists famous conjectures by name and says they are resolved.

What the catalogue claims

Among the entries in OpenAI’s overview:

• The quasi-Riemann hypothesis. Every Dirichlet L-function, the Riemann zeta function included, has no zeros with real part above 7/8. That is far short of the Riemann hypothesis, which puts the line at 1/2, but no fixed zero-free half-plane of this kind has ever been proved.
• The Unique Games Conjecture. A proof of Subhash Khot’s conjecture, which would settle the best possible approximation ratios for problems such as Max-Cut and Vertex Cover.
• Hilbert’s tenth problem over the rationals. A negative answer: no algorithm can decide whether an integer polynomial has a rational zero.
• The irrationality exponent of π is exactly 2, which would also prove that the Flint Hills series converges.
• The rational Hodge conjecture for CM abelian varieties, in every dimension, with the Tate conjecture for abelian varieties over finite fields as a consequence.
• Operator algebras: all nonabelian free group factors are isomorphic, and Kadison’s similarity conjecture holds.
• Counterexamples to Kaplansky’s zero-divisor conjecture, the reduced Baum–Connes conjecture and the hyperinvariant-subspace problem.

Other families claim the symmetric and general Mahler conjectures, the Hilbert–Smith conjecture in every dimension, Lech’s multiplicity conjecture and the complete Crouzeix conjecture. The overview sorts the 372 families into 17 fields, from number theory and combinatorics to mathematical physics and logic.

How much has been checked

OpenAI is explicit that the collection sits “at different stages of verification”. The repository’s formalization catalogue lists 162 papers whose main result has a proof in Lean, a language in which a computer checks every logical step. Among them are the quasi-Riemann paper, the Unique Games paper, the symmetric Mahler conjecture, the Kaplansky counterexamples and the Crouzeix result. Several of the most striking claims, including Hilbert’s tenth problem over the rationals, the result on π, the Hodge results and the free group factors, have no formal proof yet. The README warns that “some of the unformalized results could have issues” and promises to fix errors quickly, keeping earlier versions online.

A Lean proof also has a limit. It guarantees the formal statement follows from the axioms, not that the formal statement says what the paper claims in words. That is why OpenAI ships separate checking instructions for each formalization, and why mathematicians will still read the papers. The README also notes two exceptions to the fixed procedure: the work on zero-free regions for the zeta function and the CM Hodge proof did not come from the standard pipeline, and one writeup, for a Re(s) > 11/12 zero-free region, was edited by humans for readability. OpenAI has also released abridged summaries of the model’s reasoning for ten of the results.

The release itself

OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, an independent panel of nine mathematicians, Timothy Gowers and Edward Witten among them, set up last month to advise on how AI-produced results should be released. The group has said it holds no decision-making power over any company. OpenAI adds that it is exploring community-hosted repositories for the material, will fund workshops and programmes to help mathematicians digest the results, and is working to release the model that produced them. It has not named that model.

Early reactions, collected by Latent Space, ran from awe to caution. Anthropic researcher Levent Alpöge called it “obviously the most significant moment in mathematical history”, while also noting the awkward position of mathematicians who may find they have been scooped. Will Depue said he expected some results not to survive scrutiny, and François Chollet asked whether gains in checkable fields like maths will carry over to areas where there is no verifier. None of the headline claims has yet been confirmed by mathematicians outside OpenAI, and for the unformalized papers that process is measured in months of refereeing, not hours of compute.