Google DeepMind’s AI solves nine open Erdős problems in peer-reviewed study

Google DeepMind’s peer-reviewed math study contains a surprise: its most elaborate setup was not needed for its nine Erdős successes. AlphaProof Nexus solved nine of 353 open problems, but independent Gemini agents using a proof checker matched those results. The study also included human vetting of many proofs, adding scrutiny beyond the software’s checks.

Published October 8 in Science, the study describes how the system searched for proofs and how researchers tested different configurations. The work first appeared as a preprint earlier this year. The team had also shared its Erdős solutions online before the journal publication.

Two of the solved Erdős problems had remained unresolved for 56 years. The study’s results extended beyond that collection, covering conjectures about integer sequences and questions in other branches of mathematics. According to The Decoder’s account of the study, AlphaProof Nexus also:

• Proved 44 conjectures from OEIS, a database of integer sequences.
• Solved an open question in algebraic geometry.
• Improved a known bound in min-max optimization, a technique used to train some AI models.

Draft, check, revise—and share

AlphaProof Nexus is built around Gemini 3.1 Pro, which drafts and revises proofs in Lean, a formal language that lets software check mathematical reasoning. Lean checks each draft after an edit. Its error messages then guide the system’s next attempt, creating a repeated cycle of proposed steps, checks and revisions.

For the Erdős collection, multiple Gemini-powered agents could consult AlphaProof, a specialized mathematical proof model, on difficult steps. They also shared work with one another. Promising proof attempts circulated among the agents, while attempts that were not progressing were discarded. The full setup therefore combined software checking, collaboration and access to a specialist.

Removing the specialist did not remove the successes

The researchers then tested a stripped-down configuration on the nine problems the full system had solved. Independent Gemini agents used Lean’s feedback, but neither exchanged proof attempts nor called AlphaProof. They solved all nine too—a result that surprised study co-author Swarat Chaudhuri, a Google DeepMind research scientist.

That comparison has a narrow scope. The team did not establish whether the simpler configuration could solve any problems the full system missed. Matching the successful cases is not the same as matching performance across the entire collection. Chaudhuri said the result suggests increasingly capable language models can tackle research mathematics with relatively simple checking tools.

A checked proof still needs the right question

Lean checks the statement encoded in its language, not whether that statement correctly translates the mathematical question someone intended to ask. Errors can enter when moving between ordinary mathematical writing and code. Human mathematicians vetted many proofs in the DeepMind study, providing a layer of review beyond a successful software check.

Chaudhuri told Science News that humans still need to think through problems and set goals for the system. Even unfinished proof attempts could help: their checked steps let mathematicians concentrate on the gaps that remained. His stated objective is to advance mathematics as practiced by human researchers, rather than simply accumulate machine-produced answers.