Overview
- DeepMind reported that AlphaProof Nexus autonomously produced formal, Lean‑checked proofs for nine open problems posed by Paul Erdős, plus 44 OEIS conjectures and a 15‑year algebraic geometry question, claims published by the team after OpenAI’s recent math announcement.
- DeepMind says the system pairs a large reasoning model with the Lean proof assistant so every logical step is mechanically checked, which the company argues reduces the chance of AI 'hallucinations' where models invent lemmas or skip hard steps.
- OpenAI’s earlier result — a model-produced counterexample to the planar unit distance Erdős conjecture — relied on external mathematicians for review, highlighting two validation paths now competing in the field: human peer review and automated formal verification.
- Researchers flagged that independent scrutiny is still essential because machine verification depends on correct formalization and the community has yet to complete audits; DeepMind also reported unusually low compute costs of a few hundred dollars per solved problem, a claim that will affect adoption if verified.
- DeepMind CEO Demis Hassabis and several experts stressed these advances do not equal artificial general intelligence and the next steps are broader peer review, public release of formal artifacts, and replication before the results change mathematical practice.