A peer-reviewed Science paper made public this week shows Google DeepMind’s AlphaProof Nexus solved 9 of 353 open Erdős problems, with human mathematicians vetting many of the proofs.
The study says the system used multiple Gemini-powered agents, Lean proof-checking software and, for harder steps, the AlphaProof math model to generate and test proof attempts.
A simpler setup without shared agents or AlphaProof still solved the same 9 problems, suggesting stronger language models plus formal checking tools can handle some research math at lower cost.
Lean verification still has limits because mathematical statements can be mistranslated into code; an October 6 preprint flagged mismatches between parts of OpenAI’s written Navier-Stokes proof and its Lean version.
The publication lands amid a backlash over AI-generated math deluges: one Erdős-problem tracker shut comments and open/solved tags, while critics warn competitive releases are eroding collaboration and trust.