Advancing Mathematics Research with AI-Driven Formal Proof Search
Abstract
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erd\H{o}s problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erd\H{o}s successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
Cite
@article{arxiv.2605.22763,
title = {Advancing Mathematics Research with AI-Driven Formal Proof Search},
author = {George Tsoukalas and Anton Kovsharov and Sergey Shirobokov and Anja Surina and Moritz Firsching and Gergely Bérczi and Francisco J. R. Ruiz and Arun Suggala and Adam Zsolt Wagner and Eric Wieser and Lei Yu and Aja Huang and Miklós Z. Horváth and Andrew Ferrauiolo and Henryk Michalewski and Codrut Grosu and Thomas Hubert and Matej Balog and Pushmeet Kohli and Swarat Chaudhuri},
journal= {arXiv preprint arXiv:2605.22763},
year = {2026}
}
Comments
The first three authors and the last author have equal contributions. The first three authors are in random order