Touseef Haider

About
Research
Data Science
Other
Contact

Lean4 Learning Group Summer 2025

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