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 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 ↗
Also recorded at
erdos-12
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
erdos-138
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
vibemathedBen Green's Open Problem 57
green-open-problem-57
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
vibemathedWritten on the Wall II, Graph Conjecture 2
wow-graph-conjecture-2
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
vibemathedMonochromatic Quantum Graphs in the Diagonal Family
monochromatic-quantum-graphs-diagonal
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
vibemathedFour-Particle Monochromatic Quantum Graphs
monochromatic-quantum-graphs-four-particles
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
vibemathedLog-Concavity of Codimension-Three Pure O-Sequences
pure-o-sequences-log-concavity
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
vibemathedLast-Iterate Rate for Anchored Gradient Descent-Ascent
anchored-gda-last-iterate
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
This record cites the team's April preprint, arXiv:2604.03782, which the AlphaProof Nexus report refers to for this result; the Lean proof sits in the same results repository.
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.
History of this entry
- CorrectedRecorded the eight vibemathed records that cover parts of this result as registrations. vibemathed describes the work as autonomous, which does not move the search-scaffold grade for the reasons given in the caveats.
- 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}
}