Science published on October 8, 2026, the paper “Advancing mathematics research with AI-driven formal proof search,” by George Tsoukalas and colleagues at Google DeepMind, which presents AlphaProof Nexus: a language-model-based artificial intelligence framework that autonomously searches for mathematical proofs and verifies them step by step in Lean, a formal language whose compiler checks every logical inference. According to the summary released by the American Association for the Advancement of Science (AAAS) on EurekAlert, the system solved dozens of previously open problems across several branches of mathematics.
The most striking figure comes from the Erdős problems, the catalog of more than 1,200 questions posed by the Hungarian mathematician Paul Erdős and his collaborators, maintained by Thomas Bloom. The open Formal Conjectures repository contains Lean formalizations of a subset of those problems; at the time of the experiment there were 353. DeepMind’s full-featured agent attacked all of them, with a cap of 3,000 episodes per problem, and solved nine. Two of them had been open for 56 years, according to the paper’s preprint.
AlphaProof Nexus also proved 44 of 492 open conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS), resolved a fifteen-year-old open question on Hilbert functions in algebraic geometry and improved a known bound in convex optimization by discovering a new algorithmic parameter schedule. The authors note that the system also identified several misformalizations in the literature, helped resolve a problem from Ben Green’s well-known list and is contributing to ongoing research in quantum optics and graph theory.
The architecture is the core of the approach. In its basic version, several subagents search for proofs independently and receive as feedback the Lean compiler’s error messages, which tell them exactly which step fails. In the “full-featured” version, those subagents are coordinated by an evolutionary algorithm inspired by AlphaEvolve and can call on AlphaProof, the reinforcement learning system DeepMind built for Olympiad-level theorem proving, as a specialized tool for hard subproblems.
Formal verification tackles one of the central problems of AI in mathematics: language models can produce convincing arguments that contain subtle or outright invented errors. Checking long proofs by hand requires expert time, which is scarce. When a proof is written in Lean and the compiler accepts it, logical correctness is guaranteed, as long as the formal statement faithfully captures the original question. That is why, after each solve, experts on the team validated that the formalization of each Erdős problem matched the original statement.
Cost matters too. According to the preprint, the full agent solved the Erdős problems at an inference cost of a few hundred dollars per problem. That figure, modest against the value of a new mathematical result, suggests this kind of search could become a routine tool for research groups, at least for problems that can be formalized precisely. DeepMind released the Lean proofs and human-written prose versions in the public alphaproof-nexus-results repository.
The mathematical community has followed these advances with interest and caution. The Erdős results were logged on the wiki Terence Tao maintains about AI contributions to those problems. In a Perspective published alongside the paper in Science, Jeremy Avigad of Carnegie Mellon University and Matthew Ballard of the University of South Carolina point out that even unsuccessful AI attempts helped the authors understand the problems better, and stress that the essential goal is to support mathematicians in the search for knowledge and understanding.
The figure deserves context. Nine out of 353 is just over 2.5% of the problems attempted, and many of the Erdős problems solved are not among the catalog’s most famous. The paper does not claim to have solved any of the Millennium Prize problems or anything comparable. Its contribution is showing that an automated system can produce, with formal guarantees, new and verifiable results in research-level mathematics, something that until recently was limited to competitions or to formalizing already known proofs.
Publication in a peer-reviewed journal also contrasts with other channels. In recent weeks, other labs have posted large batches of AI-generated mathematical manuscripts directly to repositories, opening a debate about how to validate and credit such work. DeepMind’s paper went through Science’s editorial process and comes with the formal files, allowing anyone with Lean installed to check the proofs.
The expert contacts listed in the AAAS release include Pushmeet Kohli and Swarat Chaudhuri of Google DeepMind. The line of work builds on AlphaProof and AlphaGeometry, which reached medal-level performance at the 2024 International Mathematical Olympiad, and on AlphaEvolve, the evolutionary algorithm-search system. AlphaProof Nexus combines those pieces and makes the jump from competition problems, whose answers are known, to questions nobody had answered.
The implications go beyond pure mathematics. Pairing generative models with a strict verifier is a pattern that applies to other fields where results can be checked automatically, such as software verification, chip design or certain industrial optimization problems. The improved bound in convex optimization, obtained by discovering a new parameter schedule, shows how a theoretical result can have practical consequences for algorithms used every day.
Clear limits remain. The method depends on the problem being expressible formally, and much of today’s mathematics is still not formalized in Lean. It also depends on the fidelity of the formalization: a badly posed formal statement can yield a correct proof of something other than what was intended, a risk the system itself helped expose by flagging misformalizations. And choosing which questions deserve attention remains, for now, a human task.
Even so, the publication of AlphaProof Nexus in Science consolidates a trend: AI is starting to act as a verifiable collaborator in mathematical research, not just an assistant that suggests ideas. If costs keep falling and the library of formalized mathematics grows, tools like this could change how open conjectures are explored, always with formal verification as the guarantee and with mathematicians deciding which results matter.
