Deterministic ingestion pipeline for SorryDB-compatible snapshots and benchmark indexes.

Benchmark harness for Lean sorry tactic proposals, with split policy, scoring, and verification protocols.

History-mined benchmark harness for reproducible tinygrad contribution tasks.

Algebraic, round-trippable representations of Lean proof-state tactics.

WASM-first egui component library for dashboard-grade research visualization.

Offline training and reranking over exported Wonton Soup run traces.

Lean-native extractor for deterministic theorem-item JSONL used in Wonton Soup corpus workflows.

Typst template suite for Specter field manuals and public papers, with shared tokens and reproducible build routing.

Implementation for reworking CATWD 2.0 semantics and calibrating K across domains to better understand its properties.

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.

Canonical SPECTER design language specification and multi-target token generation.