Same proof family. The blocked edge lay off the path the prover actually used, so the rerun produces a search graph identical to the wild type. not_or_and under block_exact closes both runs.
Wonton Soup
Intervention framework for proof-search structure: centralized MCTS maps proof families, basin stability, and search efficiency, while distributed MCTS tests how collective control changes which proof families the search can reach.
Tactic lesions on a distributed MCTS theorem prover
Solve a theorem with distributed MCTS, then block a specific tactic family and rerun under matched seed and budget. The search graph either reaches the goal the same way it did before, finds a structurally different proof, fails to close at all, or closes faster than the wild type. The lake holds 25,798 such reruns across 340 distributed runs and three providers.
Four outcomes of a matched-budget tactic block
Same goal, structurally different proof. The lesion cuts the wild path and the prover finds an alternative through a different branch. AEMeasurable.sum_measure under block_exact closes via a different family.
The blocked tactic carried the only viable closing edge. The lesioned tree truncates before reaching the goal. hf_..._11756 under block_linarith drops from 16/16 wild-type solves to 0/16.
The blocked tactic was a learned habit that sent the prover on a tour. Without it the search closes in a small fraction of the iterations. hf_..._19703 under block_obtain drops 204 iterations and closes.
Matched-budget tactic and scheduler lesions on a distributed MCTS prover produce intervention-defined proto-cognitive signatures in the sense of Levin's TAME program. Same goal pursued by variable means is the James criterion, measured here in 25,798 intervention comparisons across 340 distributed runs.
Reroutes are structural and cheap; the gradient from redundant scaffolding to irreplaceable chokepoint comes out continuous. The naive prediction that wider basins should predict resilience fails in the same data at r = −0.18, which sets up the next question rather than answering it.
Under perturbation, some theorem-runs preserve goal reachability by rerouting through structurally distinct proof families, while others reveal compressed infrastructure whose removal disconnects the empirically accessible basin.
Lesion rows5,161across 340 distributed MCTS runs and three tactic providers.
Reroute survival34.0%1,754 of 5,161 lesioned rows preserve goal reachability through a different proof family.
Structural drift58%of solved-strict rows show non-zero normalized search-graph edit distance. The reroutes are real structure rather than measurement noise.
Naive basin hypothesisr = −0.18unique-structure count vs lesion recovery. Wider basins recover from lesions less often.
Recovery rate by tactic, redundant to load-bearingA continuous gradient. The same lesion protocol that fully recovers when
block_push_neg is removed almost never recovers when block_dsimp is removed.A single irreplaceable tactic erases every solveOne ReProver theorem under matched budget. Blocking
linarith turns every wild-type seed from a solve into a failure.Some lesions speed search up, not down~3% of lesions accelerate search (785 of 25,798 rows). Blocking a tactic that anchors a habitual commitment frees the prover's budget for the goal.
Preprint figures
The three figures that carry the argument in "Proto-Cognitive Signatures in Distributed MCTS Theorem Proving": provider-split outcome counts, the GED distribution that shows reroutes are structural, and the basin-vs-recovery scatter that produces the negative correlation.
Fig 17 · Provider splitsLesion outcomes · 340 runs
Right panel: strict main-text denominator restricted to baseline_solved = true rows whose matched control_null rerun also solves. Left panel: rows excluded from that denominator, split into rescue cases and null-unstable spillover. Three providers (ReProver, DeepSeek, heuristic) reach the same qualitative picture; DeepSeek is the noisy denominator (72.0% null-solve vs 99.9% for ReProver, 100% heuristic).
Read this as The provider asymmetry is what forces the strict denominator; DeepSeek's null instability is why the headline is 34% rather than smaller.
Fig 16 · GED bimodality1,250 solved strict rows
Normalized search-graph edit distance across solved strict-denominator rows. Of 1,250 rows, 602 (48%) are explicit reroutes by the hash-mismatch criterion; 730 (58%) show non-zero structural drift. Mean = 0.405, max = 1.091.
Read this as The distribution has real mass away from zero, so structural divergence is the norm when goal reachability survives a lesion.
Fig 18 · Basin width vs recoveryThe surprise · negative result
Wider basins recover from lesions less often. Higher unique-structure counts do not imply higher lesion recovery. Correlation r = −0.18. The highest-width quartile (3 to 9 unique structures) recovers at 25.8%, lower than Q1 (37.5%), Q2 (36.5%), and Q3 (47.2%).
Read this as Raw variant count does not predict recovery; what might is whether variants cross independent resource channels.
Search structure · MCTS treeFrom the companion blog
The centralized MCTS over Lean goal signatures with AND/OR branching: each node is one obligation, OR-branches are tactic choices, AND-sets are subgoals all required. Distributed MCTS shares this frontier across controllers and exposes a second intervention surface (scheduler lesions) on top of the same tree.
Read this as Centralized MCTS maps the structural landscape; distributed MCTS adds scheduler-level interventions on top of the same tree.
Pipeline
Pipeline schematic · data contracts between stageswonton.py lean run -m distributed
corpus selectionwild-type discoverymatched interventiondistributed orchestrationmetricslake
Search graph, proof graph, and trace graph are kept as distinct surfaces gated by run-capability flags. Lean provides search and proof; Coq adds the proof-term DAG; ATP backends (E, Vampire, Z3) provide trace only.
Lake9.9 GB37 tables, 340 distributed runs, 25,798 intervention comparisons, 17,400 wild rows, 4,640 search graphs.
Corpus5,068Lean theorems: Mathlib, miniF2F, ProverBench, registry. Coq SerAPI and TPTP backends extend the surface.
Active providers3ReProver 347 runs, DeepSeek 253, heuristic 208. BFS, InternLM-step, Coq, Z3 are present but small-n.
Proof-term DAG2.48MConstant nodes and 881K constant edges, queryable per theorem.
Per-tactic recovery rate
Block one tactic family, measure how often the system still solves the same theorem under matched budget. Headline percentages use the strict denominator (matched-control rows where the null rerun also solves); the marginal column shows the lake's raw aggregate across all 25,798 block_x rows.
Trajectory divergence under lesion · solved vs failedn = 25,798 · lake
Cut sensitivity for a single tactic
For the theorem hf_deepseek_prover_v1_train_11756, blocking linarith doesn't slow the prover down. It severs the basin entirely. Across the lake the proof-term DAG for this theorem records 128 linarith input facts, 96 preprocessed facts, and 32 certificates; the cut is not abstract.
Wild type · ReProver16 / 16
Every seed solves. The proof family uses linarith at the arithmetic-closing step; the surrounding tactics carry the structure.
block linarith →
Lesion · ReProver0 / 16
Total collapse. DeepSeek confirms cross-provider with 6/7 → 0/7. The arithmetic chokepoint is not provider-specific.
A second case shows the chokepoint is provider-relative. For list_append_nil, blocking cases collapses ReProver but the heuristic provider routes around it. The chokepoint is a property of the learned policy rather than the theorem.
ReProver / block cases0 / 16
Down from 16/16 wild type. ReProver leans on the case split; no alternative fires.
vs
Heuristic / block cases16 / 16
Heuristic routes through induction. Same goal, fully substitutable. The chokepoint sits in the policy rather than the math.
Basin width does not predict resilience
Rerun the same theorem 64 times with reshuffled seeds and the attractor structure comes out. coq_pair_andb_prop distributes across seven structural buckets, with one dominant attractor. Across the corpus, wider basins recover from lesions less often.
coq_pair_andb_prop · 64 seeds
7 buckets
01
02
03
04
05
06
07
08
09
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
Basin width vs lesion recoveryr = −0.18
Wider basins recover from lesions less often
Top-quartile theorems sit between 21 and 28 unique basin structures and recover from lesions less often than narrower-basin theorems. The candidate refinement is to count variants that cross independent resource channels rather than variants that reuse the same infrastructure.
Within-tree convergence is rare
Across 4,640 search graphs, only about 1% (68) show within-tree goal convergence. The structural variation surfaces across reshuffled seeds rather than inside a single MCTS rollout.
Rescue cases
4,508 lesioned rows solve under matched budget when the wild-type solve is also matched. The largest instance, hf_deepseek_prover_v1_train_19703 under block_obtain, closes 204 iterations sooner than the wild type. Blocking a tactic that anchors a habitual subgoal frees the budget for the actual goal.
Paired trace · hf_deepseek_prover_v1_train_19703 · wild-type vs block_obtainGED 1.00 · iter diff −204
Rescue inventory · lake aggregate4,508 solved-strict reruns · top sources
Two patterns share the column. Dense rescues like block_norm_num1 at 49% mean the wild-type provider over-uses a tactic that was rarely the cleanest closer for those goals. Big-volume rescues like block_intros at 546 are the population effect: a tactic that appears everywhere also acts as a habit everywhere, and habit costs budget when the goal would have closed faster without it.
Distributed MCTS and scheduler lesions
Shared-frontier topology · controllers, AND/OR tree, scheduler-lesion injection pointsorchestrator/lean.py
Scheduler lesions act above the tree. Block fraction f is the share of dispatch decisions the scheduler is forced to reject, so the controller has to find another goal to claim. Recovery falls modestly with f; the centralized AND/OR search is doing most of the load-bearing work. The provider split tells the same story from another angle: a noisier policy like DeepSeek generates more rescues because it has more removable habits.
Collapse is runaway expansion
Collapsed runs average 6.7 iterations and 1.7 backtracks with 2.9 unique goals visited against 3.0, 0.1, and 2.1 for solved runs, so the collapses are expanding blindly rather than exhausting the search.
K is net-negative
Across 1,905 K-scored rows the mean of log10(τ_blind / τ_agent) is −0.04 with sd 0.20, so the prover does not beat blind on average and the signal is in how K spreads across theorems rather than in the mean.
Where K is positive
add_add_neg_cancel'_right and add_sub_sub_cancel sit at K = +0.41 and +0.39 respectively: 2 prover iterations against ~5 blind.
Proof-term monodromy
Each solve also produces the proof object itself, a typed term that type-checks against the theorem's statement, and we hash that closing term on every wild-type solve to ask, per theorem, how many distinct terms the prover actually landed on. The measurement that means something holds everything fixed except the seed: same provider, same corpus, reruns only, and one theorem in six still closes on a structurally different term, so the proof is not canonical even when nothing outside the search has moved. The fraction rises to 72% across two providers and 95% across three or more, but those columns count smaller and harder subsets, 452 and 43 theorems against 975, and a second provider is a second model with its own coding habits, so they bound how wide the fiber can open rather than measure anything about diversity.
Proof-term fiber width per theorem · wild-type solves, Lean backendfraction with 2+ distinct closing terms
Whole-proof hashes, not per-goal yet
The fractions above use theorem_wild.proof_term_hash, the whole-proof hash recorded per wild-type solve. The column is 88% populated across 7,068 Lean solves, enough to call fiber width per theorem. The missing piece is per-goal monodromy: completed_proof_term_hash on the goal table, the hash of the subterm that closes each goal node along the search path. The assembly hook at prover/assembly.py is wired but currently passes None on most goal records.
What the lake says
Same goal, variable means
Among solved-strict rows, 48% are explicit reroutes by the hash criterion, 58% show non-zero structural drift, and mean GED is 0.405. The theorem is fixed and the proof family varies; the cost of that variation is invisible in the trajectory.
The block is syntactic, the response is structural
The prover is not told it was perturbed. block_dsimp stops the search at 2% recovery; block_push_neg leaves it at 100%. The same kind of edit lands very different anatomies underneath.
Partition basins by resource channel
The prediction that wider basins survive lesions better gets r = −0.18. The candidate refinement is whether basin variants cross independent resource channels rather than re-using the same infrastructure. The next dataset is a basin partition by axiom and lemma usage.
What would change the reading
- Reroutes collapse to noise around a single trajectory under tighter controls.
- Scheduler lesions produce no theorem-level effects at any block fraction.
- Cut sensitivities vanish when budgets absorb them.
- A basin partition by independent channels does no better than raw width.
Dashboard
The dashboard ships the published lake as parquet, executes queries client-side in the browser, and lets you scrub through wild-type and intervention runs side by side. Four views, each tied to a paper claim.
Open the dashboard
Vite + DuckDB-WASM. Filter pinned to backend = 'lean' in the published preset. The dashboard pulls parquet exports from the lake at build time; no server is involved at runtime.
liveDuckDB-WASMparquetKaTeXclient-only
Hero / paired player
Side-by-side wild vs intervention MCTS tree with a scrubber, theorem and intervention selectors, blocked-tactic badge, and KaTeX-rendered goal panels.
Explorer
Run / theorem / intervention drilldown. Same data plane as the figures above, with arbitrary filters.
Proof graph
Render the proof-graph (Coq) or trace-graph (ATP) for any solved row. Respects the search/proof/trace gating from the ADRs.
Rescue matrix
Theorem × intervention heatmap of rescued / collapsed / unchanged / no-data. The 256 block_intros rescues are the row to look at.
Reproducing locally
Run a distributed sweep
uv run python wonton.py lean run -m distributed --sample 32 --seed 0
Writes logs/<run-id>/ with per-theorem exploration history, MCTS tree, search graph, goal cache, proof-term (when present), and assembly trace. Run capabilities are flagged at write time and travel with the run.
Postprocess and reconcile
uv run python wonton.py postprocess
uv run python wonton.py lake reconcile
Builds GED matrices, K-metric rows, attractor counts, and trajectory metrics; reconciles them into the DuckDB lake under artifacts/lake/lake.duckdb.
Rebuild the figures
uv run python paper/build_figures.py
Renders fig16-ged-bimodality.svg, fig17-followup-provider-splits.svg, fig18-followup-basins.svg directly from the lake. The dashboard view payloads share the same query layer.
Compile the preprint
typst compile --root ../.. paper/main.typ paper/artifacts/main.pdf \
--font-path ../../addenda/typst-field-manual/assets/fonts
Typst 0.14.2 against the vendored IBM Plex bundle in the field manual. Source-of-truth is main.typ; the PDF is rebuilt from it.
Sources
- Preprint PDF — "Proto-Cognitive Signatures in Distributed MCTS Theorem Proving", Ludwig P. (Specter Labs), April 2026. The full TAME-framed argument with the three figures embedded above and appendices A/B/C on cohorts, lesion taxonomy, and rescue cases.
- Live dashboard — DuckDB-WASM, four views (paired player, explorer, proof graph, rescue matrix). The fastest way to verify any specific claim on the page against the lake.
- Companion blog post — longer-form prose treatment with the K-metric framing, the two-gate validity protocol, and an inline vignette-stepper for three lesion specimens (contrapositive, nat_succ_pred, iff_intro).
- Follow-up blog — the paired panel is three-way not bimodal; provider differences are real; constraint generates competency. Smaller pieces that didn't make the main paper.
- Cabinet documentation — lake schema, artifact contracts, distributed MCTS semantics, ADRs (checkpoint goal IDs, search-graph feasibility by backend, lake reference selection, ProofGraphIR for cross-assistant alignment), runbooks.
- Source repository —
wonton.pyCLI root with prover, atp, orchestrator, experiments, and analysis modules.docs/concepts/carries the lexicon (search vs proof vs trace graph, attractor metrics, distributed MCTS, tactic-action IR, UCB1, K-metric);docs/contracts/is the per-stage input and output contract;docs/adrs/records the design decisions that the lake schema reflects.