Editorial

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 is the single best artifact in the field.

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

Consider what has happened since. On 1 August OpenAI published ten advances on open problems in mathematics and theoretical computer science. On 3 August Quanta ran a feature on why the Erdős problems are falling. Somewhere in between, the field's only systematic record of what machines had actually done went quiet, and nothing replaced it.

This is not a criticism of the people who maintained it. They are mathematicians, and maintaining a ledger is not mathematics. It is an observation that the infrastructure and the attention have come apart, and that the gap is now wide enough to drive a narrative through.

Four claims wearing one coat

“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 are interesting. Only the first is the thing readers imagine. Of the 257 claims in this register that concern a statement itself — as opposed to supporting work like formalisation or literature search — 34 are full solutions with no significant human mathematical involvement recorded. That number is remarkable, and it is not the number in the headlines, because the headlines do not have a number.

132 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.

Not everything is a theorem

There is a second way the record goes wrong, and it is structural rather than careless. 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 inched upward for decades. Nothing was settled. A number 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 entirely. 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. These are not proofs. They are objects, and they are the bulk of what machines have actually 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 72 of them, with a machine leading on 22.

There is an unexpected dividend. An object does not need a proof assistant to check — it needs the constraints of its own problem. Is this set free of collinear triples, and how big is it? Does this decomposition reproduce the multiplication tensor exactly? Those questions are answered in seconds by a short program, 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. The verification nobody was doing turns out, for this whole class of result, to be the cheap one.

The check nobody is doing

571 statements in this register cite a Lean proof held in another repository. That is the strongest form of evidence available in mathematics: a proof a machine can confirm, where the confirmation does not depend 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, 80 contain unproved goals or declare their own axioms — which may be perfectly legitimate scaffolding, and is also exactly the thing a reader assumes has been ruled out when they see the word formal.

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 — 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. It is also a different thing from 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 rather than rounding up. V3 is only ever awarded on a rebuild — this register's own, or Palomar's, named against each check — and it is awarded 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. OpenAI did exactly that. 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: Formal Conjectures corrected the spelling of its Millennium directory four days later. Noticing that is part of what a register is for.

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 479 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 567 of them across 348 repositories. 348 were reviewed by their authors or not at all. 19 assume results from the literature rather than proving them. 316 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 249. 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 as the sources document them, against the statement, and adjudicates none of it.

The same month produced the case 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 114 results in the disclosure ledger, 100 are withheld.

One statement, one record

The register holds 1841 statements across 18 collections — Erdős, Kourovka, Hilbert, Millennium, Green's problems, and more. 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 makes a question answerable that previously required a study. A benchmark is a set of statements; so asking how many of its members already have public AI work against them is a query. Of the 439 statements the formal record still marks open, the register already holds AI claims against a fraction of them — and 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 617 problems solved with AI in the loop and has a community voting on them. One grades 70 results with more care per entry than any automated ingest could manage. One rebuilds Lean developments and issues them citable identifiers. That is a good thing, and it makes the original case for this register weaker: the ledger is being kept now, by several hands.

It also creates a problem none of them can solve from the inside. They use different vocabularies, they cover different things, and they disagree. Nobody was setting them side by side.

So that is what this register now does as well. It reads 1059 entries from other registries and joins them to its own on keys a source actually supplies. Of the 125 results held in more than one place, 40 carry a genuine disagreement about who did the mathematics, and in 61 cases somebody else holds stronger evidence than we do. That last number is published because it is true, not because it flatters.

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 will not do

It will not rule on whether a proof is correct. That is what referees and proof assistants are for, and a website that pretends otherwise would be worse than useless. It grades the evidence attached to a claim against a rubric published in full, and where a lab disputes a grade the dispute will be shown next to it.

It will not rank the labs. Selection bias makes any success rate computed from this data meaningless — the wiki's own third disclaimer says so, and it is right. Statements attract attention for reasons that have nothing to do with difficulty.

It will not audit the other registries either. Every one of them is doing something this one is not, and those curating by hand are more careful per entry than an automated ingest can be. A disagreement recorded here is a prompt to look, not a verdict, and where the difference turns out to be two projects cutting their scales in different places, the raw labels beside each position will show it.

What it will do is keep the ledger, in public, on a schedule, with every row traceable to its source. The field has produced a genuinely astonishing year. It deserves a record that is still being written.