DeepMind publishes AlphaProof Nexus in Science after solving 9 open Erdős problems

What did DeepMind publish in Science?

Science published “Advancing mathematics research with AI-driven formal proof search” on 8 October 2026 (DOI 10.1126/science.aej2213). The paper, by 21 authors led by George Tsoukalas of Google DeepMind, describes AlphaProof Nexus, a framework for agents that search for mathematical proofs with large language models and the Lean proof assistant.

The work is not new to people who follow AI and mathematics. A preprint appeared on arXiv in May 2026 and was revised in June, and DeepMind had already shared some solutions: the community site erdosproblems.com credits DeepMind with a construction that settled part of Erdős problem #12, which other mathematicians have since simplified and improved. What is new is peer review in a general-science journal, along with a Perspective by Jeremy Avigad of Carnegie Mellon University and Matthew Ballard of the University of South Carolina.

In the AAAS release, Avigad and Ballard highlight the authors’ report “that even unsuccessful proof attempts by AI could help them understand the problems better and make progress on solving them.” That is a more modest claim than “AI solves mathematics”, and it matches the paper.

How does AlphaProof Nexus work?

The input is a Lean file: a theorem statement with the placeholder “sorry” where the proof should be, plus the definitions it depends on. Markers in the file fence off what the agent may change, so it cannot quietly rewrite the theorem. The output counts only if Lean compiles it with no remaining “sorry”, which means the proof is checked mechanically rather than by a reviewer reading prose.

The basic agent is a set of independent prover subagents, each running what the paper calls a “Ralph loop”: Gemini 3.1 Pro reasons, edits the proof sketch with a search-and-replace tool, and Lean compiles it after every turn. Compiler errors become feedback for the next turn, and a validator checks at the end that the problem statement was not changed unsafely.

The full-featured agent adds two things. Rater subagents running the cheaper Gemini 3.0 Flash compare unfinished sketches for plausibility, clarity and novelty and turn the rankings into Elo scores, and an evolutionary sampler uses those scores to pick which sketches to extend. Provers can also call AlphaProof, DeepMind’s reinforcement-learning prover for olympiad-level Lean problems, on individual subgoals. AlphaProof gets a strict budget, typically 400 simulations, so it does not stall on goals that are hard or false.

Which open problems did it solve?

The main test used the Formal Conjectures collection, which contains Lean statements of open problems. DeepMind ran its full-featured agent on all 353 Erdős problems formalized there at the time, stopping after 3,000 episodes without a proof. It solved 9. The paper says two of the questions had been open for 56 years, and that after each solve, experts on the team checked that the Lean statement captured the original conjecture.

The agent also proved 44 of 492 open conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS). Gemini translated those conjectures into Lean automatically, which is error-prone, so the agent first had to prove “test lemmas” confirming the first few terms of each sequence matched its formal definition.

Beyond those benchmarks, the paper reports research use. On eight algebraic-geometry problems about Hilbert functions, from textbook exercises to open questions, the agent solved two of the four open ones, including a question about pure O-sequences open for about fifteen years. It proved an exact O(1/t) convergence rate for Anchored Gradient Descent-Ascent, a min-max optimization method, by finding a new step-size schedule. It proved a graph theory conjecture posed in 1996 by Graffiti, an automated conjecturing program, helped resolve a problem from Ben Green’s list of open problems, and is being used in quantum optics research.

DeepMind has published the Lean results in a GitHub repository under Apache-2.0 for code and CC BY 4.0 for other material, so anyone can re-check the proofs with Lean.

What did it cost, and did the extra machinery matter?

The paper puts the cost of each Erdős solve at a few hundred dollars of inference. AlphaProof added about 27.5 TPU hours, or roughly $60, per problem on v6e TPUs. The authors note that these figures understate the full cost of discovery, because running the agent over all 353 problems to find the tractable ones was itself a significant computational investment.

The more surprising result is the ablation. After the main run, the team tested the basic agent, the full-featured agent and two intermediate versions on the 9 solved Erdős problems. The basic agent, which is Gemini plus Lean with no evolution and no AlphaProof, solved all 9, though at higher cost on the harder ones. AlphaProof alone, and basic agents built on smaller models such as Gemini 3.0 Flash and Gemini 3.1 Flash-Lite, solved none.

In other words, the frontier model and the proof checker did most of the work, and the extra machinery mostly made the search cheaper. That makes the method easier for others to copy than the AlphaProof branding suggests, provided they can pay for a frontier model.

What went wrong along the way?

The paper is unusually direct about failure. Looking at the best-rated sketches on problems the agent did not solve, the authors found it often pushed the core difficulty into one helper lemma left as “sorry”, a restatement of the target in slightly different words. Prompting it not to do this did not stop it.

In several cases the top sketches relied on lemmas the agent claimed were known results from the literature. On manual inspection, those lemmas were hallucinations. The authors present both failures as an argument for end-to-end formal verification, and the logic holds: a hidden gap or invented citation cannot pass Lean, though it can pass a quick human read.

Formalization cut both ways. The agent helped find errors in the formal statements themselves; for Erdős problems #125 and #741(i), the formal versions were corrected to say “lower density” and “upper density” where the informal statements said only “density”. A machine-checked proof of the wrong statement is still the wrong result, which is why the human check of each statement matters.

How does this compare with OpenAI’s math manuscripts?

The publication landed two days after OpenAI released 722 AI-generated math manuscripts, many with Lean artifacts, and then withdrew three after a sign error. The two efforts differ in method. OpenAI produced a large library of prose papers and left the mathematics community to judge them; DeepMind reports a smaller set of results where the Lean proof is the deliverable and the paper went through peer review.

Both point the same way. Lean proofs are becoming the currency for AI mathematics claims, and they are being reused as training material, as Hugging Face showed by turning OpenAI’s proofs into reinforcement-learning environments. Specialised systems built for competitions, such as NVIDIA’s Nemotron IMO and IOI entries, test a different skill: solving set problems with known answers rather than open ones.

What should mathematicians make of it?

The paper is careful about where the agent works. Its successes are in combinatorics, convex optimization and number theory, where Lean’s mathematics library is mature and problems break into manageable subgoals. “Even most Erdős problems remain out of reach, let alone problems that require extensive new theory,” the authors write, and they note that the agents inherit the biases of their underlying models and show high variance between runs.

A solve rate of 2.5 percent on open Erdős problems is small, but each of those solves is machine-checked and cost a few hundred dollars in compute. For a working mathematician, the practical use is triage: run an agent over a list of formalized questions, read the proofs that compile, and study the failed attempts for ideas, as Avigad and Ballard suggest.

The open questions are about scale and credit. Formalizing problems correctly still takes expert time, compute for broad sweeps is not free, and journals and prize committees have not settled how to credit a proof found by an agent and checked by software.