DeepMind AlphaProof Nexus appears in《Science》: autonomously solves 9 Erdős problems

Google DeepMind's automated mathematical proof system AlphaProof Nexus appeared in the October 8 issue of《Science》, autonomously solving 9 of 353 open Erdős problems, two of which had remained open since 1970. The system uses Gemini 3.1 Pro to draft proofs in Lean, with a compiler verifying line by line and feeding back iterations; the reasoning cost per problem is several hundred dollars. The paper's ablation results show that a simplified system that removes complex structures such as the sub-agent tournament and retains only the large model plus Lean feedback can also solve these 9 problems, though the hardest few are more expensive.