Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs
Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs is graded formally verified on whataifound.org, with the AI's role graded search scaffold.
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.
- Verification
- Formally verified
- Autonomy
- Search scaffold
- Lab
- Google DeepMind
- Model
- AlphaProof Nexus (LLM + Lean)
- Field
- Mathematics
- Date
- 2026-05-21
- Human collaborators
- Pushmeet Kohli, Swarat Chaudhuri
- Notability
- 20 Wikipedia language editions
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
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 ↗
Sources
How this is graded
whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is formally verified and search scaffold. Full definitions are in the methodology.
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-nexus