Agentic Loops Overtake Bespoke Systems

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• AutoGraphForge: Towards Automated Graph Theory Discovery
• OEIS Open: How many conjectures can language models turn into theorems?
• On the Navier–Stokes Millennium Prize Problem
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science

Summary#

The headline empirical finding of DeepMind's AI-Driven Formal Proof Search paper, and its clearest cross-domain confirmation of The Bitter Lesson: a basic agent — independent prover subagents each running a simple "Ralph loop" of generate-edit-compile episodes — solved all 9 of the Erdős problems that the elaborate full-featured agent (evolutionary search + the bespoke AlphaProof RL prover) solved, only at higher cost on the hardest ones. The paper's conclusion: "an ongoing shift from specialized trained systems toward simple agentic loops as LLMs become more capable."

The surprise, in the authors' words#

The team chose the full-featured agent (D) for the large-scale exploration based on its strong competition-benchmark performance — at planning time, "simpler agentic loops did not show strong performance." Then a post-hoc analysis on the 9 solved Erdős problems found:

"Remarkably, the basic agent solved all 9 problems, though at a higher cost on the harder problems."

They attribute this to two things: (1) the LLM landscape "shifted substantially" between planning and analysis (model capability jumped), and (2) "the power of compiler feedback in grounding LLM reasoning" — the simple loop works because Lean's verifier keeps each step honest.

Why this is the bitter lesson in a new field#

The Bitter Lesson: scaled general methods beat hand-engineered structure over time. Here the "hand-engineered structure" is the bespoke apparatus — the AlphaProof RL theorem-prover (a specialized trained system) and the evolutionary population/Elo machinery (Evolutionary Proof Search). The "scaled general method" is a frontier LLM in a plain loop with a verifier. As the LLM improved, the bespoke scaffolding's advantage collapsed to a cost difference, not a capability difference on most problems. This is the exact dynamic Harness Shrinkage as Models Improve describes — scaffolding that compensates for model weakness becomes drag as the model strengthens — observed in formal mathematics rather than in coding harnesses.

The residual advantage (and its expiry date)#

The bespoke agent isn't useless — it "retains an advantage on the hardest problems for now," with 2×–5× cost savings on the two toughest Erdős problems (#125, #138). But the authors explicitly date the advantage: "as LLM capabilities grow, this advantage may diminish." The pattern is a receding frontier where bespoke systems matter: the harder the problem and the weaker the model, the more the specialized structure pays off — and that region shrinks every model release. (Standalone AlphaProof tree-search and smaller-model basic agents solved nothing — so the loop still needs a strong-enough model + a verifier; see Scale-Dependent Prompt Sensitivity.)

The counter-measurement (2026-09-21) — and what survives it#

ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving (UVA + Meta AI, arXiv 2608.26334, empirical) is the first source in this corpus to run the bespoke-vs-loop comparison as a controlled benchmark sweep rather than a post-hoc look at problems the bespoke system had already solved. Same base model in every arm (Claude Opus 4.8, weights frozen), same Lean 4 + Mathlib environment, matched per-target budget, mean of three runs, all baselines reproduced by the authors. The result is the opposite sign:

Arm	Putnam	IMO-Lean	Combi	Avg
Claude Opus 4.8, pass@16 sampling	0.0	0.0	10.0	3.3
ReAct (the plain loop), Opus 4.8	35.0	15.0	27.0	25.7
Hilbert (recursive decompose + repair)	55.5	33.3	49.0	45.9
LEAP (AND-OR proof DAG, within-target)	64.7	36.7	50.0	50.5
ProofEvolve (evolution + persistent schema library)	71.2	53.3	49.0	57.8

Every added piece of bespoke structure buys solve rate, monotonically, with the model and the budget held constant. The plain loop is 32 points behind the most elaborate system, and the unscaffolded model solves literally nothing on two of the three benchmarks.

How this reconciles with the 9/9 Erdős result, rather than simply beating it. Both sources are empirical and neither is stale, so the job is to find the axis they differ on — and it is budget, not verifier quality (both are Lean) and not model strength (both use a 2026 frontier model).

• DeepMind's finding is a capability claim at generous budget: on nine problems the full-featured agent had already solved, the basic agent also got there — "though at a higher cost on the harder problems," 2×–5× on Erdős #125 and #138. Cost was the whole residual. Nobody capped it.
• ProofEvolve's finding is a budget-efficiency claim at a tight cap: its 1× profile allows 12 model calls, 60 Lean calls, 400K tokens and 1,800 seconds per target, and every arm gets the same. Under a hard cap, the thing DeepMind measured as "higher cost" stops being a cost and becomes a failure.
• The populations differ too. DeepMind's nine were solvable research problems; ProofEvolve's are three whole competition benchmarks scored including everything nobody solves.

So the reconciled claim is narrower than this page originally stated, and more useful: a simple loop with a sound verifier converges to the bespoke system's results when you let it spend, and falls tens of points short when you don't. Scaffolding in a verified domain buys sample efficiency, which reads as "no capability advantage" exactly when budget is free. The receding-frontier framing survives; what changes is that the frontier recedes along the budget axis, not only along the model-capability axis, and a tight budget pushes it right back out.

The bespoke agent's advantage has "collapsed to a cost difference, not a capability difference" on most problems (qualified 2026-09-21 by ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving: true at uncapped budget, false at matched budget — where the same difference is 32 points of solve rate. The original wording is DeepMind's own and is kept because it is accurate about their experiment.)

Two further details worth carrying. ProofEvolve's structure is also not a trained system — every weight is frozen and the accumulated knowledge lives in an explicit Lean-checked library — so it is not the thing The Bitter Lesson predicts will be outrun; it is scaffolding that stores its learning in text a human can read. And the gap is domain-uneven: ProofEvolve's lead over LEAP is +16.6 points on IMO-Lean (proofs assembled from several lemmas) and −1.0 on CombiBench (proofs resting on one explicit construction). Where a problem does not decompose, the elaborate search stops paying — which is the same shape as the original finding, one level down.

The same shape one level down: brute table beats six searchers (2026-09)#

A small, heavily-hedged third data point, from search rather than from agents. AutoGraphForge: Towards Automated Graph Theory Discovery (Pastorek, arXiv 2609.03478, empirical) runs the refutation half of a mathematical discovery loop — hunting counterexamples to machine-generated graph conjectures — with six sophisticated backends available: an SMT encoding, variable-neighbourhood search, linear cross-entropy, MCTS, simulated annealing, and a deep-RL edge-selection policy. Against them stands the dumbest possible alternative: look the conjecture up in a precomputed table of 348,207 graphs with their invariants.

The table won, by roughly two orders of magnitude. In the single-pass baseline, 1,243 of 1,249 refutations came from the static datasets and random models; six came from the active searchers. Across the five-partition HPC run the whole battery contributed 1–22 counterexamples per round against 500–790 from the datasets. The one-time cost of precomputing the table (0.85 of the run's 1.22 CPU-years) dwarfs the loop itself — which is the bitter-lesson shape exactly: pay for scale once, and general lookup outruns hand-designed search.

Three reasons this is a data point and not evidence. It is a single run with the searchers at un-tuned default hyperparameters, and the author says so and declines to generalize. It is not an agentic loop — no LLM is in the refutation path at all, so it speaks to The Bitter Lesson rather than to harness design. And the comparison is not budget-matched in the sense this page's other numbers are: the table's cost was paid up front and is excluded from the per-round accounting, which is precisely the unlimited-spend assumption the ProofEvolve reconciliation above warns about. Carried here because it is the corpus's only instance of the pattern in a non-agentic search, and because it fails in the same direction as the 9/9 Erdős result and for the same reason ProofEvolve qualifies it. See Automated Conjecturing.

The noisy-verifier case, finally measured — and it comes back split (2026-09-21)#

Both data points above run against the Lean kernel. Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science (Google Research + CMU, arXiv 2609.15983, empirical) is the first source in this corpus to run an elaborate bespoke harness in a domain where the verifier is a council of LLMs: Stellar Colosseum writes natural-language research proofs, and its falsifiers, section reviewers and global verifier are all model instances. See Many-Agent Proof Harnesses for the architecture.

Its TCS-Bench baseline column is the interesting part, because it cuts both ways at once:

Arm (TCS-Bench, 300 FOCS/STOC/SODA theorem tasks)	Accuracy
Gemini 3.1 Pro, direct single call	30.3%
Gemini 3.1 DeepThink, direct (model-side parallel thinking)	52.0%
Colosseum (the bespoke harness) on Gemini 3.1 Pro	54.0%
GPT-5.6 Pro (max), direct single call	68.0%
Colosseum two-run cross-model selection	71.0%

• For bespoke structure: against an unscaffolded call on the same frozen model, the harness is worth +23.7 points. Structure is capability, not cost saving — the same sign ProofEvolve found in Lean. So the noisy verifier does not destroy the value of scaffolding.
• Against bespoke structure, on the harness-shrinkage axis: a thinking toggle on the same model family (DeepThink, 52.0%) comes within two points of the entire 27-page architecture, and a stronger model's plain single call (GPT-5.6 Pro max, 68.0%) beats the whole harness by 14 points. Only the two-run cross-model pipeline edges past it, by 3.0 points — and the grader is a model validated at ">90% accuracy," so that 3.0-point margin is ~9 problems inside a ~30-problem error bar. This is Harness Shrinkage as Models Improve appearing inside the paper's own baseline table.

What it does not settle, and the reason the open question below stays open: Colosseum is never compared to a plain agentic loop. Every comparator is a direct call — no ReAct arm, no best-of-N at matched budget, no token or dollar figure published anywhere in the paper. The authors name the gap themselves ("compute-matched evaluation would be needed to distinguish improved allocation from simply using more inference"). So the noisy-verifier domain now has a bespoke-vs-nothing measurement, not the bespoke-vs-loop measurement this page's question asks for.

The largest bespoke apparatus in the corpus, and it reports no comparison at all (2026-09)#

Each measurement above compares something to something else. The 2026-09-08 OpenAI announcement (The Navier–Stokes AI Claim, On the Navier–Stokes Millennium Prize Problem, vendor-claim) is worth recording here precisely because it does not, and because it is the extreme point of the apparatus axis this page tracks.

What OpenAI describes is bespoke by every criterion on this page: ~10,000 concurrent agents in communicating groups of varied size; different problem variants assigned to different groups (A/B for a proof, C/D for a disproof, run simultaneously); a mid-run model swap when a further-trained checkpoint became available; Codex used to cross-pollinate insights between groups, with OpenAI stating that the group which found the solution "was guided in such a way"; a human decision to shift resources off the other Millennium problems after an Euler result landed; and a Lean verification pass at the end, attributed to GPT‑6 Astra, 17 hours. Budget disclosed: 88 hours, 2.7 million inter-agent messages, ~130 billion output tokens on this problem.

And no baseline of any kind. No single-agent arm, no plain-loop arm, no smaller-group arm on the same problem, no ablation — the nearest adjacent configuration in the post is a different problem (~100 agents, ~50 hours, unforced Euler). The post makes no efficiency or architecture claim and does not present itself as a comparison, so this is not a vendor failing to report a control; it is a capability announcement being read here for what it cannot settle. Three consequences for this page:

• It does not bear on "loops overtake bespoke systems" in either direction. An uncontrolled result from the most elaborate apparatus ever built tells you nothing about what a simpler one would have done — the same gap the compute-controlled-benchmarking argument records from the budget side, and one OpenAI's own multi-agent lead concedes is unaffordable to close (Noam Brown: "we haven't done that experiment yet").
• It is the corpus's clearest case of the perfect-verifier setting with no loop arm — Lean is at the end of the pipeline, and there is still no comparator. The ProofEvolve reconciliation above turns on budget; here the budget is published and there is nothing to compare it against.
• The one structural detail worth generalizing is the guidance path: the winning group was steered by a separate model consolidating other groups' intermediate results. That is hand-engineered cross-population information flow, i.e. more scaffold, not less — the opposite direction from the minimal-scaffold multi-agent design the same lab describes elsewhere in the corpus, and it is asserted rather than measured.

The re-counter-measurement, on the bespoke system's own item set (OEIS Open, 2026-08)#

The section above relocated this page's claim to "loops beat bespoke once budget is unconstrained," because ProofEvolve's matched-tight-budget sweep came out 32 points the other way. OEIS Open: How many conjectures can language models turn into theorems? (OEIS OPEN, Tom Adamczewski, Epoch AI, arXiv 2608.11941, 2026-08-12, empirical) is the third measurement, and it is the one with the best claim to being the decisive comparison — because it runs a plain loop against the bespoke system on the bespoke system's own benchmark, with a hard budget cap, and with the bespoke system's own cost figures obtained from its authors.

The setup. 492 open OEIS conjectures formalized in Lean — the item set AlphaProof Nexus built and reported 44/492 (9%) on. Epoch's agent is as small as an agent gets: a ReAct tool loop on Inspect with three tools (bash, a text editor, and a resources tool reporting remaining budget), a container with Lean+Mathlib, SageMath and Python, a $50 per-conjecture spending cap, and nothing else. No evolution, no population, no Elo, no specialized prover.

System	Resolved of 492	Avg cost per resolved conjecture
Claude Opus 4.8, three-tool ReAct loop	147 (30%)	$10 (max $47)
GPT-5.5, same loop	26% (count not reported)	$6
Gemini 3.5 Flash, same loop	22% (count not reported)	$9
AlphaProof Nexus (evolution + Elo raters + AlphaProof tool)	44 (9%)	~$10 avg, up to ~$50 for the hardest few

The cost column is why this counts. ProofEvolve's reconciliation above turned on budget: the loop converges when it can spend and falls short when it cannot. Here the loop wins 3.3× and spends the same per solve, on a set where the bespoke system had home advantage. The paper's own reading is The Bitter Lesson verbatim: "rather than prescribing how the model should work through problem-specific structure, it may be better to give a model simple tools and let it choose how to use them."

The confound, which the paper states and this page must carry. The two arms do not share a model. AlphaProof Nexus's prover subagents run Gemini 3.1 Pro (released 19 February 2026); GPT-5.5 and Claude Opus 4.8 were released about two and three months later (23 April and 28 May). So the honest form of the 3.3× is not "a loop beats bespoke structure at matched budget" — it is "a loop on a model two generations newer beats bespoke structure at matched budget," which is this page's harness-shrinkage claim rather than its loops-beat-bespoke claim, and the two have been conflated here before. The comparison nobody has run remains the same one: the bespoke apparatus re-run on the newer model.

The matched-model ablation, which is the cleaner datum#

Buried in Appendix A.2 is the experiment the confound above rules out — same model, same verifier, same $200 cap, same 100-conjecture LITE subset, varying only the harness. The DeepAgent arm swaps the ReAct loop for Inspect's deepagent: subagent delegation, persistent memory, a todo-list tool, and a longer, opinionated system prompt. The literature arm hands the base loop an offline snapshot of 476,000 pure-mathematics arXiv papers.

Model	base loop	DeepAgent	+ literature
Claude Opus 4.8	39%	39%	39%
GPT-5.5	36%	41%	37%
Gemini 3.5 Flash	29%	29%	28%

"Agent variants had no effect." Opus is identical to the point across all three arms; GPT-5.5's +5 sits inside overlapping error bars at n=100 and is not reproduced. This is the matched-model, matched-budget, sound-verifier structure ablation, and its answer is zero — which is the shape this page originally claimed and ProofEvolve appeared to overturn.

So the three measurements split by what kind of structure is added, not by budget alone. ProofEvolve's structure is search — an AND-OR proof DAG with fitness read off the kernel and a persistent library of verified sub-proofs, i.e. machinery that changes how the search allocates its calls. DeepAgent's structure is agentic affordance — memory, subagents, todos, a better prompt, i.e. machinery that changes how the model organizes itself. Under a cap, the first buys 32 points and the second buys nothing. The sharpened rule: in a domain with a sound per-step verifier, spend engineering on the search, not on the agent.

The search-machinery side re-measured, and this time it is Pareto (2026-08)#

The split this page settled on above — search machinery pays under a cap, agentic affordance does not — gets a third measurement on the machinery side, and it is the cleanest of the three. Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing (Vamshi and Yang, University of Maryland, arXiv 2608.28639, empirical) runs a three-role MCTS — generator, decomposer, critic, all the same frozen 7–8B checkpoint — against flat whole-proof sampling at an exactly matched proof-attempt budget (N×K×S, nothing terminating early on success), on three provers and four benchmarks, five seeds. Detail on AI-Driven Formal Proof Search; three things belong here.

It wins at every budget, and the margin does not shrink. MiniF2F with Goedel-Prover-V2-8B: 84.2% against 82.4% at 32 attempts, 87.1% against 84.7% at 256. PutnamBench: 26/659 against 18/659 at 32. Same sign on all three models. Against the ProofEvolve reconciliation above, that is a second independent matched-budget win for bespoke search structure inside Lean.

The full matched-budget grid (moved from AI-Driven Formal Proof Search, 2026-09-29): total attempts are exactly N × K × S with N = 4 MCTS iterations and K = 4 children fixed and S varied (PAB@32 to PAB@256); every arm (whole-proof sampling, two ablated search baselines, the Prover Agent reproduction and the method) runs the same checkpoints, prompt template, decoding config and pinned environment, nothing terminates early on success, and results are mean ± sd over 5 seeds. MiniF2F, Goedel-Prover-V2-8B: 84.2 ± 0.5% at PAB@32 against 82.4 ± 0.6%, rising monotonically to 87.1 ± 0.2% at PAB@256 against 84.7 ± 0.1%; DeepSeek 77.1 → 82.6 against 75.2 → 78.2; Kimina 64.3 → 66.9 against 62.8 → 65.1. PutnamBench (audited, Goedel): 26/659 against 18/659 at PAB@32 and 36/659 against 22/659 at PAB@128. Physics at PAB@16: +1.9 to +2.4 points on PhysLeandata and +1.5 to +2.0 on LeanPhysBench with the PhysLib library as context, and the method without PhysLib approaches whole-proof sampling with it, so structured search partly substitutes for missing domain-library context. The largest single architectural term the paper isolates is the decomposer's temperature decay (τ_d annealed in depth and iteration from τ₀ = 0.7): removing it costs 1.8–2.5 points on every model.

And it costs less, which no previous datum on this page does. Every structure result here has been a quality-for-compute trade with the compute axis argued about. This one is 32.8% fewer total inference tokens and 35.8% fewer output tokens at the identical attempt budget, because the decomposer and critic calls are tiny (1,024 and 3 max output tokens) and a generator conditioned on an explicit decomposition writes shorter proofs (the 32.84% is averaged over the three models against whole-proof sampling's cumulative usage for one benchmark run at the same PAB; decomposer and critic calls add ~7k tokens per model and generator output falls ~114k). Structure that is better and cheaper is outside the frame this page has been arguing in, and the mechanism is worth naming: the structure is not buying more search, it is buying shorter generations, by telling the generator what to prove.

The caveat is the identity of the loser. Whole-proof sampling is not an agentic loop — it is best-of-N with no feedback of any kind, so beating it is not the comparison this page is about. The paper's one genuine loop arm is its reproduction of Prover Agent, which does the thing this page's original finding turns on: put the compiler's error text in the next turn's context. At a comparable budget (260 against PAB@256) Prover Agent reaches 86.2 ± 0.1% on MiniF2F against the MCTS framework's 87.1 ± 0.2%. Nine tenths of a point. So the honest reading of this source on this page's axis is the narrow one: elaborate search beats flat sampling decisively and beats a compiler-feedback loop barely, on one benchmark, in a reproduction run by the party that wins it, with every arm at 7–8B.

Where it sits on the loop-versus-bespoke axis: on the machinery side but at its cheap end. There is no trained component anywhere — no value network, no RL, no fine-tuning; three prompt templates and a UCB formula around a frozen checkpoint. The paper deliberately excludes comparators that retrain the prover (BFS-Prover, HunyuanProver) on the grounds that a changed checkpoint conflates search gains with model gains. That exclusion is the discipline this page has repeatedly asked for, applied by an author to his own advantage-seeking, and it places this squarely in ProofEvolve's category rather than AlphaProof's: structure without a specialized trained system, which is the half of "bespoke" the bitter lesson has the least grip on.

A fidelity-graded task where the bare loop comes last (ProofLoom, 2026-09)#

ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization (empirical) runs seven systems on one model and one 48-hour cap over 15 formalizations of stochastic-optimization algorithms and grades source faithfulness, not only a kernel pass. The bare Codex loop and its Goals variant score 2.8 and 3.0 out of 7 human rating; the role-structured harnesses (OpenGauss, LeanMarathon, Trellis, Archon, ProofLoom) score 3.5 to 6.3 on textbook tasks. That points the opposite way from this page's headline, and the page's own verifier clause explains it: loops win where a cheap reliable verifier exists, and here the target includes "is this the source's theorem", which a compiler does not provide, so a loop without a reviewer has no signal on it (and, per Kernel-Level Proof Auditing, drifts the statement). The caveats are the usual ones: the authors ran every baseline on their own adapters, tokens are unreported for the baselines, and nothing here is a model-generation trend, so it does not test the "expiry date" argument above.

Generalization#

The transferable claim: when a domain has a cheap, reliable verifier, prefer the simplest agentic loop that can exploit it, and re-evaluate bespoke scaffolding every model release — it tends to convert from capability-enabling to merely cost-saving, then to drag. The verifier (The Verifiability Thesis) is what makes the simple loop viable; the loop is what makes the system cheap to build and maintain. Bespoke systems earn their keep only at the receding hard frontier.

With the budget clause attached (2026-09-21): …prefer the simplest loop if the marginal call is cheap enough that you never have to cap it. The moment a per-task budget binds — a latency SLO, a token cap, a paid API, a verifier call that costs seconds of CPU — the ordering flips, and the measured flip in Lean is 32 points. "Cost-saving, not capability-enabling" is only a downgrade under an implicit assumption of unlimited spend; the same structure that saves cost is capability under a cap. This is the formal-math statement of Large-Scale Test-Time Compute's core point — that asking how capable a system is without naming its budget is ill-posed — applied to harness design rather than to model evaluation.

Connections#

• AI-Driven Formal Proof Search — the setting; this is its central architectural finding
• The Bitter Lesson — the principle this empirically confirms in formal mathematics
• Harness Shrinkage as Models Improve — the same "scaffolding becomes drag as models improve" dynamic, here for a proof-search harness
• Harness Build-vs-Buy — the same don't-build-bespoke conclusion by an independent route: not capability erosion but maintenance economics, where a fork loses 866 upstream bug fixes a year even if it never loses a capability
• Agent Loop Pattern — the "Ralph loop" basic agent is an instance of the loop-as-primitive
• Evolutionary Proof Search — the bespoke scaffolding (population + Elo) the simple loop matched; also now the home of ProofEvolve's kernel-grounded variant, the system that beats the plain loop by 32 points once budget is capped
• Many-Agent Proof Harnesses — the noisy-verifier branch of the same comparison: a bespoke many-agent harness graded by a model council rather than a kernel, worth +23.7 points over a bare call on the same model and 14 points behind a stronger model's bare call
• The Navier–Stokes AI Claim — the apparatus axis at its extreme and the comparison axis at zero: ~10,000 agents, per-group problem variants, a mid-run model swap, Codex-mediated cross-pollination and a Lean pass, with no baseline of any kind and a vendor-claim tier
• Automated Conjecturing — the non-agentic instance of the same shape: a precomputed 348,207-graph lookup table out-refutes six stochastic and neural search backends by two orders of magnitude
• OEIS Open Benchmark — this page's closest thing to a decisive comparison and its cleanest null: a three-tool ReAct loop resolves 147/492 against AlphaProof Nexus's 44/492 on the bespoke system's own item set at matched cost per solve (confounded by a two-generation model gap), while a same-model, same-budget DeepAgent arm — subagents, persistent memory, todo list — moves the score by zero
• Kernel-Level Proof Auditing — the same source's second half, and a prerequisite for reading any comparison on this page: when the harness reports "compiled, no sorry" rather than asking the kernel what the declaration depends on, 31–44% of one prover's PutnamBench successes are not proofs — and a search procedure produces more of them than flat sampling does, without introducing the exploit
• AlphaProof Nexus — the framework spanning basic (A) → full-featured (D) agents
• The Verifiability Thesis — the verifier is what lets the simple loop work at all
• Client-Side Agent Optimization — "match capability at lower cost" is the cost/quality optimization AgentOpt formalizes; here the cheap config wins
• Scale-Dependent Prompt Sensitivity — the loop needs a strong-enough model: smaller Gemini variants solved nothing
• Recursive Self-Improvement — this is RSI's clearest existing-domain proxy: a simple loop matched a bespoke trained system as the model improved, the dynamic that, run on AI development itself, closes the loop
• AI Accelerating AI Development — the same simple-loop-overtakes-bespoke pattern, observed in Anthropic's internal AI-R&D throughput rather than in formal math
• Tree Search over Agent Trajectories (LATS) — the reward-oracle MCTS whose matched-budget grid is carried above, read as tree search: a value function whose second term is a compiler accept-count, with free reversibility and the allocation sweep that shows the gain is backpropagation, not call budget

Derived#

• Single General Agent vs. Multi-Agent Coding Architecture — the 9/9 Erdős result is the corpus's cleanest evidence that a single simple loop overtakes a bespoke multi-component system as models improve, one half of the answer to whether single beats multi-agent (the other half: context/evaluative separation persists)

Open Questions#

• The bespoke advantage is dated "for now." What's the next model generation's verdict — does the evolutionary/AlphaProof apparatus survive on any problems, or fully collapse to a cost line? Partially answered 2026-09-21, by analogy rather than directly — Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science does not test the evolutionary/AlphaProof apparatus or run in Lean, so it cannot close this. What it does supply is the first instance of the predicted collapse happening within a single paper's own baseline column, one model generation on: a 27-page bespoke many-agent harness reaches 54.0% on research-level TCS proofs with Gemini 3.1 Pro, a model-side thinking mode on the same family reaches 52.0% with no harness at all, and a stronger model's plain single call (GPT-5.6 Pro max) reaches 68.0% — 14 points above the harness. The mechanism is the one predicted here, with a twist worth recording: the capability was absorbed not by a better loop but by test-time compute moving inside the model, which is a route this page did not anticipate. Three reasons it stays #oq/wait: different apparatus, different verifier (model council, not a kernel), and the comparison is cross-vendor rather than the same system re-run on a newer model. The trigger event is unchanged — the AlphaProof/evolutionary system re-run on a next-generation LLM against the same nine Erdős problems. Extended 2026-09-21 by On the Navier–Stokes Millennium Prize Problem, and the extension is a warning rather than a datum. The next model generation arrived, and what the lab holding it built around it was more apparatus, not less: 10,000 concurrent agents in communicating groups, per-group problem variants, a mid-run model swap, a separate model consolidating insights across groups, and a Lean pass at the end. So the first observation of frontier-model-plus-bespoke-apparatus at the new generation points the opposite way from this question's expectation — though it cannot be scored, because the announcement reports no baseline, no ablation and no comparison of any kind, and it is vendor-claim about an unreleased model. Two readings stay live and this source separates them: the apparatus may still be buying capability at the frontier, or it may be the cheapest way to spend a weekend's compute when nobody is measuring efficiency. The trigger event is unchanged, and this adds a second one worth watching — any lab publishing a same-problem comparison between its many-agent apparatus and a single long-running agent on the newest model. Partially answered 2026-09-23 by OEIS Open: How many conjectures can language models turn into theorems?, from the other side of the comparison. Nobody re-ran the apparatus on a newer model; instead a third party ran a three-tool loop on newer models against the apparatus's own 492-conjecture OEIS item set at a $50 cap, and the apparatus's 44/492 became the bar in someone else's figure at 147/492 — a 3.3× gap at matched average cost per resolved conjecture ($10 either way, from the apparatus authors' own correspondence). Read against this question that is the collapse it anticipates, one generation on and on 492 items rather than nine. It stays #oq/wait because the apparatus itself was never re-run: Gemini 3.1 Pro against Opus 4.8 and GPT-5.5 is a two-to-three-month model gap, so the result cannot separate "the apparatus stopped paying" from "the newer model would have made the apparatus better too." The trigger event is unchanged.
• Does the "simple loop + verifier beats bespoke system" result hold only where the verifier is perfect (Lean), or also in noisy-verifier domains (tests, LLM-judge councils)? Partially answered 2026-09-21 — and the answer arrived from an unexpected direction. ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving says nothing about noisy verifiers; everything in it runs against the Lean kernel. What it does is falsify the question's premise inside the perfect-verifier case: run the comparison at matched, tight per-target budget with the base model frozen and a plain ReAct loop scores 25.7% average against 57.8% for the bespoke evolutionary system, with the intermediate systems ordered monotonically between them. So the result does not even hold unconditionally where the verifier is perfect — it holds where the verifier is perfect and budget is effectively uncapped. The noisy-verifier half is still open, and is now a sharper ask: a budget-matched loop-vs-bespoke sweep in a domain whose verifier is a test suite or a judge council, which would separate "structure buys sample efficiency" from "structure buys robustness to a lying verifier." Extended the same day by Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science, which supplies the noisy-verifier domain and still not the loop arm. Stellar Colosseum is a bespoke many-agent harness whose entire correctness signal is model-generated — adversarial falsifiers, per-section reviewers and a global verifier, with no formal check anywhere in its mathematics arm — so the "perfect verifier" premise is finally removed. Result: against an unscaffolded single call on the same frozen model, the elaborate structure is worth +23.7 points (30.3% → 54.0% on 300 research-level FOCS/STOC/SODA theorem tasks). So a noisy verifier does not by itself destroy the value of bespoke structure; the ProofEvolve direction holds outside Lean. Two things keep this partial and keep the tag at #oq/source. First, the loop arm is missing entirely — every comparator in the paper is a direct model call, there is no ReAct-style loop, no best-of-N control, and the paper publishes no token count, call count, wall-clock or dollar figure at all, so the budget axis the reconciliation above turns on cannot even be located. The authors concede it in future work: compute-matched evaluation "would be needed to distinguish improved allocation from simply using more inference." Second, in the other direction the same table shows a stronger model's plain single call (68.0%) beating the whole harness (54.0%), which is a harness-shrinkage datum rather than a loop-beats-bespoke datum and does not substitute for one. The ask is now precise: run a plain loop and the bespoke harness at a stated, matched call budget on the same model with a judge-council verifier. A third source arrives 2026-09-21 with the missing budget and the same missing arm (On the Navier–Stokes Millennium Prize Problem, vendor-claim): a ~10,000-agent apparatus over 88 hours, 2.7 million inter-agent messages and ~130 billion output tokens, ending in a Lean verification — so the verifier is back to perfect and the budget is published in full, and there is still no loop arm, no single-agent arm and no ablation. Worth recording because it makes the pattern a property of the field rather than of one paper: across three sources in one month, two verifier regimes and two labs, nobody has run the comparator, and the one party asked about it directly says the experiment has not been done. Partially answered 2026-09-23 — somebody ran a comparator, in the perfect-verifier regime, and it came out null. OEIS Open: How many conjectures can language models turn into theorems? runs base ReAct against Inspect's deepagent (subagent delegation, persistent memory, a todo-list tool, a longer system prompt) on the same model, the same 100-conjecture LITE subset, the same Lean/SafeVerify gate and the same $200 cap: 39/39, 36/41, 29/29 across Claude Opus 4.8, GPT-5.5 and Gemini 3.5 Flash. A 476,000-paper arXiv literature arm is equally flat (39/37/28). So bespoke agentic affordance buys nothing at matched budget with a sound verifier, which is the opposite sign from ProofEvolve's bespoke search machinery at matched budget — and the distinction between the two kinds of structure is the useful thing this adds. Two reasons it stays #oq/source: the verifier is still perfect, so the noisy-verifier half of the question is untouched; and the arms are matched on dollars rather than on calls or tokens, so a DeepAgent arm that spends its $200 on subagent overhead rather than on proof attempts is not distinguishable from one whose affordances simply do not help.

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving — arXiv 2608.26334, UVA + Meta AI, 2026-08-26, empirical. Table 1 was re-read from pdftotext -layout and matched against the §5.2 prose before the table above was written. Caveat that belongs on every number in it: all five agentic baselines (ReAct, Aristotle, AxProver, Hilbert, LEAP) are the ProofEvolve authors' own reproductions — "retains its search strategy, and runs under a matched budget" — not numbers reported by their original authors. A reproduction that under-tunes a competitor inflates the gap, and there is no third-party replication
• AutoGraphForge: Towards Automated Graph Theory Discovery — arXiv 2609.03478, Ján Pastorek (Comenius University in Bratislava), 2026-09-03, 17pp, ITAT 2026 submission, empirical. Cited here only for the dataset-versus-active-search attribution in §4.1, quoted from prose. Single author, workshop track, one run, searcher hyperparameters explicitly not optimised — the weakest evidence on this page, and hedged in place. Full source treatment on Automated Conjecturing
• On the Navier–Stokes Millennium Prize Problem — OpenAI (no byline), openai.com, 2026-09-08 with a 2026-09-10 update, ~1,900 words, vendor-claim. Cited here only for the apparatus description (group structure, per-group problem variants, the mid-run model update, the Codex cross-pollination and the guided winning group) and the published budget. It contains no comparison, so nothing in it is a measurement for this page's purpose — it is recorded as the extreme point of the apparatus axis and as evidence that the control is not being run anywhere. First-party about an unreleased model, disputed on priority, unverified. Full treatment on The Navier–Stokes AI Claim
• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science — arXiv 2609.15983, Lin, Woodruff, Deng, Mao, Zuo & Mirrokni (Google Research; Woodruff also CMU), v2 2026-09-15, 27pp, empirical. Cited here only for Table 2's baseline and Colosseum rows, reconciled against pdftotext -layout before use, plus the §8.1 compute-matching concession quoted from prose. Carry three caveats with every number: the grader is itself a model (reference-assisted, ">90% accuracy" on 100 expert labels, no agreement statistic), so the 3.0-point margin over GPT-5.6 Pro is inside its error bar; the paper reports no call count, token count, wall-clock or cost, so nothing in it can be placed on the budget axis this page's reconciliation depends on; and it is a first-party Google evaluation of Gemini in which three of the six authors also wrote the benchmark. Full source treatment on Many-Agent Proof Harnesses
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), "OEIS Open: How many conjectures can language models turn into theorems?", arXiv 2608.11941, 2026-08-12, 27pp, empirical. Cited here for the 147/492-versus-44/492 comparison and its cost columns, the model-release dates that confound it (the paper's own footnote 10), and the Appendix A.2 agent-variant ablation. The 3.3× headline is not a matched-model comparison and this page must not quote it as one; the matched-model datum is the DeepAgent/literature null. Every figure above is from prose, a figure caption or a figure image (Figures 1 and 3, viewed); the paper's single table is reconciled against pdftotext -layout and cited nowhere here. Full treatment on OEIS Open Benchmark
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing — Vamshi & Yang (University of Maryland), arXiv 2608.28639, 2026-08-11, 14pp, empirical. Cited here for the matched-PAB comparison against whole-proof sampling, the Prover Agent reproduction at budget 260, the token-efficiency figures and the paper's stated reason for excluding retrained comparators. Every baseline is the authors' own reproduction, including the Prover Agent arm they beat by 0.9 points — the same caveat this page already carries for ProofEvolve. All three provers are 7–8B open-weight checkpoints, so nothing here transfers to frontier-scale models. Full treatment on AI-Driven Formal Proof Search and Kernel-Level Proof Auditing
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — Wang, Li & Yuan, arXiv 2609.34960, 2026-09-28, empirical. Cited for the seven-system human-rating comparison only; full treatment on Many-Agent Proof Harnesses.