A paper published in Science on October 8, 2026, reports that Google DeepMind’s AlphaProof Nexus resolved 9 of 353 open Erdős problems and proved 44 of 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS). Two of the Erdős problems had been open for 56 years. The paper describes a system that generates candidate proofs with a large language model (LLM) and checks them with Lean, a formal proof assistant. (The paper in Science)
What AlphaProof Nexus achieved
The paper reports two separate results: AlphaProof Nexus resolved nine problems in a set of 353 open Erdős problems, and proved 44 conjectures in a separate set of 492 open OEIS conjectures. The two counts concern different collections, so each result is tied to its own set and denominator.
Two of the Erdős problems had remained open for 56 years. The reported count covers the system’s results across the evaluated collection; it does not identify those two problems here.
How proof generation and Lean verification work
AlphaProof Nexus alternates between LLM-generated proof attempts and Lean’s formal verification. Lean checks the proof steps in a format that its system can verify, providing a check of the formal proof rather than a plain-language explanation.
The paper also reports that a basic agent alternating LLM generation with Lean verification reproduced the nine Erdős results. That finding shows the same results could be reproduced with this simpler generation-and-checking setup.
