Wonton Soup docs
Wonton Soup runs Monte Carlo tree search (MCTS) over proofs, perturbs the search, and measures what survives. Centralized runs map which proof families the search finds, how stable its basins are, how it reroutes or collapses, and how much faster it is than blind search (K). Distributed runs test whether coordinated controllers change access to the same landscape.
Start here
- Analysis lexicon: the terms used across the analysis and reports.
- Analysis metrics reference: what each metric family measures.
- Log file schemas: what a run writes, and which graphs each proof backend can produce.
Measures
- Attractor metrics for proof search: basins of attraction in proof search, and when their size means something.
- UCB1 and blind-uniform search: how centralized search picks nodes and orders tactics, and the blind-uniform baseline.
Run artifacts
- Analysis artifacts reference
- Log schemas: run level
- Log schemas: per-theorem artifacts
- Distributed MCTS trace event dictionary
Search machinery
- Distributed MCTS: scheduling and control in distributed runs.
- Goal identity, deduplication, and preview/commit
- ProofGraphIR: the proof graph shared across proof assistants.
- TacticActionIR: a typed summary of what each proof step did.
- Partial proof terms, assembly tracking, and sequential replay
- Tactic provider options for tactic suggestion
- DeepSeek provider settings