DeepMind: AlphaProof Nexus Does Research-Level Math

Not to be out-Erdős'd, DeepMind released AlphaProof Nexus: Gemini 3.1 Pro paired with the Lean proof assistant, so every step is formally verified. Its strongest agent autonomously resolved 9 of 353 open Erdős problems (two open for 56 years) and proved 44 of 492 open OEIS conjectures, at a few hundred dollars per problem, with all proofs on GitHub for audit. Lean doesn't accept vibes, which neatly sidesteps the autonomy fight. Two Erdős-flavored AI results in one month; the man's problem lists are becoming a benchmark suite.

Sources: paper, The Decoder