A city made
of invariants.

Explore the atlas, research districts, interactive instruments and connected architecture.

Inspect compiler-accepted Lean and Coq results, exact matrix witnesses and the remaining hardware and Mathlib proof gates.

Run and inspect the public spectral experiments, simulations, validators and scientific instruments.

Review the formal proof sources, GitHub Actions receipts, machine-readable evidence packets and active proof branches.