A Crash Course in Type Theory

Patrick Lutz gave an overview of the mathematics of type theory together with some notes on how Lean4 implements it in a talk titled A Crash Course in Type Theory. Additionally, we discussed various exercises that Calvin collected in the lean_exercises folder in the Github repository.

Slides available here: https://docs.google.com/presentation/d/1rCUIwiDXAjgJETUytakntq0P4oQpf5HqYG8wMaX-j9c/

---

Date published: Monday, February 16, 2026