Wonton Soup
MCTS search over Lean tactic proofs: an intervention harness for proof structures and basins, and a study of distributed MCTS as a search algorithm in its own right.
We solve a theorem with Monte Carlo tree search, then block a tactic it used or stall the scheduler, and run it again. The same goal can come back through a different proof, take a longer route, fail, or solve faster once a wasteful step is gone.
From the paper
When the baseline solved a theorem, a lesion still reaches a proof often enough, and many of those recoveries are different proofs.
Resilience
A lesioned run still solves. The minimum sign of goal-directed recovery.
Reroute
The lesion solves but lands in a different proof family or shows graph distance. The change is structural.
Rescue
The baseline fails but the damaged run solves. The block removed a path that was leading search astray.
ReProver solves the theorem when linarith is available.
Block linarith and it collapses completely.
The theorem is an endpoint, not the object.
The object is the fiber of histories and proof structures that can realize that endpoint.
A block tests whether a tactic was necessary.
If a block recovers, the removed resource was substitutable. If it collapses, that resource carried the basin.
Some damage makes search better.
Some constraints prune bad branches, so a lesion can sharpen the search instead of breaking it.
- Preprint PDF has the frozen numbers from the paper.
- Visual showcase walks through every result.
- Dashboard opens individual theorem traces and run data.
- Cabinet docs explain the lake and how to rerun things.