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.