Wonton Soup Docs

Canonical documentation map for dossiers/wonton-soup.

Mode Framing

wonton-soup is an intervention framework for studying proof-search structure. Centralized MCTS establishes the structural landscape: proof families, basin stability, recovery after lesion, and blind-relative efficiency (K). Distributed MCTS tests how collective control changes access to that landscape through multiple local controllers, coordination pressure, and scheduler lesions over a shared frontier.

The research stack is sequential. Centralized runs map the morphology and measure K as a single-controller baseline, comparable to the single-agent examples in Chis-Ciure and Levin (2025). Distributed runs then ask whether collective search creates efficiency that individual search does not access, and whether K decomposes across agents following the framework’s compositionality property.

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
• Verification and representative command coverage: Verification Matrix
• Inspect run outputs with jq workflows: 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)
• Paper workflow runbook: Paper Workflow Runbook
• Follow-up run matrix and execution script: Follow-Up Run Program (March 2026)