What the paper claims
A Google DeepMind team has published a peer-reviewed account of an AI system that finds mathematical proofs and has them machine-checked as it goes. The paper, “Advancing Mathematics Research with AI-Driven Formal Proof Search” by Tsoukalas and colleagues, appeared in Science on 8 October.
The system, AlphaProof Nexus, is built around Gemini 3.1 Pro. It drafts a proof in Lean, a formal language in which every logical step is verified by software, and the checker’s error messages steer the next draft. For harder sub-problems it can hand off to AlphaProof, DeepMind’s specialised proof tool.
The researchers selected 353 open problems from the Erdős collection and encoded them in Lean. The system closed nine of them — about 2.5% — two of which had stood unsolved for 56 years. It also proved 44 conjectures from the On-Line Encyclopedia of Integer Sequences, settled an open question in algebraic geometry and improved a known bound in min-max optimisation, a technique used in training some AI models.
The ablation is the interesting part
DeepMind reports that the system solved the same nine Erdős problems without AlphaProof. An ablation analysis found that a simpler configuration, which the paper labels Agent A, reached the same nine, a point raised by Josep Curto of the Open University of Catalonia in expert comments collected by Science Media Centre España. Curto reads the result as a sign of over-engineering, and argues the paper carries methodological inconsistencies.
His sharper point is about what formal verification does and does not buy you. Lean, he notes, guarantees that a proof is logically valid. It does not guarantee that the statement someone formalised is the problem they meant to state. The translation from an informal conjecture into Lean is still a human step, and an error there survives the checker untouched.
How nine out of 353 should be read
The denominator matters. This is nine successes out of a defined set the team chose and formalised, not a general ability to pick off famous conjectures. Pablo Haya Coll of the Autonomous University of Madrid, in the same set of comments, points to the methodology rather than the count: the value is a repeatable way of generating mathematical discoveries, not the nine themselves.
Javier Aramayona, who directs Spain’s Institute of Mathematical Sciences, raises the issue that follows from machine-checked proofs arriving faster than anyone reads them: many AI-generated results are verified and yet not fully understood. Teodoro Calonge of the University of Valladolid called it a high-quality article and an early attempt, with considerable room for improvement.
The contrast with the other lab
The route this work took is itself part of the story. DeepMind posted the Erdős solutions publicly before the paper appeared, then put the work through peer review. OpenAI took the other route, publishing hundreds of AI-generated proofs to a repository, which is what prompted a group of mathematicians to call for a boycott of the company earlier this month.
What to watch is whether the Lean files hold up to outside scrutiny, and whether any of the nine formalisations turn out to state something other than the Erdős problem they are labelled with. That check is now available to anyone, which is the practical argument for the route DeepMind chose.
