Date | Group Number | Content | Recommended Reading | Lecture Notes |
---|---|---|---|---|
May 12 | Group 1 | Lean's Interactive Feedback Loop & Course Overview | Mathematics in Lean : Chapter 1 | Day_1 |
May 13 | Group 2 | Propositions as Types, Proofs as Objects (Curry-Howard Correspondence) |
Video:1
Video:2 |
Day_2 |
May 14 | Group 3 | Basic Tactics and First Proofs using rfl and rw. | Mathematics In Lean(MIL) 2.1 | Day_3 |
May 15 | Group 4 | Using Existing Lemmas. | Mathematics In Lean(MIL) 2.2 | Day_4 |
May 16 | Group 5 | Overview of tactics intro, exact, apply, simp. | Mathematics In Lean(MIL) 2.3 | Day_5 |
May 19 | Group 1 | Implication and Universal Quantifier | Mathematics In Lean(MIL) 3.1 | Day_6 |
May 20 | Group 2 | Existential Quantifier | Mathematics In Lean(MIL) 3.2 | Day_7 |
May 21 | Group 3 | Negation and Proof by Contradiction | Mathematics In Lean(MIL) 3.3 | Day_8 |
May 22 | Group 4 | Conjuctions and Bi-implication | Mathematics In Lean(MIL) 3.4 | Day_9 |
May 23 | Group 5 | Disjunction and Proof by Cases | Mathematics In Lean(MIL) 3.5 | Day_10 |
May 26 | Group 1 | Sequences and Convergence | Mathematics In Lean(MIL) 3.6 | Day_11 |
May 27 | Group 2 | Sets | Mathematics In Lean(MIL) 4.1 | Day_12 |