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 access to that landscape.
A lesion atlas for proof search
Wonton Soup turns theorem proving into an intervention assay. First solve a theorem. Then damage the path or the distributed scheduler. The result is not just pass or fail: the same formal goal can replicate, reroute, collapse, or occasionally improve when a bad habit is blocked.
- intros control path opens the theorem directly
- subst then substitutes variables
- rw rewrites with mul_div_cancel_right
- hash control proof term has 435 nodes
block_intros
solved by a different proof family: hash b160eca8, GED norm 0.800, proof term 427 nodes
A same-family control lesion: the proof endpoint and structure remain stable.
Same theorem, new proof family, shorter trajectory.
The rewrite resource is load-bearing in the control basin.
The run still moves through search space, but never reaches proof.
Paper snapshot
The preprint pins a fixed analysis cohort. Those numbers are the headline claim: baseline-solved interventions preserve reachability often enough, and many recoveries are structurally different proofs.
Repo-local lake
The local lake is broader than the paper snapshot. It is useful for the live showcase because it reveals the shape of the measurement system: runs, intervention rows, graph rows, proof resources, basin seeds, and reference K scores.
The page should read like an instrument, not a report appendix.
Manifest-backed corpus selection fixes theorem identity, ordering, seed, and budget.
Centralized MCTS records the baseline path, tree, graph, goals, tactics, and proof term.
Path lesions block tactics. Scheduler lesions block, delay, or reroute controller work.
Hash families, graph edit distance, trajectory drift, and solve status separate outcomes.
Run artifacts become DuckDB tables for cross-run aggregation and dashboard export.
Replicates, reroutes, collapses, and rescues become evidence about proof dependence.
Resilience
A lesioned run still solves. This is the minimum evidence for flexible goal pursuit under damage.
Reroute
A solved lesion lands in a different proof family or shows nonzero graph distance. This is where the signal becomes structural.
Rescue
The baseline fails but the damaged run solves. These are not ordinary recoveries; they are search regularization cases.
A tactic block is a scalpel.
The most frequent local-lake interventions show why a single solve-rate number is not enough. Low recovery marks dependency. High GED marks structural movement. Together they distinguish redundant scaffolding from real chokepoints.
ReProver solves the fixed arithmetic theorem when linarith is available.
The same panel collapses when the arithmetic compression channel is removed.
2,441
tactic dependency rows
226
simp used-rule rows
167
linarith fact rows
37
linarith certificate rows
This is why the showcase can be more than prose.
The page is backed by normalized surfaces, not a pile of screenshots. The important schema names are stable enough to explain directly: runs, theorem_intervention, theorem_intervention_comparison, theorem_variant_metrics, basin_runs, basin_seed, k_reference_score, graph_nodes, graph_edges, and proof_term_const_edges.
| Provider | Runs | Completed | Lean research |
|---|---|---|---|
| reprover | 347 | 347 | 158 |
| deepseek | 252 | 251 | 154 |
| heuristic | 208 | 207 | 93 |
| coq | 18 | 18 | 0 |
| bfs | 8 | 8 | 3 |
| z3 | 6 | 6 | 0 |
Seed reruns reveal proof attractors, not just solve rates.
The basin tables rerun the same theorem across seeds and record which proof-structure hash each solved seed falls into. In the 64-seed coq_pair_andb_prop run, only 26 seeds solve, and those 26 successes split into 21 distinct structures. The largest attractor has only three seeds. That is a shattered basin: reachable, but not organized around one proof form.
50 seeds, 39 solved, 5 structures. The top attractors hold 16, 14, and 7 seeds.
50 seeds, 17 solved, 14 structures. Blind solve rate is slightly higher at 36%.
50 seeds, 20 solved, 5 structures. One attractor holds 14 of the solved seeds.
50 seeds, one structure, K 2.764. A single attractor with a large guided advantage.
Scheduler lesions matter because coordination is part of the system.
Distributed MCTS is not just faster centralized MCTS. It creates a controller surface: agents reserve frontier nodes, virtual loss pushes them apart, and one Lean REPL serializes expansion. Blocking or delaying controller actions changes theorem outcomes.
The theorem is an endpoint, not the object.
The object is the fiber of histories and proof structures that can realize that endpoint.
Damage turns tactics into questions.
If a block recovers, the removed resource was substitutable. If it collapses, that resource carried the basin.
Rescue is the surprise.
Some constraints improve search by pruning bad branches. That makes lesions instruments, not just sabotage.
- Preprint PDF is the fixed manuscript snapshot for the headline results.
- Dashboard is the inspection surface for theorem traces and run payloads.
- Cabinet docs map the lake, artifact contracts, distributed MCTS semantics, and runbooks.
- dossiers/wonton-soup/artifacts/lake/lake.duckdb is the local evidence lake used for the live inventory and intervention bars on this page.