Google DeepMind's AlphaProof Nexus solved nine formalized Erdős problems, Science paper shows

Google DeepMind's AlphaProof Nexus solved nine of 353 formalized Erdős problems and 44 of 492 selected conjectures from the Online Encyclopedia of Integer Sequences, according to a paper published in Science on October 8, 2026. The work is a substantial demonstration of an AI system producing research mathematics with machine-checkable proofs rather than relying only on human inspection of generated prose.[1][2] The system also produced results in graph theory, algebraic geometry, convex optimization and quantum optics. Among the reported examples are a proof that every pure O-sequence of codimension 3 and type 2 is log-concave, an optimization result involving an anchored gradient descent-ascent method, and proofs concerning graph reconstruction and monochromatic quantum graphs.[1][5] The Erdős evaluation covered a formalized subset of a much larger catalog of open problems. DeepMind ran its most capable configuration on all 353 Lean statements available in the test set and stopped an attempt after 3,000 episodes without a proof. The paper reports nine successful results, including two questions that had remained open for more than 50 years.[1][2] The broader evaluation found 44 solved conjectures out of 492 selected OEIS problems. In a separate algebraic-geometry result, the system established the remaining codimension-3, type-2 case of a log-concavity conjecture concerning pure O-sequences. The authors also describe an optimization experiment in which the agent found a parameter schedule that produced an exact convergence-rate result for an anchored gradient descent-ascent method.[1][5] These results vary in mathematical scope. They are verified solutions to precisely stated formal problems, not evidence that the system can independently choose important questions, build a new mathematical theory or replace a research mathematician across fields. The 9-of-353 result also shows how selective the capability remains.[1] AlphaProof Nexus starts with a Lean theorem containing a `sorry` placeholder, together with a proof sketch and, where available, natural-language context. Gemini 3.1 Pro-based prover agents edit the file, compile it and use Lean's error messages to revise their attempts. The full system adds AlphaProof for difficult subgoals, a shared population of proof sketches, language-model-based ranking and an evolutionary search process.[1] A candidate is accepted only when the theorem compiles without `sorry` and the original statement remains intact. DeepMind says its SafeVerify process checks the proof specification and guards against environment exploits such as axiom injection. Compilation and formal validation run inside isolated Docker sandboxes using Lean 4.27.[1] This is a stronger audit trail than an AI-generated proof in ordinary mathematical prose. The project has released the Lean files and selected natural-language versions in a public GitHub repository, where users can rebuild the project with Lean and run `lake build`.[1][3] Lean verifies that a formal proof follows from a formal statement and the imported library. It does not decide whether the formal statement matches the intent of an informal Erdős problem, whether the result was already implied by earlier literature or whether the chosen problem was genuinely open. The paper says the system helped detect ambiguities in some formalizations, including questions involving different meanings of density.[1] That distinction has already affected the headline count. An independent audit of the public files concluded that Erdős problem 846 had a valid formal proof but that an older theorem by Reiher, Rödl and Sales already implied the result after translation. Under the audit's stricter definition of a newly resolved problem, the total becomes eight rather than nine. The audit did not invalidate the Lean proof; it changed the classification of the mathematical discovery.[6] Outside experts have emphasized the system's boundaries. A Science Media Center review said AlphaProof Nexus is strongest where formal libraries are mature and problems can be decomposed into manageable subgoals, such as combinatorics and number theory. It also noted that the agent itself is not publicly available, limiting independent experimentation with the system rather than with its released outputs.[7] In a related Science perspective, Jeremy Avigad and Matthew Ballard argued that unsuccessful AI proof attempts could still help mathematicians understand the structure of difficult problems. That frames the nearer-term contribution more narrowly: AlphaProof Nexus is a formal proof-search system and research tool, not a general-purpose autonomous mathematician.[4] The stories that matter, in one email. Free — unsubscribe anytime.