Framing article for the dossier: proof-space morphology under interventions, with centralized MCTS as the structural baseline and distributed MCTS as the coordination layer.
Proof search in Lean as a structured problem space: centralized MCTS maps proof families and basin structure, while distributed MCTS tests how coordination changes access to that landscape.
- Read the dossier framing article.
- Use the Wonton Soup docs map for concepts, schemas, and runbooks.
- Open the dashboard to map the structural landscape from centralized runs, then compare distributed runs to test coordination effects on that same theorem slice.
-
March 1, 2026Cabinet docs rebuilt with updated Wonton Soup references and stable doc IDs.
-
February 6, 2026Dashboard manifest defaulted to run
corpus-2026-02-06-003808with 522 theorems. -
February 3-12, 2026Follow-up analysis window logged with 355 run entries and intervention taxonomy pressure tests.
Docs, ADRs, and runbooks for the dossier.
Inspect theorem-level traces and run metrics across the structural baseline and the distributed coordination layer.
Source code, CLI entry points, and test harnesses.
- Dashboard manifest (run selection and metadata).
- Active payloads live under the dashboard data directory and are selected by the manifest rather than a hardcoded run id.