On the night of 6 to 7 October, in the early hours in Spain, OpenAI uploaded 722 mathematics manuscripts to GitHub. They were written by an internal model that the company has neither released nor named, and they are grouped into 372 “families”: each one brings together a main result with its variants and consequences. OpenAI explains that it evaluates its models on unsolved research problems and that it has published the results that reached a sufficient level of significance.
On 21 September, the company had said its model had solved “more than a hundred” open problems, without showing any of them. Now it has shown them, and there are more. Among them are claims that, if confirmed, would settle questions that have been open for decades: about how prime numbers are distributed, about the limits of optimisation algorithms, or about why a magnet stays a magnet.
Lance Fortnow, a veteran of theoretical computer science, wrote the following day that his field had advanced more in 24 hours than in the previous three decades combined. In the same post he added that none of it has been verified yet.
That caveat is the question of this article: what it means for these results to be “checked”. This time part of them can be reviewed by a machine, something that was not the case with any previous announcement. But that review has layers, and most of the work is still to be done.
What exactly is in the repository
According to the repository’s README, the model was given some 4,000 problems, and each result used, on average, the compute equivalent of three hours of ChatGPT Pro reasoning. The company does not explain how it chose those problems, but it does reveal a proportion: some 4,000 attempts produced 372 families. As Fortnow points out, the model solved less than 10% of what it was given.
Almost everything was obtained with the same automated procedure. The README acknowledges two exceptions without giving details: a region of the Riemann zeta function in which there are no zeros, and the Hodge conjecture for a certain family of geometric objects. These are precisely the two results closest to Millennium Prize Problems. One of the texts on the zeta function was also edited by people to make it readable.
The repository includes:
- the papers in PDF with their sources;
- ten abridged summaries of the reasoning the model followed;
- a library of formal proofs in Lean, which we will come to shortly;
- and a commitment to preserve the history: corrections will be published as new versions, without deleting the previous ones.
The README itself warns: “Some of the unformalized results could have issues”.
The announcement post does not highlight any specific result. The list of “major results” circulating these days is a selection made by the press and by mathematicians themselves. We have chosen four that help convey the scale of what is being claimed.
Four results to understand what is at stake
Prime numbers and the zeta function
Prime numbers seem to be scattered without order, but they follow an average law that was proved in 1896: up to a number x there are approximately x/ln x primes. The interesting question is how far the actual count strays from that law. And the answer depends on where the zeros of the Riemann zeta function lie, the points at which that function equals zero.
The Riemann hypothesis, formulated in 1859 and one of the seven Millennium Prize Problems, states that all those zeros lie on a specific line, the one with real part 1/2. If it is true, the error in counting primes is the smallest possible. Until now, all that was known was that there are no zeros right at the edge, at real part 1, and in a strip that narrows as you go up. Nobody had managed to prove that there is a strip of fixed width free of zeros. That weakened version is what is known as the quasi-Riemann hypothesis.
OpenAI claims to have proved it: there are no zeros with real part greater than 7/8. It is not the Riemann hypothesis, which requires reaching 1/2, but it would be the first advance of its kind since the question was posed. Another manuscript in the same family also rules out the so-called Siegel zeros, a hypothetical anomaly that forces many theorems about primes to depend on constants nobody knows how to compute. A second manuscript proves a somewhat smaller region, from 11/12, by a different route. That is the text people edited.
The limits of optimisation algorithms
Many practical problems are too hard to solve exactly at large scale. One example is splitting a network into two groups so that as many connections as possible are cut (Max-Cut). Another is choosing the smallest number of nodes that touch every connection (Vertex Cover). For these cases we use algorithms that give an approximate answer with a guaranteed quality. The one for Max-Cut, for example, guarantees at least 87.8% of the optimum.
Since 2002, Subhash Khot’s Unique Games Conjecture has predicted that it is impossible to do better in a reasonable amount of time. If it is true, many of the approximation algorithms we already use would be the best possible, unless P = NP. OpenAI claims to have proved the conjecture. In addition, in a separate result, it claims to prove, without relying on it, that improving those guarantees for Max-Cut and Vertex Cover is NP-hard, that is, as hard as the hardest problems in its class.
There is a human story here. According to Quanta Magazine, on 11 September rumours began to circulate that OpenAI had the proof. Dor Minzer (MIT) and two students had spent seven years on a variant of the problem and had solved it in April. Three days after the rumours, they published 95 pages with a warning on the first: the text was mathematically complete, but it was not in the form in which they wanted to share it. “There is a lot of value in failing and knowing why you failed,” Minzer told the magazine.
Why a magnet stays a magnet
In a magnet, the tiny magnetic moments of the atoms, the spins, line up. Quantum physics describes this behaviour with the Heisenberg model, and any physicist takes it for granted that in three dimensions, at low temperature, the material keeps its magnetisation. Proving it rigorously was another matter. The classical version of the model and the antiferromagnetic quantum case, in which neighbouring spins point in opposite directions, were settled decades ago. But the technique that worked in those cases does not work for the ordinary quantum magnet, and in 1999 Elliott Lieb included it as “Problem A” in a list of open problems in mathematical physics.
OpenAI claims to have proved it for every dimension from three upwards. It is a good example of a kind of result that tends to go unnoticed: it does not change what we believe about the world, but it turns a physical certainty into a theorem.
A classic question with an unexpected answer
Starting from a “free group”, the set of all words that can be written with two letters and their inverses, or with three, one builds an object from analysis called a von Neumann factor. These objects appear in the foundational work of Murray and von Neumann, and the question, attributed to Richard Kadison, is whether the object remembers how many letters it started with. It is considered the best-known open problem in its area, and much of the research was aimed at proving that the objects were different.
OpenAI claims the opposite: with two letters or with three, you get the same object. If confirmed, it would be one of those results that force a whole field to revise its intuition. It also illustrates well the problem discussed in the next section.
The rest of the catalogue
These four are a sample. The table lists other top-tier results and whether they have a formal proof in Lean:
| Result | What is claimed | Formalised in Lean? |
|---|---|---|
| Hodge conjecture for CM abelian varieties | A broad case of another Millennium Prize Problem, posed in 1950 | No. It is also one of the two exceptions to the procedure |
| Kakeya in four dimensions | A set that contains a segment in every direction cannot be “thinner” than the space itself. The three-dimensional case was solved in 2025 | No |
| Erdős conjecture on progressions | If the sum of the reciprocals of a set of integers is infinite, the set contains arbitrarily long arithmetic progressions | Only the qualitative part |
| The irrationality exponent of π | π cannot be approximated by fractions better than a typical number can. The best previous bounds were around 7.1; the new one is 2, the lowest possible | Yes |
| Hilbert’s tenth problem over the rationals | There is no algorithm that decides whether a polynomial equation has fractional solutions | No |
| Mahler conjectures | Which convex body, together with its dual, takes up the smallest possible volume, in any dimension | Yes |
Source: repository catalogue and formalisation catalogue, accessed on 7 October 2026. Descriptions simplified by Codin.
”Checked” can mean three different things
What sets this release apart from the previous ones is Lean. Lean is a language in which a proof is written in so much detail that a program can review it step by step, without trusting anyone. It relies on Mathlib, a community library of definitions and theorems that have already been checked. A proof that “compiles” in Lean means that every step follows from the previous ones.
But when a result is said to be checked, it is worth separating three questions.
First: is the formal proof correct?
This is what Lean settles, and it can be repeated outside OpenAI. The repository includes challenges for Comparator, a tool that accepts a proof only if it proves exactly the reference statement and uses only the standard axioms. Within hours of the release, several people outside OpenAI recompiled the proof of the 7/8 region on their own machines, and it checked out.
The repository contains more than 120,000 Lean files, but that library covers a small part of the catalogue: 162 of the 722 manuscripts have their main result formalised.
Second: does the formal statement say what we think it says?
Lean guarantees that the proof proves the statement it has been given. It does not guarantee that the statement means what the paper says. This is the layer that depends most on people, and its difficulty varies a great deal from one result to another.
In the best case, the statement is so short that anyone with some training can read it:
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
{s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
sorryIt reads: for any complex number s whose real part is greater than 7/8, the zeta function is not zero. riemannZeta is the Mathlib definition, written and reviewed by the community before this announcement. The sorry marks the gap that OpenAI's proof must fill, and that proof lives elsewhere in its library.
Source: QuasiRiemannHypothesis.lean, in OpenAI's repository.
If the definition is the community’s and the statement fits in two lines, the confidence Lean provides is very high. That is why the 7/8 zero-free region is, today, the best-checked result in the catalogue.
The case of the free group factors is different. Mathlib does not yet have those objects, so the Comparator challenge defines them from scratch, with definitions also written by OpenAI. Something similar happens with Unique Games: the statement relies on thousands of characters of in-house encodings. A perfect proof of a slightly wrong definition proves something else. Someone who knows the area has to read those definitions and confirm that they capture the real problem.
The formalisation catalogue makes this clear in two fields: the Lean proofs were also written by an AI agent (automation: agent), and their review is listed as pending (review: unchecked).
Third: what have we understood?
Even when the statement is properly formalised, Lean usually covers only the main theorem. For the quasi-Riemann hypothesis, the documentation itself warns that the paper’s applications are not included. Those applications are precisely what interests a specialist in prime numbers.
The other 560 manuscripts currently depend on their natural-language text and on OpenAI’s internal judgement. Among them is the Hodge conjecture, one of the two results that did not follow the automated procedure and that has no formalisation.
And then there is what no program reviews: which idea makes each proof work, whether it opens new paths and what it changes in the area. We already discussed this shift in when proving stops being the bottleneck. This release makes it tangible: the machine has made the first layer much easier, and human work is concentrated on the other two.
What mathematicians asked for and what has arrived
On 21 September, OpenAI introduced an independent advisory group of nine mathematicians, AGMAI, based at the Institute for Advanced Study in Princeton. On 29 September, a week before the release, the group published its recommendations, based on more than 600 responses from the community. They opened with a request: that labs stop testing advanced mathematical problems with proprietary models. This is how what they asked for compares with what has arrived:
| What AGMAI asked for | What OpenAI has published |
|---|---|
| Formalise in Lean with Comparator challenges | Yes, for 162 of the 722 manuscripts |
| Summarise the reasoning behind each result | Ten summaries, not one per result |
| Report failed attempts and how the problems were chosen | Some 4,000 problems attempted, with no breakdown or selection criteria |
| Fund the work of understanding the results | A commitment to fund workshops and conferences, with no figures |
| Publish in a repository not controlled by a lab | No: on OpenAI’s GitHub account, which it says is exploring alternatives |
| Model name, prompts, time and cost of each result | No: only the average cost |
| Broad access to the models | No: the model is internal. OpenAI says it is working to release it, with no date |
Sources: AGMAI recommendations of 29 September, OpenAI announcement and repository README. Comparison prepared by Codin.
Without the model or the prompts, nobody can reproduce how each result was reached. That does not prevent anyone from checking a proof, which stands or falls on its own. But it does prevent us from knowing how much the choice of problems weighed, what was tried without success, or whether the two exceptions received help that the rest did not.
That same 6 October, AGMAI published a statement that is worth reading in full. It says its advisory role should not be interpreted as an assessment of the impact of these results or as an endorsement of the process. It adds that it is up to the community to judge to what extent its recommendations have been followed. And it sums it up like this: “This release is the beginning, not the completion, of the process”.
How the community has received it in the first hours
As of 7 October, no specialist had published a review of any specific result, and no error had been confirmed. What there is are positions on how to read the announcement.
Andrew Sutherland (MIT) argued in Scientific American that anything that cannot be reproduced should be treated as unverified: “We should ask for receipts”. Daniel Litt (University of Toronto) replied in the same article with the opposite argument. If we want to know the answers, it makes no sense to ask the company to keep them secret, and he believes it will be good for mathematics. Mark Braverman (Princeton) told Quanta that mathematics by press release is not very healthy, although he acknowledged that a proof like this can open new lines of research.
Meanwhile, verification has begun to be organised outside OpenAI. In addition to the Lean recompilations, a community catalogue of open problems has imported hundreds of results with the same warning on each one: no independent mathematician has reviewed it yet. It already marks several as disputed, because of possible conflicts with previously published results.
The underlying tone has two sides. There is amazement at the scale, even among the critics. And there is weariness: after the controversy over the authorship of Navier–Stokes and the Fields medallists’ letter, criticism is no longer aimed only at what these systems say. It is also aimed at who decides the pace and how results are published.
A green test only proves what the test asks
On 29 September we argued that whoever announces a hundred advances should accompany each one with enough information to check it and build on it. This release provides considerably more than the previous one. There are complete manuscripts, a formal library that anyone can run and a version history. It would be unfair not to acknowledge that. But what would allow the process to be reproduced is still missing, and it is still unclear who pays for the work of reviewing it.
In software we know well the distinction this case makes visible. Passing tests do not prove that a program does the right thing: they prove that it does what the tests check. If the specification is badly written, the code can meet it perfectly and still be useless. Lean has turned the correctness of a proof into something like an automated test, fast and reliable. The question has shifted to the specification: whether the formal statement is the problem we care about, and what the proof teaches us beyond the fact that it is true.
That is why the figure worth following over the coming months is not 722. There are three others that will tell us more:
- How many formal statements are reviewed by someone from the area, starting with those that rely on in-house definitions.
- How many top-tier results receive a specialist review, especially those without Lean, such as Hodge.
- How many corrections the version history records. A repository of this scale with no errata would be more suspicious than one with them.
If those figures grow, this release will have helped the community incorporate real results. If they do not, we will have hundreds of theorems about which all we know is that a machine says they are true.
Sources
- OpenAI: “Sharing AI progress in mathematics”, 6 October 2026.
- openai/math repository: README, manuscript catalogue, formalisation catalogue, scope of the quasi-Riemann hypothesis formalisation and Comparator challenge. Commit
adc7f124, accessed on 7 October 2026. - AGMAI: recommendations of 29 September 2026 and statement of 6 October.
- Lance Fortnow: “Open No More”, 7 October 2026.
- Quanta Magazine: the race for the Unique Games Conjecture, 7 October 2026.
- Scientific American: reactions from Sutherland and Litt, 6 October 2026.
- Elliott Lieb: “Problem A”, list of open problems in mathematical physics, 1999.
- Independent recompilations of the 7/8 region: Zhang-Liao/quasi-riemann and davegoldblatt/openai-zeta-proof-check. They check the formal proof, not the paper.
- vibemathed community catalogue: import of OpenAI’s results.
Editorial note: we have not audited any of the results. The mathematical descriptions are simplified for a non-specialist reader and reflect what OpenAI claims, not a consensus in the community.
