Google DeepMind’s AlphaProof Nexus Is Published in Science: 9 of 353 Erdős Problems, 44 of 492 OEIS Conjectures, by the Authors’ Own Account

Google DeepMind’s AlphaProof Nexus, an AI system that writes mathematical proofs and has a computer check them, was published in the journal Science on 8 October 2026 [1][2]. That the paper exists and what it claims is confirmed. The results are the authors’ own claims, and TSN has not re-checked any proof.

What the release and the paper say

The American Association for the Advancement of Science (AAAS) release says: “In tests, the system was able to solve nine of the 353 attempted Erdős problems, including two that had remained unsolved for more than 50 years. It was also able to solve 44 of 492 open On-Line Encyclopedia of Integer Sequences (OEIS) conjectures” [1]. Science’s editor’s summary says the two had “been open for 56 years” [2].

Erdős problems are open questions posed by the mathematician Paul Erdős and his collaborators; the authors cite an online catalogue of “over 1200” [3]. The OEIS is an online catalogue of whole-number sequences and their known and open properties [3].

What “solved” means here

The system alternates between an AI model writing a proof and Lean, a proof checker whose compiler verifies every step [2]. The Science abstract says the agent “autonomously resolved nine of 353 open Erdős problems” [2]. The authors add that after each one, “experts on our team validated that the Lean statement faithfully captured the original conjecture” [3]. For the OEIS, they counted 44 conjectures “that a manual review found to be correctly formalized and previously unproven” [3].

Cost

The arXiv abstract says “at the per-problem cost of a few hundred dollars” [3]. The paper adds: “The reported costs also do not capture the full cost of discovery: we applied the full-featured agent to all 353 Erdős problems in Formal Conjectures, and identifying tractable problems was itself a significant computational investment.” [3]

What this does not show

• A general success rate. The 353 were not a random sample: the problems were those the community had formalized in Lean, and the authors “recognize that this process has a bias toward problems amenable to formalization in Lean” [3]. The OEIS set was 492 conjectures after a model chose 500 from 2,649 open ones and 8 were dropped [3]. Nine of 353 is the authors’ result on that set.
• That a special system is needed. A basic agent “replicated the Erdős successes but proved costlier on the hardest problems” [3].
• Independent checking by TSN. The Lean proofs are public [4]; TSN did not run them or read the Science Perspective by Jeremy Avigad and Matthew Ballard beyond a sentence in the release [1].

Related on TSN: OpenAI’s 372 math and CS results: Lean helps, independent checks pending

Sources

1. AAAS, “Introducing AlphaProof Nexus: An AI tool for formal mathematical proof discovery”, news release, 8 October 2026. https://www.eurekalert.org/news-releases/1146436
2. Tsoukalas et al., “Advancing mathematics research with AI-driven formal proof search”, Science 394, 234-239, 8 October 2026 (abstract and editor’s summary read). https://www.science.org/doi/10.1126/science.aej2213
3. Tsoukalas et al., “Advancing Mathematics Research with AI-Driven Formal Proof Search”, arXiv:2605.22763 (preprint; v1 21 May 2026, v2 8 June 2026). https://arxiv.org/abs/2605.22763
4. Google DeepMind, alphaproof-nexus-results (Lean proofs), GitHub. https://github.com/google-deepmind/alphaproof-nexus-results