Google DeepMind in Science: a Lean formal proof agent resolves 9 of 353 open Erdős problems and 44 OEIS conjectures, and a basic generate-and-verify loop replicates the Erdős results

Why it matters

【Key points】

The Oct 8 issue of Science (vol. 394, no. 6820, pp. 234–239) carries a Google DeepMind paper, "Advancing mathematics research with AI-driven formal proof search." Nearly all 20 authors are at Google DeepMind, including Thomas Hubert, Matej Balog and Pushmeet Kohli.

The team built a formal proof search agent: a large language model writes proofs in Lean, the Lean compiler checks every step, and failures are fed back for another attempt. According to the abstract, the agent autonomously resolved 9 of 353 open Erdős problems, proved 44 of 492 open conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS), and is now being used in combinatorics, optimization, graph theory, algebraic geometry and quantum optics research.

The paper also ran a control: a basic agent that simply alternates LLM generation with Lean verification replicated all nine Erdős results.

【Verifiable】

The DOI is 10.1126/science.aej2213; Crossref lists an Oct 8, 2026 publication date and author affiliations. The 9/353 and 44/492 figures and the basic-agent replication are stated in the abstract.

【Our read】

Compare OpenAI's 722 natural-language math manuscripts this week, where one sign error forced 3 withdrawals and 14 revisions within two days. DeepMind's output is far smaller, but every proof is machine-checked line by line, so correctness no longer rests on human review. We think the next contest in AI mathematics is not volume but whether results can be verified by machine.

That a basic agent replicates the results suggests the gains come mostly from the underlying model plus a reliable verifier, not from elaborate search scaffolding.

The limits matter too: 9 of 353 is roughly a 2.5% hit rate, so most open problems remain out of reach, and Lean only guarantees that a proof matches its formal statement. Whether that statement faithfully captures the original problem still needs a mathematician's check.