Google DeepMind's AlphaProof Nexus Solves 9 Open Erdős Problems, and Science Signed Off

Google DeepMind's AlphaProof Nexus autonomously resolved 9 of 353 open Erdős problems it attempted, and the work has passed peer review at Science, which dates the paper October 8, 2026. The same system proved 44 of 492 conjectures drawn from the Online Encyclopedia of Integer Sequences (OEIS), according to the paper.

The press release is generous with adjectives. The eval table is more interesting, so let us read that.

What the system is

AlphaProof Nexus is a framework, built by DeepMind researchers and collaborating institutions, for agents that query frontier models and the Lean compiler to produce formal proofs. Lean is the point: the agents get compiler feedback, not just another model saying the proof sounds right.

The basic agent (Agent A) is a set of independent prover subagents with no shared state. Each runs what the paper calls a "Ralph loop": multi-turn inference loops based on Gemini 3.1 Pro, with a search-and-replace tool to refine a proof sketch.

The full-featured agent (Agent D) adds optional calls to AlphaProof and an evolutionary algorithm. That algorithm coordinates a population database, and Gemini 3.0 Flash evaluates the sketches and assigns them Elo ratings.

The numbers

The full-featured agent solved 9 of 353 Erdős problems, including two questions open for 56 years, at an inference cost of a few hundred dollars per problem. That is a hit rate of about 2.5 percent, which is a fine result on problems that humans have not cracked and a poor one if you were promised a mathematician in a box.

On OEIS, it proved 44 of 492. A manual review found those 44 to be correctly formalized and previously unproven. The review matters because the conjectures were autoformalized, and a proof of a mistranslated statement is a proof of nothing.

The paper also reports results beyond those two sets:

• Algebraic geometry: Zanello's conjecture on log-concavity of pure O-sequences, for codimension 3 and type 2.
• Optimization: an exact O(1/t) convergence rate for Anchored Gradient Descent-Ascent, tightening a slower published bound. The agent found a novel parameter schedule along the way.
• Graph theory: a conjecture posed in 1996 by the automated conjecturing system Graffiti, on spanning-tree leaves.
• Additive combinatorics: a counterexample disproving a conjecture from Ben Green's list (problem #57).
• Quantum optics: with Mario Krenn, multiple conjectures on monochromatic quantum graphs, in particular N=d in {4, 6, 10}.

The footnotes

Here is the part the headline skips. In post-hoc ablations, the basic agent solved all 9 Erdős problems too. The paper's own word is "Remarkably", and it adds that the cost was higher on the harder problems. AlphaProof in standalone tree-search mode, and basic agents built on smaller models (Gemini 3.0 Flash, Gemini 3.1 Flash-Lite), solved none.

So the lesson is about the base model more than the machinery. An analysis from Science Media Centre España calls the design "over-engineering" and "evolutionary fireworks". The DeepMind authors, for their part, maintain that Agent D pays off on harder problems such as Erdős #125 and #138. Both readings can be true, and the paper gives you the data to check.

A second footnote is the price. AlphaProof execution cost roughly 27.5 TPU hours ($60) per problem on v6e TPUs, and that cost is excluded from the reported comparison metrics for agents B and D. Sixty dollars is not ruinous. It is simply excluded from the reported Agent B and D comparison metrics.

A third, smaller one: EurekAlert credits the work to "George Tsoukalas and colleagues", while the arXiv author list does not include him. Neither document explains the mismatch.

Why peer review is the story

The Decoder frames the Science publication against OpenAI, writing that it "recently dumped hundreds of AI proofs on GitHub instead of submitting them to journals", that the Association for Human Mathematics, led by Terence Tao, called for a boycott, and that "Deepmind put its work through peer review." The reporting does not say what specifically triggered the boycott call.

DeepMind also released the Lean proofs and natural-language proofs on GitHub, with software under Apache 2.0 and other materials under CC-BY 4.0. That is the right combination: peer review and publicly released proofs.

Jeremy Avigad and Matthew Ballard, in a Perspective accompanying the paper, write that 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 modest claim, and it is the most believable one in the package.

What to watch

First, the full list. The excerpts detail only some of the nine Erdős problems (#12(i), #12(ii), #26, #125, #138 and #741(i)), so check the repository for the rest.

Second, whether outside mathematicians reproduce the 44 OEIS results and the cost figures with the code and proofs now public.

Third, the 344 Erdős problems that Agent D attempted and did not solve. A 2.5 percent success rate on hard problems is a result. What the failures look like is the next paper.