Google DeepMind’s AlphaProof Nexus pairs language-model proof generation with Lean, a proof assistant that mechanically checks formal proofs. In a study published October 8, 2026, the authors reported that the system proved 9 of 353 formalized Erdős problems and 44 of 492 selected conjectures from the Online Encyclopedia of Integer Sequences (OEIS). Two of the solved Erdős questions had been open for 56 years.
What AlphaProof Nexus does
AlphaProof Nexus searches for proofs of mathematical statements that have already been expressed in Lean. Rather than beginning with an ordinary-language question, the described workflow takes a Lean theorem and a proof sketch as input. Natural-language context can supplement that input, alongside mathematical knowledge encoded in Lean.
The key distinction is between proposing a proof and checking one. A language model can revise a proof attempt, but Lean’s compiler checks whether the formal proof satisfies the formal theorem. That feedback gives the system a mechanical way to assess each attempt.
What the reported results measure
The study reported results on two separate collections. Their counts have different denominators and describe different sets of mathematical questions.
| Evaluation set | Problems or conjectures proved | Items evaluated | Scope |
| Erdős problems | 9 | 353 | Erdős problems formalized in Lean and available in the Formal Conjectures repository for the study |
| OEIS conjectures | 44 | 492 | Selected open conjectures from the Online Encyclopedia of Integer Sequences |
The 353 Erdős statements were the formalized problems available in the repository at the time of the run; they were not the entire Erdős catalog, which contains more than 1,200 problems. The study authors also reported that two of the nine solved questions had been open for 56 years.
For the OEIS evaluation, the authors reported that manual review found the 44 proved conjectures correctly formalized and previously unproven. These results remain specific to their respective test sets; combining the counts would obscure what each evaluation measured.
How the proof-search loop works
In the basic configuration, language-model agents make edits to proof sketches, then use Lean’s compiler feedback to guide further attempts. The full-featured agent adds a shared pool of candidate sketches, ranks them with a language-model-based system, and uses evolutionary selection to develop promising attempts. It can also call AlphaProof to work on subgoals.
The paper names Gemini 3.1 Pro as the reasoning model for proof subagents and Gemini 3.0 Flash for agents that rate sketches. In a post-hoc comparison, the basic agent also solved all nine Erdős problems solved by the full-featured agent; the authors reported that relative costs varied across harder problems.
What the results do—and do not—show
Lean checks a proof against a formal statement. That check does not, by itself, establish that the formal statement captures the mathematician’s intended informal question. The study authors reported expert review of the Erdős formalizations, treating that correspondence as a separate part of the work.
Most of the evaluated Erdős problems remained unsolved. The authors said the agents’ successes clustered in areas such as combinatorics, convex optimization, and number theory, where Lean’s mathematical library is mature and problems can often be divided into tractable subgoals. AlphaProof Nexus’s reported results therefore concern formal proof search on prepared Lean inputs, rather than a general system for solving arbitrary mathematics questions.
