Wonton Soup Docs
Canonical documentation map for dossiers/wonton-soup.
Mode Framing
wonton-soup uses one proof-space model with two control regimes. Centralized MCTS is the structural baseline for proof-space morphology: use it to map proof families, basin structure, recovery, and blind-relative efficiency. Distributed MCTS is the collective-control layer over that same proof-space morphology: use it to test how multiple local controllers, scheduler lesions, and coordination pressure change access to the landscape established by the centralized baseline.
Concepts
- Analysis terminology index: Analysis Lexicon
- Metric-family definitions: Analysis Metrics Reference
- Attractor/basin metrics deep dive: Attractor Metrics for Proof Search
- Distributed MCTS scheduling and control semantics: Distributed MCTS Semantics
- Goal identity, deduplication, and preview/commit: Goal Identity, Deduplication, and Preview/Commit
- Cross-assistant proof graph abstraction: ProofGraphIR
- UCB1 behavior and tuning in this repo: UCB1 and Blind-Uniform Search in Wonton-Soup
Contracts
- Artifact definitions: Analysis Artifacts Reference
- Log schema index: Log File Schemas
- Run-level schema details: Log Schemas: Run-Level
- Per-theorem schema details: Log Schemas: Per-Theorem Artifacts
- Backend artifact-family mapping: Log Schemas: Backend Artifact Mapping
- Distributed MCTS trace event dictionary: Distributed MCTS Trace Event Dictionary
- Partial proof-term extraction + sequential replay: Partial Proof-Terms and Sequential Replay
- Provider options and selection rubric: Tactic Provider Options for Tactic Suggestion
- DeepSeek runtime settings and reproducibility notes: DeepSeek Provider Settings
Decisions
- ADR index: ADR Index
Operations
- Setup Lean + REPL environment: Lean REPL Setup
- Build/validate/sweep corpus artifacts: Corpus Pipeline
- Inspect run outputs with
jqworkflows: Log Query Cookbook - Paired Lean↔︎Coq primary gate: Cross-Assistant Paired Benchmark (Primary Gate)
- Unpaired alignment diagnostic: Cross-Assistant Alignment (Diagnostic)
- Cross-run lake reconcile/export/sync: Run Lake (Cross-Run DuckDB)
- Lake jobs and reference selection: Lake Jobs (Materialized Datasets)
- Follow-up run matrix and execution script: Follow-Up Run Program (March 2026)