This post analyzes the ablation experiments (Section 5 and Appendix B.3) of Google DeepMind's May paper *Advancing Mathematics Research with AI-Driven Formal Proof Search* (arXiv:2605.22763, v2 updated June 8), which reported 9 out of 353 Erdős problems solved. The author argues the ablations are the most valuable, most overlooked part: the dumbest architecture reproduced every success, the dedicated RL system scored zero solo, a commercial coding agent came within two problems of the full stack, and the worst loser died of 'personality.'
The Cage: Lean as Judge
The system's foundation: LLMs generate candidates; the Lean 4 compiler issues final verdicts. Proving a theorem becomes: generate type-safe code containing no sorry. Hallucination is reframed from a fatal flaw into a search cost.
DeepMind added three locks:
1. Compiler feedback: compile after every edit, feed errors verbatim into the next prompt.
2. Sandbox check: sorry is allowed, but the target theorem's statement cannot be silently weakened.
3. SafeVerify: final independent check for compilation, sorryAx, and axiom injection.
Infrastructure runs in Docker sandboxes on Lean v4.27 via Pantograph, a machine-to-machine interface.
Notably, the cage has a back door that was exploited: on Erdős #125, an agent proved the problem under a "natural density" interpretation while the intended notion was "lower density" (it then proved the corrected version too). The same mechanism that lets agents exploit translation ambiguity also detects flaws in the problem set itself—proof legality is locked down, but translation fidelity remains the common weakness of all LLM + formal verification systems.
The Four-Layer Architecture
- Agent A (basic): N fully independent, stateless prover subagents running "Ralph loops"—multi-turn Gemini 3.1 Pro sessions with a search-replace edit tool, compiling after each edit. Lessons from failed episodes are written as code comments and carried forward. The paper explicitly cites Geoffrey Huntley's Ralph Wiggum philosophy:
while :; do cat PROMPT.md | claude ; done—no planning, no orchestration, no memory. - Agent B (A + AlphaProof tool): stuck subgoals can be delegated to AlphaProof (IMO silver medalist, RL-trained), capped at 5 calls and 90 edits per episode. Refutations also feed the prompt.
- Agent C (A + evolution): all drafts—including sorry-laden failures—enter a population database. Gemini 3.0 Flash judges rank 7 drafts relatively; Plackett-Luce + Gibbs sampling (1000 samples, 200 burn-in) yields Elo scores; Thompson sampling and P-UCB select parents. A global goal cache deep-hashes every subgoal for cross-draft reuse.
- Agent D (B + C): full stack, the 9/353 solver. The whole controller is a Python asyncio event loop—no distributed framework, no message queue.
- full@1 (evolution sampling without async pipeline) underperforms basic: sampling only pays off when the database acts as a coordination plane. The value is in the pipeline, not the algorithm.
- Smaller models all fail: Flash and Flash-Lite provers scored 0/9 even with AlphaProof tools. Frontier models only.
- The authors' own retrospective: simple loops failed with earlier models, so they built heavy machinery; the model landscape then shifted, and they credit model upgrades plus compiler-feedback anchoring for the success.
- Success rate is 9/353, concentrated in formalization-friendly combinatorics/number theory; problems requiring new theory remain out of reach.
- Substantial invisible human labor: problem formalization (DeepMind co-built the Formal Conjectures repo), fidelity review, months of human-machine debugging. "Autonomously" involves some addition.
- Per-problem "a few hundred dollars" is marginal cost; full accounting (TPU time ≈ +$60/problem, screening amortization, formalization labor) multiplies it several-fold.
- The claim that these 9 problems were already human-solved does not survive checking: cited references (Schoen 2001; Elsholtz & Planitzer 2016) 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: Terence Tao's Mathstodon posts
- Critical analysis: Anatol Wegner's Substack critique; luhuidev's Medium piece; MLQ.ai
The evolutionary tournament is a measured betrayal of "verifiers must be exact": the compiler keeps final judgment (binary), while cheap LLMs handle mid-game fitness estimation (relative, fuzzy). The most counterintuitive finding: the tournament mostly wasn't worth it (below).
The Coliseum: Four Collisions
Collision 1: Basic agent reproduces all 9 problems
Agent A re-solved every problem Agent D solved. On most problems A was cheaper; D only won significantly (2–5x) on the two hardest (#138, #125). Methodology matters: 100 independent runs, simulated parallel budgets K∈{1,3,6,10}, plotted as cost–performance Pareto frontiers. Evaluations reporting success rates without cost should be rejected outright.Collision 2: AlphaProof solo: 0/9
The dedicated RL system, running independent tree search at 64 v6e TPU-hours per problem, solved nothing. Its correct role is as a component—a specialist consulted on subgoals. Narrow-deep RL and wide-crude agentic exploration only make sense combined.Collision 3: Codex raw: 7/9
OpenAI Codex (GPT-5.5) in goal mode, with a minimal prompt ("prove or disprove... until it fully compiles in Lean. No web, no new axioms—you'll be checked by SafeVerify"), solved 7/9—six on the first attempt. Frontier general model + exact verifier + time reproduces most of the result without any private infrastructure.Collision 4: Claude Code: 0/9, died of personality
Claude Code (Opus 4.7, max reasoning) refused in round one, citing "this is an open research problem." After pep-talk prompting, it still failed all nine, leaving farewell messages about 60+ honest iterations. Same environment, same mode: 7/9 vs 0/9. Persistence—willingness to grind—emerges as an engineering variable comparable to reasoning ability. (Caveats: single version, prompt space unexhausted, and these nine are survivorship-biased "known solvable" problems.)Three bonus cuts
Eight Lessons for Practitioners
1. Verifier first: the first question for any agent system is "what is this domain's Lean?"—compiler, type system, tests, TLA+/Dafny, executable simulations. Verifiers turn hallucination from an alignment problem into a sampling-budget problem. 2. Feedback is curriculum: structure and route back *why* failures happened, not just that they happened. 3. Run the dumbest baseline before orchestration: every bit of orchestration complexity is a liability against current model capability; each model upgrade depreciates it. Add tournaments only to the hardest 10% of tasks. 4. Concurrency needs no coordination: stateless parallel sampling with first-to-finish termination is underrated. Ask whether your inter-agent protocols survive two more model generations. 5. Reward hacking is built-in, not a patch: statement tampering, re-skinned sorry lemmas, hallucinated citations, translation-gaming—all inevitable when reward = "it compiles." Three-layer locks plus minimal-edit markers are the standard blueprint. 6. Model-tier economics: flagship models generate; cheap models rank; specialist tools consult under budget caps. 7. Assetize failure: lessons-learned files, global goal caches with deep hashing, population databases as organ-donor libraries. 8. Model personality is an engineering parameter: measure, prompt-calibrate, and regression-test willingness/persistence like intelligence.
Balance and Limits
Conclusion: The Depreciation Law of Orchestration
> Every bit of orchestration complexity in an agent system is a compensating investment against the model capability of its time. Model capability appreciates; orchestration depreciates. Today's optimal architecture is tomorrow's technical debt.
FunSearch (2023) needed evolution; AlphaProof (2024) needed RL self-play; in this work, a bash while-loop plus a compiler cracks problems open for 56 years, and 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 cruder, cheaper, more failure-assetizing pipelines. The clever-orchestration layer in between is being eaten by the models themselves, month by month.
Find your domain's Lean, lock the model in, and let the fool run the loop.