Blog

Oct 18, 2026 Formal Learning Theory in Lean 4 Upcoming talk · Dhruv Gupta Pajor's inequality over infinite sets, its origins in Banach space geometry, and the foundational questions that make learning theory a natural target for Mathlib. Sep 6, 2026 Composing CRDTs Convergent by Construction Upcoming talk · Alexander Städing A Lean 4 framework for assembling operation-based CRDTs from five combinators, carrying convergence proofs through composition and into an executable implementation. Aug 30, 2026 Formalizing Gromov's Theorem in Lean Upcoming talk · Aaron Hill A formalization of Gromov's theorem on groups of polynomial growth — every finitely generated group of polynomial growth is virtually nilpotent — a founding result of geometric group theory. Aug 16, 2026 Prismriver Past talk · Claire Wang 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 Past talk · Joomy Korkut 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 Past talk · Justin Asher 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 Past talk · Gregory Wickham Building a Hilbert space and a *-homomorphism from a C*-algebra — an essential step toward the Gelfand–Naimark theorem, now merged into Mathlib.