AlphaProof Nexus reports formal proof-search results on open mathematics problems
A paper in *Science* reports that AlphaProof Nexus, an agent framework combining large language models with Lean-based proof verification, autonomously resolved nine of 353 open Erdős problems. Two of those problems had been open for 56 years. The paper also reports proofs of 44 of 492 open conjectures from the Online Encyclopedia of Integer Sequences, resolution of an open question in algebraic geometry, and an improved bound in min-max optimization.
The system alternates LLM-generated proof attempts with formal verification in Lean. The authors say even a basic agent using this alternating process replicated the Erdős results. The report demonstrates formal proof search on specified research problems; it does not establish that the system can solve arbitrary mathematics problems autonomously.