Lean theorem prover and monoidal category theory
Organizers
Speaker
Yuma Mizuno
Time
Wednesday, June 18, 2025 3:00 PM - 4:30 PM
Venue
A3-3-301
Online
Zoom 242 742 6089
(BIMSA)
Abstract
Lean is a theorem prover that enables mathematical formalization with computer-verified correctness. In this talk, I will provide an overview of monoidal category theory as implemented in Mathlib, which is Lean's user-maintained mathematics library. I will also explain how Lean's metaprogramming framework handles the coherence theorem in monoidal categories, demonstrating the interaction between functional programming and formalized mathematics.
Speaker Intro
Yuma Mizuno obtained his PhD from Tokyo Institute of Technology with research on cluster algebras. He is currently a postdoc at University College Dublin. He is also interested in Lean theorem prover and is working on formalization of 2-category theory.