DeepMind's AlphaProof Nexus cracks decades-old math puzzles for cheap

For decades, tackling a math problem left unsolved by human minds meant years of lonely whiteboard work and dense academic debate.

DeepMind just turned that into a background computing job that costs less than a decent dinner party.

Google DeepMind published its paper on AlphaProof Nexus, an AI agent designed to generate machine-verified mathematical proofs. Out of 353 open math problems attempted, the system autonomously cracked nine Paul Erdős problems spanning combinatorics and graph theory. Two of those problems had been sitting unsolved for 56 years, untouched since 1970.

On top of that, the system verified 44 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS).

The Lean verification loop

AlphaProof Nexus works by pairing an LLM with Lean, a formal proof assistant.

Instead of trusting an LLM's natural language answers, which are notorious for subtle hallucinations in rigorous math, Nexus uses Lean as a ruthless gatekeeper. The LLM generates candidate proofs in formal code, Lean checks every single logical step, and if the proof fails, the agent iterates until it finds one that compiles cleanly.

The full version of the agent even integrates evolutionary algorithms to guide the search process. A simpler version DeepMind tested could match the same results, but ended up costing significantly more compute.

With this setup, the inference cost to resolve each problem dropped to just a few hundred dollars.

Firing back at OpenAI

The timing here is impossible to ignore.

Just days before DeepMind's drop, OpenAI celebrated a major win by disproving an 80-year-old Erdős conjecture. That came several months after OpenAI had to walk back an earlier claim about solving 10 novel problems.

DeepMind essentially answered OpenAI's headline with a fleet of nine solved problems, backed by rock-solid machine verification.

Still, the researchers were clear about the tool's ceiling. Problems that require brand-new mathematical machinery or novel conceptual frameworks remain entirely out of reach for the system.

Why it matters

We think this marks a critical shift in how frontier AI is evaluated.

For the past two years, every lab has bragged about acing competition benchmarks like the Math Olympiad. AlphaProof Nexus proves that AI is ready to graduate from standardized tests to genuine research assistance on unsolved territory.

For working mathematicians, this changes the day-to-day workflow. Formalizing proofs in Lean has traditionally been so painful that few researchers bother. An agent that can churn through open conjectures for a few hundred dollars turns mathematical proof-checking into a scalable background service.

It also highlights why formal verification is becoming the holy grail for reasoning models. By putting the LLM inside a strict compiler loop, DeepMind sidesteps the hallucination problem entirely.

While Nexus still cannot invent fundamentally new mathematical concepts from scratch, automating the grind of combinatorial discovery is already a massive leap forward.