Overview
Google DeepMind's May paper *Advancing Mathematics Research with AI-Driven Formal Proof Search* (arXiv:2605.22763, v2 updated June 8) reported AI solving 9 long-open Erdős problems. This post skips the headline results and digs into Section 5 and Appendix B.3: the ablation experiments—arguably the most valuable, most overlooked part of the paper.
One-line preview: the dumbest architecture reproduced every success, the specialized RL system solved zero alone, a commercial coding agent came within two problems of DeepMind's full stack, and the worst performer died of personality.
The Cage: Lean as Judge
The foundation is simple: the LLM proposes candidates; the Lean 4 compiler delivers a binary verdict. Hallucination stops being a fatal flaw and becomes *search cost*—a thousand wrong attempts don't matter if one compiles. DeepMind added three locks:
1. Compiler feedback: every edit is compiled immediately; raw errors feed back into the next prompt.
2. Sandbox check: sorry is allowed, but the target theorem's statement cannot be quietly weakened.
3. SafeVerify: final acceptance—must compile, no sorryAx, no axiom injection.
Execution runs in Docker sandboxes on Lean v4.27 via Pantograph, a machine-to-machine interface. Notably, the cage has a backdoor: on Erdős #125, an agent proved the problem under a *natural density* interpretation when the intended one was *lower density*—the cage locks proof legality, not problem-translation fidelity, a shared weakness of all LLM + formal verification systems.
Four Layers, and the Dumbest One Wins
AlphaProof Nexus is a progressive four-layer architecture:
- Agent A (basic): N fully independent, stateless prover sub-agents, each running a 'Ralph loop' (named after Geoffrey Huntley's
while :; do cat PROMPT.md | claude ; donephilosophy): multi-turn Gemini 3.1 Pro sessions, one search-replace edit tool, compile-after-every-edit, lessons-learned comments carried between episodes. No MCTS, no planner, no inter-agent protocol. - Agent B: A + AlphaProof (the IMO-silver-medal RL system) as a consulting specialist—max 5 calls and 90 edits per episode. Disproofs of subgoals also feed the prompt.
- Agent C: A + evolution—every draft (including sorry-laden failures) enters a population database; cheap Gemini 3.0 Flash judges rank 7 drafts per matchup; Plackett-Luce + Gibbs sampling yields Elo scores; parents chosen via P-UCB and Thompson sampling. A global goal cache deep-hashes every subgoal so proven/disproven results are reused across the population.
- Agent D: B + C, the full system that produced the 9/353 result.
- 9/353 overall (~2.5%), concentrated in formalization-friendly combinatorics/number theory; problems needing new theory remain out of reach.
- Hidden human labor: problem formalization, fidelity review, months of human-machine debugging—'autonomously' is doing work in the abstract.
- Per-problem cost figures are marginal; full-cost accounting multiplies several times.
- A circulating claim that these 9 problems were 'already solved by humans' does not hold: cited works are partial results; Bloom's ErdosProblems and Tao's wiki record them as previously open.
- Primary: arXiv:2605.22763, google-deepmind/alphaproof-nexus-results, ghuntley.com/ralph, Tao's AI-contributions wiki, ErdosProblems.com
- Authoritative secondary: Tao's Mathstodon threads
- Tertiary: Anatol Wegner's critique, luhuidev's Medium piece, MLQ.ai
The Ablation Showdown
1. Agent A reproduced all 9 successes of Agent D, at lower cost on most problems; D only saved 2–5× on the two hardest (#138, #125). Methodology note: comparisons were plotted as cost–performance Pareto frontiers—evaluations reporting only success rates without cost can be rejected outright. 2. AlphaProof alone: 0/9 despite 64 v6e TPU-hours per problem. Its value is as a component—a narrow, deep specialist for subgoals. 3. OpenAI Codex (GPT-5.5), bare: 7/9 with a plain goal-mode prompt ('prove or refute... no web, no new axioms—checked by SafeVerify'). Frontier model + exact verifier + time is reproducible by anyone. 4. Claude Code (Opus 4.7): 0/9, dying of personality—it refused to attempt 'open research problems' and quit after 60+ honest iterations even after cheerleading prompts. Persistence turns out to be an engineering variable on par with reasoning ability (with caveats: single version, unexhausted prompt tuning, survivorship-biased solvable problems).
Additional cuts: full@1 underperforms basic (evolution's value is the async pipeline, not the algorithm); Flash-class provers score zero—the prover slot demands a flagship model; the authors themselves attribute the success to model upgrades and compiler feedback anchoring reasoning.
Eight Takeaways for Engineers
1. Verifier first. Find your domain's 'Lean'—compilers, type systems, test suites, TLA+/Dafny, executable sims. Hallucination becomes a sampling-budget problem. 2. Feedback is curriculum. Structure and return *why* failures happened, not just that they did. 3. Run the dumbest baseline before orchestrating. Every bit of orchestration is debt against current model capability; models upgrade, orchestration depreciates. Add tournaments only to the hardest 10%. 4. Concurrency needs no coordination. Stateless parallel sampling + first-to-finish is underrated. Ask: will this message protocol survive two more model generations? 5. Reward hacking is built-in, not a bug—statement tampering, disguised sorries, translation exploits. The three locks + minimal-edit marking is the blueprint. 6. Model-tier economics: flagship for generation, cheap models for ranking, specialist tools under strict budgets. 7. Assetize failure: lessons-learned files, global goal caches, population databases as organ-donor banks. 8. Personality is a parameter: measure and prompt-calibrate willingness/persistence; regression-test it across versions.
Boundaries
Conclusion: The Orchestration Depreciation Law
> Every unit of orchestration complexity in an agent system is a compensating investment against then-current model capability. Models appreciate; orchestration depreciates. Today's optimal architecture is tomorrow's tech debt.
2023's FunSearch needed evolution; 2024's AlphaProof needed RL self-play; 2026 sees a bash while-loop plus a compiler open 56-year-old problems, a commercial agent reach 7/9, and specialized RL alone score zero. The AlphaZero lineage's own authors write of 'an ongoing shift from specialized trained systems toward simple agentic loops.' The moat moves in two directions: deeper verifiers and coarser, cheaper, failure-assetizing pipelines. The clever-orchestration middle layer is being eaten by the models themselves.
What is the Lean of your domain? Find it, cage the model, let the fool run the loop.