Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs
An agent pairing language models with the Lean proof assistant resolved 9 of 353 open Erdős problems and 44 of 492 open OEIS conjectures, with every proof mechanically verified.
- Model
- AlphaProof Nexus (LLM + Lean)
- Field
- Mathematics
- Date
- 2026-05-21
- Human collaborators
- Pushmeet Kohli, Swarat Chaudhuri
What was found
The system proposes proofs with a language model and checks every step in Lean, so a hallucinated argument cannot pass. Beyond the Erdős and OEIS totals it settled a 15-year-old question on log-concavity of pure O-sequences in codimension 3 and type 2, and proved an exact O(1/t) convergence rate for anchored gradient descent-ascent via a parameter choice not previously identified. Two of the Erdős problems had been open for 56 years. All formal proofs were released in a public repository.
Novelty check
The Erdős problems were listed as open in the erdosproblems.com database and the OEIS conjectures as unproven at the time of the run; the paper documents which. In the course of the work the authors found misformalizations in the stated problems #125 and #741(i), which had to be corrected before resolution, a reminder that 'open' status in a database is itself fallible. Terence Tao's community wiki independently tracks AI contributions to Erdős problems and records these.
Caveats and known objections
The headline is a hit rate, not a sweep: 9 of 353 and 44 of 492. The authors state successes concentrate in combinatorics, convex optimization and number theory where Lean's library is mature, that the agent inherits its LLM's biases and shows high search variance, and that it cannot solve problems requiring substantial new theory. Formal verification guarantees the proofs are correct; it says nothing about whether the problems were deep. Autonomy is graded search-scaffold rather than autonomous: humans built the agent, chose the problem sets, and supplied the formalization targets.
Independent checks
Lean compiler via the paper's SafeVerify step: all proofs compile with no sorry and no disallowed axioms (sorryAx) · link ↗
Terence Tao's AI-contributions wiki: tracked among AI contributions to Erdős problems · link ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Search scaffold.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and search scaffold for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-05-21-alphaproof-nexusBibTeX
@misc{whataifound-googledeepmind-2026-nexus,
title = {Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Google DeepMind. Verification: Formally verified. Autonomy: Search scaffold.},
url = {https://whataifound.org/finding/2026-05-21-alphaproof-nexus}
}