k-semantics-reference
Implementation for reworking CATWD 2.0 semantics and calibrating K across domains to better understand its properties.
Addenda Index
Projects outside the lab's primary dossiers, kept as part of the public record.
All Addenda
lean-corpus-extractor
Lean-native extractor for deterministic theorem-item JSONL used in Wonton Soup corpus workflows.
lean-mcts-learning
Offline training and reranking over exported Wonton Soup run traces.
lean-sorry-dataset
Deterministic ingestion pipeline for SorryDB-compatible snapshots and benchmark indexes.
lean-sorry-repos-benchmark
Benchmark harness for Lean `sorry` tactic proposals, with split policy, scoring, and verification protocols.
lean-tactic-representation
Algebraic, round-trippable representations of Lean proof-state tactics.
specter-viz
WASM-first `egui` component library for dashboard-grade research visualization.
tinygrad-benchmarks
Reproducible benchmark design for LLM contribution quality on tinygrad and related codebases.
typst-field-manual
Typst template suite for Specter field manuals and public papers, with shared tokens and reproducible build routing.