On 6 October 2026 OpenAI published the openai/math repository on GitHub, with 722 mathematics manuscripts produced by an unreleased internal model and grouped into 372 families of results. It is the same model that in September produced the Navier-Stokes proof.

The model was posed about 4,000 problems. On average a result took the equivalent of three hours of ChatGPT Pro reasoning. For 235 of the 372 families there is a formalisation in Lean, at least of the main result, the language that lets a computer check a proof step by step.

What it contains

Among the claimed results, these are the ones that made the most noise.

  • The Unique Games Conjecture of Subhash Khot, central to theoretical computer science. It would follow that Max-Cut cannot be approximated better than the Goemans-Williamson algorithm, nor Vertex Cover better than a factor of two, unless P equals NP.
  • The quasi-Riemann hypothesis. The zeta function and all Dirichlet L-functions have no zeros with real part greater than 7/8. The Riemann hypothesis asks for 1/2, so this is not the millennium problem, but a zero-free half-plane of this kind was precisely the open question.
  • The isomorphism of the free group factors, a question open for decades in von Neumann algebras.
  • A counterexample to Kaplansky’s zero-divisor conjecture, after Giles Gardam had found one to the unit conjecture in 2021.
  • The irrationality of Catalan’s constant and the exact irrationality exponent of π.

Other major results, such as the Birch and Swinnerton-Dyer formula for every elliptic curve over ℚ with Selmer corank 0 or 1 or the counterexamples to the Baum-Connes conjecture, have no formalisation for now. OpenAI itself writes that some unformalised results could have issues.

How it can be checked

For the formalised results the check does not depend on OpenAI. The repository includes challenges for Comparator, a Lean community tool that verifies the proved theorem matches a reference statement and that the proof uses only the three standard axioms. The check can therefore be rerun independently on a Linux machine with Lean and the tools listed in the repository.

One question remains that Lean does not settle: does the formal statement really say what the title says? For zeta the statement is one line, the function does not vanish when the real part exceeds 7/8, and it is hard to get wrong. For more structured results the fidelity of the translation has to be read by competent people, and across 722 manuscripts that work will take months.

OpenAI says it consulted the Institute for Advanced Study’s advisory group, which had published its recommendations on 29 September. On transparency it followed them in part: reasoning summaries for ten families, the average compute and the number of problems posed, but not the model’s name or the prompts.

The Comparator challenges do answer the request to formalise. The group also asks for repositories not controlled by the labs, and for now the repository belongs to OpenAI, which says it is exploring community-hosted options.

On 6 October the group clarified that its role should not be read as an endorsement of the process, and that it is up to the mathematical community to judge how far the recommendations were followed.

What I think

For mathematics understood as the production of proofs, a phase is over. Until yesterday the scarce resource was finding the proof. Today it is checking that the statement is the right one, understanding why the result is true and deciding which problems are worth posing.

It is the shift that the Fields medallists who signed the declaration of 11 September ask to govern, so that the speed of results does not come at the expense of understanding them.

For the rest of the world the answer is more cautious. The direct consequences of these theorems are real but slow. If the zeros of zeta lie below 7/8, the error in the prime number theorem drops to x to the power of 7/8 plus epsilon, a huge improvement for number theory.

The expected effect on cryptography is limited: these theorems establish properties and limits, they provide no attack algorithms, and RSA rests on the difficulty of factoring. The Unique Games Conjecture sets limits on how well certain optimisation problems can be approximated, and does not speed up existing algorithms: it says how far they can go.

What changes the world is the method. A model that is given about four thousand problems and closes a few hundred, with proofs a machine can check, is the same kind of system that the Cambridge paper on the intelligence explosion sees applied to AI research.

Mathematics is the first field where this is plainly visible, because it has a formal verifier. In other fields the verifier is the laboratory, and it is slower.

My answer to the question in the title is that the time when the difficulty of producing a result also guaranteed its scarcity is over. From here on the value shifts more and more towards those who know how to pose the questions and check the answers.

Limits

At the time of writing I have found no public confirmation of the main results by outside mathematicians. Manuscripts without a formalisation should be treated as unverified, and at least one result, the zero-free region with real part above 11/12, was edited by people for readability. OpenAI also states that the work on the zeta zero-free region and on the Hodge conjecture for CM abelian varieties did not follow the standard procedure.

The model is not available, so the process cannot be reproduced from outside. The reference statements for Comparator were written by OpenAI, and their correspondence with the original conjectures has to be checked case by case.

Cover image: the first page of Bernhard Riemann’s memoir Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse*, in the report of the Berlin Academy of Sciences for November 1859. It is the text in which the Riemann hypothesis appears — public domain — https://commons.wikimedia.org/wiki/File:RiemannPrim1859.djvu*