AlphaProof Nexus — AI Agents That Solve Open Problems With Lean Checking Every Step

AlphaProof Nexus is a framework for AI agents that tackle open mathematical problems, described by 21 Google DeepMind researchers in a paper posted on arXiv on 21 May 2026. A large language model writes proofs, and the compiler of the Lean proof assistant checks them step by step. By repeating that loop, according to the paper, its most capable agent "autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars", two of them open for 56 years since 1970. The peer-reviewed version was published in Science on 8 October 2026.

The day before, on 20 May, OpenAI had announced its disproof of the unit distance conjecture, so two AI companies were competing over Erdős problems on consecutive days. The difference lay in method. OpenAI's result was a natural-language proof checked by human mathematicians; AlphaProof Nexus counts only proofs that Lean accepts.

How it works: an AI that writes, and Lean that checks

The paper opens by noting that language models increasingly excel at mathematical reasoning, "but their unreliability limits their utility in mathematics research." Its mitigation is to have them write proofs in a formal language such as Lean, in which a compiler automatically verifies every logical step.

The user supplies a Lean file containing the target theorem with "sorry" in place of a proof. The agent adds lemmas and definitions, and when Lean reports an error it uses the message to repair the attempt. The full-featured agent can call AlphaProof (2024) as a focused tool to dispatch sub-goals.

Results

Problem #12, posed by Erdős and Sárközy in 1970, concerns sets of integers in which no element divides the sum of two larger elements; several mathematicians had obtained partial results. The agent built its answer from "blocks" placed along a rapidly growing sequence. Problem #125, open since 1996, asks about the sum of the set of numbers written with only the digits 0 and 1 in base 3 and the analogous set in base 4.

Even the simplest agent succeeded

Afterwards the team compared all four agents on the nine Erdős problems the full-featured agent had solved. "Remarkably, the basic agent solved all 9 problems, though at a higher cost on the harder problems," the paper says. Its authors read this as pointing "to an ongoing shift from specialized trained systems toward simple agentic loops as LLMs become more capable."

The failure analysis was candid. The agent often pushed a problem's core difficulty into a single helper lemma marked "sorry" that merely restated the target, and explicit prompting against this failed to stop it. On several problems, its best attempts relied on lemmas that the agent claimed were established results in the mathematical literature; "Upon manual inspection, these lemmas proved to be hallucinations." The paper argues that such failures underline the value of end-to-end formal verification against hallucination.

Reception: how to read 2.5%

The Decoder pointed out that 9 of 353, about 2.5%, is close to Terence Tao's estimate that AI can solve only 1–2% of Erdős problems. Most remain out of reach, and the successes cluster in areas such as combinatorics and number theory. The 353 problems were also only the open ones already formalised in Lean, out of the 652 open problems listed on erdosproblems.com in August 2026. The results published on GitHub include only successes, but the repository also lists every Erdős problem attempted, so outsiders can check the success rate.

Quanta Magazine observed that problems to which Erdős once attached his own cash prizes are now discussed in terms of their per-problem cost, the price of the tokens needed to solve them. The AlphaProof Nexus paper put exactly that cost forward as a headline measure.

What changed, and for whom

AI with formal verification moves the burden of checking from people to machines. Anyone can re-run a Lean proof locally, which answers one weakness of natural-language AI proofs: that their correctness is unknown until a human reads them through. It also creates a new state, in which a formal proof exists but no human has understood it. In July 2026 the Erdős problems community began labelling such problems "open (Lean)"; that debate is covered in Erdős problems and AI (2026).

The paper also says the agent is being deployed in research on combinatorics, optimisation, graph theory, algebraic geometry and quantum optics. Proof-search tools entering mathematicians' everyday work mark a new stage in the history of computers and proof that runs from the four color theorem (1976) through Flyspeck (2014). The thread is on the AI and mathematics timeline.