THE HOOK
Google DeepMind's maths agent has gone from Olympiad party tricks to closing problems that sat open for 56 years.
THE GIST
A peer-reviewed study in Science says AlphaProof Nexus, a Gemini-based agent checked by the Lean proof compiler, solved 9 of 353 Erdős problems it attempted and 44 of 492 open OEIS conjectures. The paper puts inference cost at a few hundred dollars per solved problem.
THE TAKE
This is the right way to do AI maths: machine-checked proofs, a proper journal, and the files out in public for anyone to poke at. Formal verification kills the hallucination problem stone dead. The catch is the headline number, which is softer than it looks. Still, a few hundred dollars per open problem is a bargain.
OPINION
The proofs sit in DeepMind's results repo, and an independent audit already trims the nine to eight because one answer was implied by older work. Several others are variants or parts of the same entry, so "nine Erdős problems" really means a handful of genuinely new results, which is still a very good year for anyone.
- Story type: Important story
- Impact: Medium
- Confidence: High (official announcement)
- Audience: Researchers
- What changed: A peer-reviewed Science paper reports DeepMind's AlphaProof Nexus produced Lean-verified proofs for 9 of 353 Erdős problems and 44 open OEIS conjectures.
- What to watch: Further community audits of the Erdős results and whether mathematicians adopt the agent as a routine research tool.
- Reading time: 1 minute
