k-semantics-reference
Playground for re-implementing Cognition All The Way Down 2.0 semantics and calibrating K on small domains before wider use.
Addenda Index
Addenda are side-projects that might not fit our research programme, but were interesting or valuable enough to pick up.
All Addenda
lean-corpus-extractor
Lean-native extractor for deterministic theorem item JSONL used by Wonton Soup corpus workflows.
lean-mcts-learning
Offline training and reranking experiments over exported Wonton Soup run traces.
lean-sorry-dataset
Deterministic ingestion pipeline for SorryDB-compatible snapshots and benchmark index materialization.
lean-sorry-repos-benchmark
Benchmark harness for Lean `sorry` tactic proposals with split policy, scoring, and verification protocols.
lean-tactic-representation
Research planning track for 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 thread for LLM contribution quality on tinygrad and related codebases.
typst-field-manual
Typst field-manual template and workflow for doc ID allocation plus reproducible PDF output routing.