The problem
Most AI results in mathematics come with informal proofs that people then have to check. AlphaProof Nexus, from Google DeepMind, searches directly for proofs in the Lean proof assistant, so a result is either machine-checked or not produced at all.
What AI did
The paper (Tsoukalas et al., arXiv:2605.22763, May 2026; published in Science on 8 October 2026) reports that the system autonomously proved 9 of 353 open Erdős problems it was run on and 44 of 492 OEIS conjectures, at a cost of a few hundred dollars per problem. The Erdős results in the public repository are #12 (parts i and ii), #125 (a variant with positive lower density), #138 (a variant), #152, #26 (a variant), #741 (parts i and ii) and #846. The paper also reports results found in collaboration with mathematicians. The individual Erdős problems also have their own entries on this site, taken from Tao's wiki.
How it was checked
Every proof compiles in Lean 4, and the build instructions are public. The natural-language proofs in the paper were written by people from the Lean proofs.
Limitations
Several Erdős results are variants or parts of the problems, not necessarily the problems as posed. Lean proves only the formal statement, so a mistranslated statement would go unnoticed; Josep Curto (UOC) made this point and also raised "methodological inconsistencies". Whether some of the problems were genuinely open has been disputed. The success rate was low, about 2.5% of Erdős problems attempted.
∎