Lean Interactive Theorem Prover

SLUG (Stockholm Lean User Group)

Formalization Projects

Linear Algebra Game

With Alex Bentkamp, Jon Eugester, and Marcus Zibrowius, we developed the Linear Algebra Game for teaching a seminar course on proof-based linear algebra to undergraduate students at Heinrich Heine University, Düsseldorf. We also maintain the Lean Game Server. You can make your own game using the Game Skeleton.

Contribution to Mathlib

• Locally Cartesian Closed Categories
• Monoidal and Cartesian Distributive Categories
• Grothendieck construction for category-valued functors
• Cartesian closedness of sheaf categories, coauthored with Dagur Asgeirsson, Jon Eugster
• Finite products for the preorder category of a meet-semilattice with a top element
• Stonean is precoherent,coauthored with Dagur Asgeirsson, Jon Eugster, Boris Bolvig Kjær, Nima Rasekh
• Grothendieck construction for type-valued functors
• ExtrDisc is precoherent, coauthored with Dagur Asgeirsson, Jon Eugster, Boris Bolvig Kjær, Nima Rasekh
• Profinite is precoherent
• Various basic API lemmas in set theory
• Triple adjunctions of slice cateogries
• Wide subcategories

Teaching with Lean Interactive Theorem Prover

Introduction to Proofs

1. Computability and Incompleteness, Stockholm University, Fall 2025
2. Introduction to Proofs, Johns Hopkins University, Spring 2024
3. Introduction to Proofs, Johns Hopkins University, Fall 2023
4. Introduction to Proofs, Johns Hopkins University, Fall 2022
5. Introduction to Proofs, Johns Hopkins University, Spring 2022