Jasper Ganten:
Probability Theory and Monads: From Category Theory to Lean4 Implementation
Time and place
Thursday, 18.9.25, 10:00-11:00, Seminarraum 232
Abstract
Monads provide an elegant categorical framework for formalizing probabilistic objects. Using the Giry monad as our theoretical foundation, I demonstrate how probability measures can be structured categorically and then implement this in Lean4 through the binomial distribution.
Three equivalent definitions—recursive, convolution-based, and closed formula—illustrate both the power of categorical abstraction and the practical challenges of formal verification. Key technical hurdles include working with extended nonnegative real numbers versus standard reals, managing type conversions, and proving equivalence between different implementations.
The talk targets mathematically interested audiences with basic probability knowledge—no prior experience with category theory or Lean required. Through concrete code examples, I'll show how elegant mathematical theory meets the gritty reality of formal proof verification.