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) 
leanmode 
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 
MidSemester 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 (theHottBook) 

12 
04/17 
Axioms (Chapter 12 of the tutorial) 
Spring Carnival 
13 
04/24 
Formal Methods in Mathematics 


05/01 
No class 
