Formal proof search closes nine Erdos problems
An agent that generates proofs in Lean and verifies them there autonomously resolved 9 of 353 open Erdos problems and proved 44 of 492 conjectures from the encyclopedia of integer sequences.
Why it matters
A denominator appeared: not a count of problems closed but a share of a fixed open set, with every proof machine-checked.
The paper was submitted to arXiv on 21 May 2026 with twenty-one authors, the first being George Tsoukalas, Anton Kovsharov and Sergey Shirobokov. The system pairs a large language model generating formal proofs in Lean with Lean-based verification of every step: if a proof does not hold up, it is rejected. The stated results are that the agent autonomously resolved 9 of 353 open Erdos problems and proved 44 of 492 open conjectures from the Online Encyclopedia of Integer Sequences. A second approach, alternating model generation with Lean verification, replicated the Erdos results but proved more expensive on the hardest problems. The work spans combinatorics, optimisation, graph theory, algebraic geometry and quantum optics. Quanta Magazine attributes the work to a DeepMind team of 21 researchers.