Google DeepMind’s AlphaProof Nexus paper published in Science

On 8 October 2026 Science published Google DeepMind’s paper on AlphaProof Nexus, a framework of LLM agents that search for formal proofs in Lean. The preprint (arXiv 2605.22763) had appeared on 21 May 2026 and was covered then by the tech press. Publication in Science, after peer review, brought a second wave: an EurekAlert release, expert reactions from the Spanish Science Media Centre, a Science Perspective by Jeremy Avigad and Matthew Ballard, an “Expert Voices” piece by Emily Riehl in the same issue, a Pushmeet Kohli thread on X, and on 10 October a viral summary by @Dr_Singularity.

The system pairs Gemini 3.1 Pro prover subagents with the Lean compiler. Every proposed proof is machine-checked, and failed attempts feed back into the next try. The paper compares a basic agent (independent subagents plus compiler feedback) with a full-featured agent, which coordinates subagents with an evolutionary algorithm, ranks proof sketches with Gemini 3.0 Flash raters and can call AlphaProof (the 2024 RL prover) as a tool.

Results (from the paper):

• Erdős problems: 9 of 353 attempted, autonomously, at a few hundred dollars of inference per problem. The 9 are formal sub-questions: #12(i), #12(ii), #125, #138, #152, #26, #741(i), #741(ii) and #846, several in variant forms. The two “open for 56 years” are #12(i) and (ii), posed by Erdős and Sárközy in 1970. In a post-hoc ablation, the basic agent also solved all 9, at higher cost on the hardest ones.
• OEIS: Gemini autoformalized 492 open conjectures from the Online Encyclopedia of Integer Sequences. The agent proved 44 that manual review judged correctly formalized and previously unproven.
• Research deployments: an exact O(1/t) last-iterate rate for Anchored Gradient Descent-Ascent in min-max convex-concave optimization, found together with a new step-size schedule. With Gergely Bérczi (Aarhus), it solved 2 of 4 open problems on Hilbert functions, including Zanello’s log-concavity conjecture for pure O-sequences in the (codimension 3, type 2) case. It also helped resolve a problem from Ben Green’s list, found misformalizations in the literature and supported quantum optics work with Mario Krenn.

This is a peer-reviewed, fully formal account of LLM agents solving open research problems at scale and at low cost. Its main finding, that a simple generate-and-check loop does about as well as a complex agent, supports the view that model capability, not agent engineering, now drives AI mathematical discovery.

• Lean-verified and peer-reviewed. All proofs are public Lean files (github.com/google-deepmind/alphaproof-nexus-results), and erdosproblems.com credits DeepMind on the pages of the solved problems. Science’s article pages were not readable for this entry (HTTP 403). Volume and pages come from Science’s RSS table of contents; the received and accepted dates come from press summaries.
• Not all fully new. On erdosproblems.com, #741 and #846 are credited to DeepMind and an internal OpenAI model, found independently. The #846 page notes that a counterexample also follows from a theorem of Reiher, Rödl et al. Several solutions settle variants or single parts of a problem.
• Critics. Anatol Wegner’s blog (31 May, written with Gemini assistance; not peer-reviewed) argues that some “open” problems had prior literature and that the agent exploited loose formalizations. These are his claims and were not checked here. The Perspective and Riehl’s piece were seen only as titles in Science’s table of contents (the pages return HTTP 403 to us); their text is not summarised here. In the SMC Spain reactions, Josep Curto (UOC) called the system “a severe case of over-engineering”, since the basic agent matched it. Javier Aramayona (ICMAT-CSIC) warned of results “known to be true” that “no one fully understands”. Pablo Haya Coll (UAM) and Teodoro Calonge (Valladolid) were positive.
• In May, WION reported Demis Hassabis saying AGI is still far away despite the result, and a video posted to Hacker News was titled “Hassabis said solving Erdős isn’t real invention” (not checked against the video).

Measured by count, AlphaProof Nexus is now well behind later systems. The OEIS Open benchmark (arXiv 2608.11941) reports 147 of the same 492 formalised OEIS conjectures resolved at $50 per attempt. OpenAI’s 6 Oct release lists 722 manuscripts, but only 162 are Lean-formalized and their review is marked “unchecked”. The 44 OEIS and 9 Erdős results were obtained with a May 2026 model. What sets this paper apart is that every result is formally verified and the work passed peer review in a top general-science journal.