Overview
- DeepMind disclosed Monday that its system AlphaProof Nexus autonomously generated proofs for nine open Erdős problems and had those proofs checked step‑by‑step by the Lean proof assistant.
- Researchers also reported the system proved 44 OEIS conjectures, resolved a 15‑year algebraic geometry question, and found a new optimisation parameter while costing only a few hundred dollars of compute per problem.
- DeepMind says Nexus pairs a large language model reasoning stack with Lean so the system rejects unsupported claims and fake lemmas automatically rather than relying solely on human reading.
- The announcement intensifies a current debate because OpenAI used external mathematicians to review its recent Erdős result while DeepMind emphasizes machine verification, leaving independent peer review and publication processes still underway.
- Mathematicians told DeepMind that AI proof attempts helped them focus on unresolved steps, and the wider effect may be faster workflows and new collaboration norms but also stronger demands for open data and reproducibility.