Blog
Notes, talks, and dispatches from the community.
Jun 27, 2026
Prismriver
A formalization of music theory and algorithmic composition in Lean 4 that makes the rules of music machine-checkable and opens the door to verifiable composition. Joint work with Leni Aniva.
Jun 25, 2026
Numina Fuse
An agent-native autoformalization platform, built on LeanExplore, that lets you turn an AI agent loose on your Lean projects from the browser — blueprints, parallel subagents, and long-running auto mode.
Jun 6, 2026
Formalizing the GNS Construction in Lean
Building a Hilbert space and a *-homomorphism from a C*-algebra — an essential step toward the Gelfand–Naimark theorem, now merged into Mathlib.