Textbooks
We are using two online textbooks, both free.
-
Theorem Proving in Lean 4
— Avigad, de Moura, Kong, and Ullrich -
Mathematics in Lean
— Avigad and Massot
Installing VS Code and Lean
Quick links:
- Lean Web — run Lean and Mathlib right in your browser, no install required (needs an internet connection)
- Download VS Code
Step-by-step videos:
Reading Assignments
The reading assignments are from Theorem Proving in Lean 4 (TPIL) and Mathematics in Lean (MIL).
- Sep 10: TPIL Chapters 1+2
- Sep 15: TPIL Chapter 3
Lecture Notes
These files use the Unicode character set and are UTF-8 encoded. If your browser does not display them correctly, download the files instead — Lean Web or VS Code will know what to do with them.
- pdf Sept 8: Lean design and first steps
- lean Sept 8: First steps
- lean Sept 10: Name spaces, simple types, products, functions
- lean Sept 15: Polymorphism, implicit arguments, dependent function types
- pdf Sept 17: First steps in logic
- lean Sept 17: Variable declarations, universes, first steps in logic
- pdf Sept 22: Propositions as types
- lean Sept 22: Propositions as types
- lean Sept 24: More on propositional logic