A recent paper on formal proof search reports nine resolved Erdős problems out of 353 attempted in Lean. The same system proved 44 of 492 conjectures from the Online Encyclopedia of Integer Sequences.

Nine out of 353 is 2.5 percent. It looks like a score, which is exactly the trouble.

The 353 questions do not form a calibrated test. They differ in age, difficulty, importance, mathematical area, and how much serious attention they have received. Thomas Bloom, who maintains the Erdős Problems site, has been warning about this for months. His AI links page collects work in this area. In a January 30 forum comment, Bloom writes that comparing systems by a hard count of solved problems is “at best, misleading.”

That warning is not an argument that the recent systems have done nothing interesting. It is a request to keep the information that the count discards.

“Open” is a status, not a difficulty score

A January study using Gemini ran a semi-autonomous workflow across 700 conjectures then marked Open in the Erdős Problems database. The system produced roughly 200 candidate solutions. Human grading found 63 technically correct responses.

Expert review cut that number again. Thirteen answers were judged to address the intended mathematical problems. Five appeared to be new autonomous solutions. Eight located earlier solutions in the literature. Other responses had found technically valid special cases or exploited wording that did not capture what the problem was really asking.

That sequence, 700 to about 200 to 63 to 13, is more informative than any one of the numbers by itself. The paper also notes that some entries had remained marked Open because they were obscure, not because generations of mathematicians had failed to solve them.

So even the label on the database needs interpretation. A literature rediscovery can be useful evidence about search and mathematical retrieval. It should not be counted as a new theorem. A correct answer to an unintended special case is something else again.

Lean gives a strong check on correctness

The formal-proof-search paper addresses one of the genuine weaknesses of LLM mathematics: a natural-language proof can look competent while concealing a bad step. Lean checks the derivation against a formal statement. For the nine reported Erdős resolutions, that gives substantially stronger evidence of correctness than a plausible-looking write-up would.

The paper reports inference costs on the order of a few hundred dollars per problem. It also makes clear what its denominator contains: the 353 Erdős statements that were available in an open Lean formalization repository in early February. That is a useful test set, but it is not a random sample of research mathematics. Problems that have already been formalized are selected in ways that matter.

Formal verification therefore settles a specific and important question about the proof. It does not measure the importance of the problem, establish novelty, or tell us whether the formal statement captured every bit of the intended informal question. Those need separate evidence.

The harder examples change the picture

Raw counts are especially bad at representing outliers, and research progress often lives in the outliers.

In May, an internal OpenAI model produced a counterexample to a planar unit-distance conjecture associated with Erdős and dating to 1946. External mathematicians checked the argument, and the Erdős Problems history for Problem 90 now records the disproof.

This was not one of the forgotten easy entries that make Bloom nervous about leaderboard arithmetic. The result drew serious attention from mathematicians, and the proof used ideas from algebraic number theory in a geometric setting. Whatever one concludes about the general rate of AI progress in mathematics, this is evidence of a different quality from finding an old paper that happened to settle an obscure database entry.

A database total gives each event one unit.

A better report needs more columns

For research mathematics, the useful questions are not difficult to name. They are just inconvenient for a leaderboard.

  • Which problems were attempted, and how were they selected?
  • How long had the problems been open, and how much expert attention had they received?
  • Was the result new, a rediscovery, a special case, or a correction to the problem statement?
  • How many independent attempts were run, with what compute and tool access?
  • Did the system have access to the web or mathematical literature?
  • Was the final argument formally verified, human-checked, or both?
  • How much human repair or interpretation was needed before the result became usable mathematics?

Those columns will not collapse neatly into one percentage. That is fine. The recent work already gives us something better than a headline score: formally checked proofs, documented rediscoveries, clear failures, and at least a few results on problems that mathematicians themselves regard as substantial.

That is enough to say that AI systems have crossed a meaningful threshold in research mathematics. Measuring the threshold well will require keeping the distinctions that made it visible.

Sources