Lean Interactive Theorem Prover

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. See more about this in the following link below from a talk I gave at the Hausdorff Research Institute in Mathematics (HIM), Bonn.

Linear Algebra Game in Lean4

Contribution to Mathlib

• Grothendieck construction for category-valued functors
• Cartesian closedness of sheaf categories, with Dagur Asgeirsson, Jon Eugster
• Stonean is precoherent, with Dagur Asgeirsson, Jon Eugster, Boris Bolvig Kjær, Nima Rasekh
• Grothendieck construction for type-valued functors
• ExtrDisc is precoherent, 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. Johns Hopkins University, Fall 2023
2. Johns Hopkins University, Fall 2022
3. Johns Hopkins University, Spring 2022
4. Johns Hopkins University, Fall 2021