The AlphaProof Nexus agent, developed by Google DeepMind, has successfully solved 9 out of 353 open mathematical problems associated with Paul Erdos. Two of these problems had remained unsolved for 56 years. The system also proved 44 out of 492 open hypotheses from the Online Encyclopedia of Integer Sequences.
Unlike standard chatbots, the system utilizes Lean, a language and environment for formalizing mathematical proofs. The AI generates a formal proof, which Lean then verifies step-by-step. If an error is detected, the agent receives feedback to refine its search. Each solved Erdos problem cost several hundred USD in computational resources.
The architecture employs multiple AI agents working in parallel, coordinated by an evolutionary algorithm and the AlphaProof system, which relies on reinforcement learning. A simpler version of the agent also solved the nine Erdos problems but proved more expensive on complex tasks, highlighting the importance of search organization.
Beyond Erdos problems and OEIS hypotheses, the system has addressed challenges in algebraic geometry, convex optimization, and graph theory, while also identifying errors in existing scientific literature. However, it still faces limitations, particularly with tasks requiring the development of entirely new mathematical theories.
