Specter Labs
A reaction–diffusion pattern, a gene network that counts its peaks, and the feedback between them form one controller. The diagram is the wiring the code exports through Catlab.
The comparison of wirings runs today. The later numerical sweep has not been reproduced yet, and the injury and repair experiments are still proposals.
Explore the controller →
The start, goal, legal moves, and cost unit stay fixed. A blind walk and a shortest-path policy take different routes through the same problem.
The paths are two seeded replays. K = log₁₀(τ_blind/τ_agent) comes from a separate exact calculation that caps each walk at 500 steps, so its value of 1.22, about 16.6 times less expected cost, is a lower bound for this grid.
Explore the executable comparison →We condensed the known implications among 4,694 equational laws into a short sheet a model can use offline. Small operation tables give explicit counterexamples when one law does not imply another, and rules keyed to the starting law prove some of the cases where it does.
The colors, type sizes and spacing used by this site, our papers and our emails, written once in TOML and generated into CSS, Typst and email styles.
Typst templates that typeset our papers and field manuals in the site’s fonts and colors.
Pulls theorems out of Lean libraries into the fixed, reproducible lists that Wonton Soup searches over.
Trains small models on Wonton Soup search logs to score proof states, rank tactics and suggest the next one.
Rust chart and panel components for our research dashboards, built with egui and compiled to WebAssembly for the browser.
A research plan and a small interpreter for writing Lean tactics as parts that combine and convert back without loss.
Coding tasks taken from merged tinygrad pull requests, each asking whether a model can write a patch that passes the check the original change passed.
Asks a model for the next tactic at an unfinished step of a real Lean proof and checks the answer with Lean.
Turns snapshots of SorryDB, a catalogue of unfinished proofs in public Lean projects, into a fixed benchmark index.