Design Tokens A-011
Canonical SPECTER design language specification and multi-target token generation.
Addenda
Projects outside the lab's primary dossiers, kept as part of the public record.
equational-theories-distillation A-010
Compact decision procedure for equational implication over magmas, distilled from the 4694-law implication graph into a sub-10KB offline cheatsheet for SAIR's Stage 1 benchmark.
k-semantics-reference A-009
Implementation for reworking CATWD 2.0 semantics and calibrating K across domains to better understand its properties.
lean-corpus-extractor A-007
Lean-native extractor for deterministic theorem-item JSONL used in Wonton Soup corpus workflows.
lean-mcts-learning A-006
Offline training and reranking over exported Wonton Soup run traces.
lean-sorry-dataset A-001
Deterministic ingestion pipeline for SorryDB-compatible snapshots and benchmark indexes.
lean-sorry-repos-benchmark A-002
Benchmark harness for Lean `sorry` tactic proposals, with split policy, scoring, and verification protocols.
lean-tactic-representation A-004
Algebraic, round-trippable representations of Lean proof-state tactics.
specter-viz A-005
WASM-first `egui` component library for dashboard-grade research visualization.
tinygrad-benchmarks A-003
Reproducible benchmark design for LLM contribution quality on tinygrad and related codebases.
typst-field-manual A-008
Typst template suite for Specter field manuals and public papers, with shared tokens and reproducible build routing.