Advancing mathematics research with AI-driven formal proof search
Large language models (LLMs) increasingly excel at mathematics tasks, but their unreliability limits their utility in mathematics research. A mitigation is to use LLMs to generate formal proofs in languages such as Lean, in which the compiler verifies every proof step. We present the first demonstration of this method’s value in solving open problems at scale. We built an artificial intelligence agent for formal proof search that autonomously resolved nine of 353 open Erdős problems, proved 44/492 On-Line Encyclopedia of Integer Sequences conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. Even a basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes. These findings demonstrate the power of formal proof search as an enabler of autonomous mathematical discovery.
Authors
- Aja Huang (ORCID: https://orcid.org/0000-0002-2476-9194)
- Pushmeet Kohli (ORCID: https://orcid.org/0000-0002-7466-7997)
- Henryk Michalewski (ORCID: https://orcid.org/0000-0001-8541-8112)
- Miklós Z. Horváth (ORCID: https://orcid.org/0000-0001-6928-7423)
- Eric Wieser (ORCID: https://orcid.org/0000-0003-0412-4978)
- Swarat Chaudhuri (ORCID: https://orcid.org/0000-0002-6859-1391)
- Codruţ Grosu (ORCID: https://orcid.org/0000-0002-2479-0073)
- Ascher Wagner
- Matej Balog (ORCID: https://orcid.org/0000-0002-5552-9855)
- Gergely Bérczi
- Thomas Hubert (ORCID: https://orcid.org/0000-0003-2209-3933)
- Francisco J. R. Ruiz (ORCID: https://orcid.org/0000-0002-2200-901X)
- George Tsoukalas
- Edward Lockhart
- Sergey Shirobokov (ORCID: https://orcid.org/0000-0002-0945-6296)
- Anton Kovsharov
- Moritz Firsching
- Andrew Ferrauiolo
- Anja Surina
- Lei Yu
- Arun Suggala
Institutions
- Google (United States) (US)
- Aarhus University (DK)
- Google DeepMind (United Kingdom) (GB)
Publication Details
- Journal
- Science
- Published
- 2026-10-08
- DOI
- https://doi.org/10.1126/science.aej2213
- Citations
- 3
- Primary Topic
- Mathematics, Computing, and Information Processing
- Type
- article
- Field-Weighted Citation Impact
- 11.07