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

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.

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

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

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

Offline training and reranking over exported Wonton Soup run traces.

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

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

Reproducible benchmark design for LLM contribution quality on tinygrad and related codebases.

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

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