---
title: "Google DeepMind's AlphaProof Nexus Cracks 9 Math Problems Unsolved for 56 Years"
subtitle: "Google DeepMind's AlphaProof Nexus autonomously cracks 9 open Erdős problems and 44 OEIS conjectures using LLMs paired with Lean formal verification, at just a few hundred dollars per problem."
url: "https://alphasignal.ai/news/google-deepmind-s-alphaproof-nexus-cracks-9-math-problems-unsolved-for-56-years"
author: "AlphaSignal Newsroom"
author_url: "https://alphasignal.ai/editorial-team"
company: "AlphaSignal"
company_url: "https://alphasignal.ai/company/alphasignal"
published: "2026-05-21T17:24:57.000Z"
updated: "2026-07-13T23:05:51.310Z"
type: "Paper"
topics:
  - "Reasoning"
  - "Agents"
subtopics:
  - "Math Reasoning"
  - "Computer Use"
  - "Tool Use"
upvotes: 33
source_url: "https://arxiv.org/abs/2605.22763"
comments: 0
truncated: true
---

# Google DeepMind's AlphaProof Nexus Cracks 9 Math Problems Unsolved for 56 Years

> Google DeepMind's AlphaProof Nexus autonomously cracks 9 open Erdős problems and 44 OEIS conjectures using LLMs paired with Lean formal verification, at just a few hundred dollars per problem.

For 56 years, a problem posed by Paul Erdős and András Sárközy sat unsolved: does there exist an infinite set of positive integers satisfying a specific divisibility constraint while remaining dense enough to meet a precise growth condition? On May 21, 2026, a Google DeepMind AI agent resolved it autonomously, overnight, at an inference cost of a few hundred dollars. That problem was one of nine. Google DeepMind's AlphaProof Nexus, a system that fuses large language models with the Lean formal proof assistant, has autonomously cracked 9 out of 353 open Erdős problems and proved 44 out of 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS).

## The hallucination problem, solved with a compiler

The core challenge with using LLMs for mathematics research has always been reliability. LLMs can produce plausible-sounding proofs that contain subtle logical errors, and verifying them requires expensive expert review. AlphaProof Nexus addresses AI hallucination by pairing an AI model's generative capacity with formal proof-checking through the Lean proof assistant. The AI proposes a proof, and then a separate verification system checks every logical step. If the proof doesn't hold up, it gets rejected.

Lean is a proof assistant where every definition, theorem, and proof step is mechanically verified code. The key primitive is the `sorry` tactic, which closes a pending goal without actually proving it. A proof is only complete when the compiler reaches a state with no pending goals and zero `sorry` placeholders. This binary pass/fail signal is what makes the system trustworthy: there's no partial credit, no "looks about right."

![Architecture diagram of AlphaProof Nexus showing how mathematician input flows through Prover and Rater subagents with a Population Database to produce formal proofs](https://arxiv.org/html/2605.22763v2/x2.png) 

## Four agents, one framework

AlphaProof Nexus is built around a spectrum of four agent configurations, each adding capabilities on top of the last:

* **Basic agent (A):** Multiple independent prover subagents run in parallel. Each runs a "Ralph loop" , a multi-turn LLM session (Gemini 3.1 Pro) where the model edits a Lean proof sketch using a search-and-replace tool, gets compiler feedback after each edit, and iterates. As soon as one subagent finds a valid proof, all others stop.

_Preview only. Full text requires an AlphaSignal Pro account._

## Sources

- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://arxiv.org/abs/2605.22763)
- [Google DeepMind's AlphaProof Nexus solves 9 Erdős problems and proves 44 sequence conjectures](https://cryptobriefing.com/deepmind-alphaproof-nexus-erdos-problems/)
- [How DeepMind AlphaProof Nexus Cracks 56-Year-Old Math: Agentic LLM Loops and Lean Formal Verification](https://dev.to/monuminu/how-deepmind-alphaproof-nexus-cracks-56-year-old-math-agentic-llm-loops-and-lean-formal-45ei)
- [AlphaProof Nexus: DeepMind Solves 9 Erdos Problems](https://www.buildmvpfast.com/blog/deepmind-alphaproof-nexus-erdos-math-problems-ai-reasoning-2026)
- [DeepMind AlphaProof Nexus Explained: 4 System Paradigms for AI Math Research](https://luhuidev.medium.com/deepmind-alphaproof-nexus-explained-4-system-paradigms-for-ai-math-research-b09654ef97e4)