Calendar
Past topics
Final project work
- Apr 18
- Day 1
- Apr 20
- Day 2
Logical foundations of Lean
- Apr 6
- Type universes and the oddball Prop
- Sections 12.1-12.3
- Apr 11
- Subtypes
- Section 12.4
- Apr 13
- Quotient types
- Section 12.5
Verification, Specification, and Inductive Predicates
- Mar 14
- An inductive predicate for sorted lists
- Chapter 6
- Mar 16
- Insert sort in Lean
- Mar 21
- Prove that our InserSort sorts
- Mar 23
- Refactor from Bool to Decidable Prop
- Mar 28
- Compiling and running Lean code
Interlude
- Mar 2
- Advent of Code
- 2022 Day 1
Programming constructs in Lean
- Feb 16
- Structures
- Section 5.5
- Quiz 5
- Feb 21
- More on structures
- Feb 23
- Classes and instances
- Section 5.6
- Quiz 6
- Feb 28
- Categories via classes
- Mar 30
- Monads
- Chapter 7
- Apr 4
- Monads II: the re-monading
Proofs and tactics
- Jan 24
- Theorems and proofs
- Sections 2.3-3.1
- HW 1 due
- Jan 26
- First tactics and some logic
- Sections 3.2-3.3
- Quiz 2
- Jan 31
- Quantifiers in Lean
- Sections 3.3
- HW 2 due
- Feb 2
- More quantifiers and equality in Lean
- Sections 3.4-3.5
- Quiz 3
- Feb 7
- Induction in Lean
- Section 3.6
- HW 3 due
- Feb 9
- More tactics
- Sections 4.1-4.2
- Quiz 4
- Feb 14
- Calc tactic & proof terms
- Sections 4.3-4.4
- HW 4 due
Terms, types, and type-checking
- Jan 12
- Terms and types
- Sections 1.1-1.2
- Jan 17
- Type checking and type inhabitation
- Sections 1.3-1.4
- Jan 19
- Intro to inductive types
- Sections 2.1-2.2
- Quiz 1
Introduction and setup
- Jan 10
- Orientation