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
- Oct 15: TPIL Chapters 4+7
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 Sep 8: Lean design and first steps
- lean Sep 8: First steps
- lean Sep 10: Name spaces, simple types, products, functions
- lean Sep 15: Polymorphism, implicit arguments, dependent function types
- pdf Sep 17: First steps in logic
- lean Sep 17: Variable declarations, universes, first steps in logic
- pdf Sep 22: Propositions as types
- lean Sep 22: Propositions as types
- lean Sep 24: More on propositional logic
- pdf Sep 29: Topological interpretation of propositional intuitionistic logic, and the BHK interpretation of quantifiers
- lean Sep 29: Quantifiers
- lean Oct 1: Equality and inductive types
- lean Oct 6: Inductive types, continued