Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

Read on arXiv

Type: paper
Venue: arXiv / Google DeepMind
Year: 2026
Source: arxiv
Access: free
Language: en
Added: 2026-08-14T19:20:00Z
Verified: 2026-08-14T19:20:00Z

Summary

Google DeepMind AlphaProof Nexus: agents that edit Lean sketches (EVOLVE-BLOCK/VALUE) with Gemini 3.1 Pro, compiler feedback, optional AlphaProof tree-search, and an AlphaEvolve-style evolutionary population with Elo-rated incomplete sketches. Full-featured agent solved 9/353 formalized Erdős problems (including 1970 #12 variants and 1996 #125) at a few hundred USD per solve, proved 44/492 autoformalized OEIS conjectures, and was deployed on anchored GDA convergence, bipartite reconstruction, Zanello log-concavity, Green #57, and quantum-optics GHZ constructions. Post-hoc, a basic Ralph-loop agent also solved all 9 Erdős items, cheaper on easy ones and costlier on hard ones; Codex GPT-5.5 solved 7/9; Claude Code Opus 4.7 solved 0/9. Lean proofs released; agent code not public.

Keywords

alphaproof · lean · erdos · oeis · google-deepmind · formal-proofs · alphaevolve

Topics

formal theorem proving, Lean, mathematical discovery

Research notes

Primary: arxiv abs 2605.22763. Discord posted https://t.co/iHqa9CYqKa which resolves to the PDF (arXiv 2605.22763v2). Equal contributions Tsoukalas/Kovsharov/Shirobokov (random order); correspondence pushmeet@google.com and swarat@google.com. Proofs https://github.com/google-deepmind/alphaproof-nexus-results (Apache-2.0, Lean). Agent framework itself is not released. Proof artifacts, not a training corpus, so no datasets_local row.