CMU 15-815 Interactive Theorem Proving

Lecture Slides and Reading

# Date Lecture Additional Readings and Notes
1 01/16 Introduction / Dependent Type Theory (Chapters 1 & 2 of the tutorial)
2 01/23 Dependent Type Theory / Propositions and Proofs (Chapters 2 & 3 of the tutorial) lean-mode
3 01/30 Propositions and Proofs / Quantifiers and Equality (Chapters 3 & 4 of the tutorial)
4 02/06 Quantifiers and Equality / Interacting with Lean (Chapter 4 & 5 of the tutorial)
5 02/13 Inductive Types (Chapter 6 of the tutorial) Inductive Families
6 02/20 The formal proof of the Kepler conjecture, Thomas Hales Professor, University of Pittsburgh
7 02/27 Inductive Types, Induction and Recursion (Chapters 6 and 7 of the tutorial)
03/06 No Class Mid-Semester Break
03/13 No Class Spring Break
8 03/20 Elaboration and Unification (Leonardo de Moura; Chapter 8 of the tutorial)
9 03/27 Type Classes and Structures (Chapters 9 and 10 of the tutorial) Elaboration
10 04/03 Tactics (Chapter 11 of the tutorial)
11 04/10 Homotopy Type Theory (the-Hott-Book)
12 04/17 Axioms (Chapter 12 of the tutorial) Spring Carnival
13 04/24 Formal Methods in Mathematics
05/01 No class