Google DeepMind’s AlphaProof Nexus solves Erdős problems

Proofs, checked by Lean

AlphaProof Nexus is built on Gemini 3.1 Pro, which writes and revises proofs in Lean, a formal language. Lean checks each revision; its error messages guide the system’s next attempt. For harder subproblems, Nexus can call on AlphaProof, a specialised proof tool.

Google DeepMind says nine Erdős problems were solved without AlphaProof. The announcement reports nine solutions among 353 problems; it does not say how the system performed across the full set.

The team also reports a solution to an open problem in algebraic geometry and an improvement to a known bound in minimax optimization. Those claims broaden the range of the announcement, but the article does not provide further detail about the problems or the new bound.

Peer review is part of the result

The submission comes amid debate over how AI-generated mathematics should be evaluated. OpenAI recently posted hundreds of AI-generated proofs on GitHub rather than sending them to scientific journals. The Association for Mathematics for Humanity, led by Terence Tao, called for a boycott of that approach. Google DeepMind chose to submit its work for peer review.

I think the distinction matters, but submission is not validation: the announcement does not say what reviewers have concluded. What I’d want to know is how much of the reported work survives independent checking, and how the results compare with what mathematicians could verify without the system. Until then, the strongest case for AlphaProof Nexus is not just that it produces proofs, but that its claims are being put through a process that could test them.