LLM-Driven Formal Proof Agents Crack Open Problems in Mathematics at Scale
This paper presents the first large-scale evaluation of LLM-based agents generating formal proofs in Lean to autonomously solve open mathematical problems. The most capable agent resolved 9 of 353 open Erdős problems and proved 44 of 492 OEIS conjectures, at a cost of only a few hundred dollars per problem. The system is already being deployed across active research domains including combinatorics, algebraic geometry, and quantum optics — marking a meaningful transition from AI as a math reasoning benchmark tool to AI as a genuine research collaborator. A simpler baseline agent (LLM generation alternating with Lean verification) matched Erdős results but scaled poorly to harder problems, highlighting the importance of agent architecture.