DeepMind’s nine proofs face a novelty test

A mathematical proof can read beautifully and still hide a gap that nobody spots for years. Google DeepMind's AI agent AlphaProof Nexus produced proofs for nine problems posed by Paul Erdős, and software checked every step. The work first appeared in a May preprint (arXiv) and was published after peer review in Science on 8 October (Science). Software could confirm the logic, but deciding whether that logic said anything new was a job for mathematicians.

A referee that cannot be charmed

Chatbots are good at writing mathematics that sounds right. A confident paragraph can paper over a missing step, and only a careful reader will catch it. AlphaProof Nexus avoids that trap by working in Lean, a programming language for stating definitions, claims and proofs so precisely that a computer can check them.

Think of Lean as a referee who reads every line of a finished proof and applies fixed rules. Style earns no points. If one step does not follow from the ones before it, the proof fails, however elegant the rest looks.

The team describes the agent as searching for proofs written in Lean. Researchers also gave it access to AlphaProof, an earlier DeepMind system built specifically for proofs. In the team's tests, a simpler setup gave the same results: a language model paired with Lean, without AlphaProof, still obtained all nine Erdős proofs (The Decoder). For those problems, the specialist component turned out to be unnecessary.

The paper reports accepted proofs for the nine Erdős statements and for 44 conjectures (claims believed true but never proven) from the Online Encyclopedia of Integer Sequences, a vast catalogue of number patterns (Science). Among the Erdős results is a two-part question about whole numbers that Erdős and András Sárközy posed in 1970. It stayed open for more than half a century (ABC).

What the referee cannot see

Lean's guarantee has a precise edge. It confirms that a proof establishes the statement exactly as it is written in code. Three questions lie beyond it: whether that code captures what Erdős meant, whether someone answered the question long ago, and whether the answer teaches anything.

The 1970 problem shows why the last two matter. Its second part implies the first, so a single proof settles both. Once the agent's proofs circulated, it emerged that a modest tweak to a construction in the original 1970 paper answers both parts as well (arXiv). The agent's proofs were correct. The problem had simply been closer to solved than its "open" label suggested.

Catching that kind of thing takes people who know the field. Gergely Bérczi, a mathematician at Aarhus University in Denmark and one of the authors, helped choose suitable questions and validate the solutions (Aarhus University). He also helped write versions of the proofs that human readers can follow. Lean vouched for each line, while Bérczi and his colleagues judged what the lines added up to.

That division of labour sets this study apart from a milestone last month. Then, Anthropic's Claude converted the already-known proof of Fermat's Last Theorem into Lean (To Brief). A translation of a famous proof raises no doubts about novelty. A search through statements treated as open does, and there the novelty check becomes the main event.

The team has published its proof files, so others can run them through the same referee (GitHub). The advance this study shows is specific. An AI agent produced machine-checkable proofs for some statements that mathematicians had treated as open, and the guarantee covers those statements as written in Lean. Working out what each proof added to mathematics still fell to the mathematicians who read them.