The record stopped on 30 June

qed.bot

The most complete public account of what artificial intelligence has contributed to the Erdős problems is a wiki page attached to a GitHub repository. It is careful work. It distinguishes standalone machine results from collaborations, flags incorrect claims in red, and carries eleven separate disclaimers warning the reader not to treat it as a benchmark.

It now opens with a line in bold: the wiki is no longer updated. The latest data is 30 June 2026.

Since then, OpenAI has published ten advances on open problems in mathematics and theoretical computer science (1 August), and Quanta has run a feature on why the Erdős problems are falling (3 August). Over the same weeks the field's only systematic record of what machines had done stopped, and nothing replaced it.

Its maintainers are mathematicians, and keeping a ledger is not their job. But the attention the field now receives has outgrown the records kept of it.

What “AI solved an open problem” can mean

“AI solved an open problem” can mean at least four things. It can mean a system was handed the problem and returned a proof with no human in the loop. It can mean a human formalised the statement, supplied the relevant literature, and steered the search. It can mean the system found a result already implicit in a paper nobody had connected to the question. It can mean a person and a machine worked it out together over a fortnight.

All four are interesting, but readers usually picture the first. Of the 261 claims in this register that concern a statement itself, rather than supporting work such as formalisation or literature search, 34 are full solutions with no significant human mathematical involvement recorded. Headlines rarely give that number.

143 of the recorded contributions were worked jointly with a named human. They are listed here with the collaborator's name against them, because a collaboration reported as a solo machine result is the most common way this field gets misdescribed.

Results that are not theorems

A list of open problems can only record that something was settled. But in August 2026 a model asked to attempt the Riemann hypothesis failed, and on the way raised the proportion of zeta zeros provably on the critical line from 41.6 per cent to 67.2 per cent, a constant mathematicians had raised slowly for decades. Nothing was settled, but a bound moved.

That result appears on no list of problems, so a register built only from lists would miss the most discussed piece of AI mathematics of the year. The same is true of a cap set of 512 points, of a 4×4 matrix product in 47 multiplications rather than 49, and of the roughly twenty constructions AlphaEvolve improved on across its problem set. They are objects rather than proofs, and they make up much of what machines have contributed.

So this register holds a second kind of node. A target is a quantity with a direction and a history of values, each attributed to whoever reached it. It now holds 77 of them, with a machine leading on 27.

Objects are also cheaper to check. Checking one needs the constraints of its own problem rather than a proof assistant. Is this set free of collinear triples, and how big is it? Does this decomposition reproduce the multiplication tensor exactly? A short program answers those in seconds, where a Lean proof costs an hour and several gigabytes. We ran them: the 512-point cap set holds, and the 47-multiplication algorithm is an exact identity.

Rebuilding cited proofs

582 statements in this register cite a Lean proof held in another repository: a proof a machine can confirm, without relying on anybody's judgement or reputation.

We fetched every one of them. 24 could not be retrieved at the address given. Of those that could, 85 contain unproved goals or declare their own axioms. That may be legitimate scaffolding, but a reader who sees the word formal usually assumes it has been ruled out.

So we started recompiling them. 35 cited proofs have been rebuilt here: dependencies resolved at the pinned commit, the file elaborated, and #print axioms run against every theorem it declares. 19 came back clean, with 1787 theorems resting on nothing beyond propext, Classical.choice and Quot.sound.

1 of the proofs rebuilt so far turned out to rest on axioms beyond the standard three: Lean.ofReduceBool, Lean.trustCompiler. Those are the signature of native_decide, which discharges a goal by running compiled code and trusting the result. It is a legitimate and sometimes necessary technique, but it is not a proof the kernel has checked, and a reader following a link marked formal proof has no way to tell the two apart.

The rest of the cited artifacts are unchecked, and the register says so against each one. V3 is awarded only on a rebuild, by this register or by Palomar, named against each check, one proof at a time.

Checked against what?

On 8 September OpenAI announced a proof that the Navier–Stokes equations can blow up in finite time under a smooth force (a negative answer to a Millennium Prize problem), together with a Lean formalisation. A Lean proof settles that the proof is valid. It cannot settle that the statement proved is the one that was claimed, and that gap is what the field now argues about.

The best available answer is to check the proof against a statement somebody else wrote, and OpenAI did so. Its formalization.yaml declares that the reference statements for Fefferman's alternatives (C) and (D) come from DeepMind's Formal Conjectures, and its Comparator challenge checks the proof against them. That is the strongest evidence of fidelity the field has, and it is written in a form a program can read. The link in the declaration no longer resolves, because Formal Conjectures corrected the spelling of its Millennium directory four days later; the register records the move.

So the register now grades a third axis. F3 is a proof anchored to a statement written independently of it; F2 a correspondence the authors declare; F1 a formal artifact nobody has compared with its claim; F0 nothing formal at all. Of the 488 results carrying claims here, 3 are anchored.

Most of what the field says about its own formalisations is now published in these files. We read 636 of them across 400 repositories. 389 were reviewed by their authors or not at all. 23 assume results from the literature rather than proving them. 349 have been checked by nobody independent of their authors. Palomar, which rebuilds a project at a pinned commit, confirms its statement with Comparator and replays the proof through two independent kernels, has checked 285. Where Palomar has done that work, this register cites it rather than repeating it.

Navier–Stokes also shows why provenance belongs in a register. Tristan Buckmaster and Levent Alpöge announced blowup with smooth forcing for Euler twelve hours earlier. Both teams built on a programme of Diego Córdoba and Luis Martínez-Zoroa, and the first version of OpenAI's paper did not cite it. The register records precursors and competing work against the statement, as the sources document them.

In the same month came a claim no checker can reach. On 21 September OpenAI said its models had resolved more than a hundred long-standing open problems, and named none of them. A result that has not been identified cannot be graded for autonomy, evidence or fidelity. It can only be counted: of the 118 results in the disclosure ledger, 100 are withheld.

One statement, one record

The register holds 1850 statements across 19 collections: Erdős, Kourovka, Hilbert, Millennium, Green's problems and others. Each is a single record. Its formalisations, cited proofs, recompilations, prizes and every claim made about it hang off that one node, which is why the same problem cannot appear twice with two different stories attached.

It also turns some questions into counts. A benchmark is a set of statements, so how many of its members already have public AI work against them can be read off the register. Of the 432 statements the formal record still marks open, the register already holds AI claims against a fraction; that fraction is on the benchmarks page, recomputed on every build.

The field filled in

Since this register was started, several others have appeared. One tracks 755 problems solved with AI in the loop and has a community voting on them. One grades a smaller set of results with more care per entry than any automated ingest could manage. One rebuilds Lean developments and issues them citable identifiers, 377 so far. The ledger is being kept now, by several hands.

But they use different vocabularies, they cover different things, and they disagree, and nobody was setting them side by side.

So this register does that as well. It reads 1132 entries from other registries and joins them to its own on keys a source supplies. Of the 128 results held in more than one place, 40 carry a disagreement about who did the mathematics, and in 61 cases somebody else holds stronger evidence than this register does.

One kind of finding needs no judgement at all. When a registry grades a result as machine-checked, it is making a claim about an artifact, and that claim can be tested without rebuilding anything: does the repository cited contain any Lean? 1 of the 6 repositories cited to us as holding a machine-checked proof contain none at all. Whatever supports those grades, it is not in the repository given.

What this site does not do

It does not rule on whether a proof is correct; that is for referees and proof assistants. It grades the evidence attached to a claim against a rubric published in full, and where a lab disputes a grade the dispute is shown next to it.

It does not rank the labs. Selection bias makes any success rate computed from this data meaningless, as the wiki's own third disclaimer says. Statements attract attention for reasons that have little to do with difficulty.

It does not audit the other registries. Each of them does something this one does not, and those curating by hand are more careful per entry than an automated reading can be. A disagreement recorded here is a reason to look again, and where the difference turns out to be two projects dividing their scales in different places, the raw labels beside each position show it.

It keeps the ledger in public, on a schedule, with every row traceable to its source.