Blog
Notes, talks, and dispatches from the community.
Aug 16, 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.
Aug 2, 2026
Crane
An extraction system from the Rocq Prover to modern C++, generating readable, functional-style output with disciplined ownership and no separate runtime, built to make verified developments credible candidates for production integration.
Jun 28, 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 7, 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.