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 |
-
Rutgers University - Newark, Newark, NJ
Applied Calculus (Fall 2024), Intermediate Algebra (Fall 2022, Summer 2023), College Algebra (Summer 2020, 2021, 2022, 2024) -
Institute of Business Administration, Karachi, Pakistan
Calculus-II with Application (Fall 2016), Linear Algebra (Spring 2017) -
Federal Urdu University, Karachi, Pakistan
Foundation Mathematics (Fall 2015), Mechanics (Fall 2015) -
Rutgers University - Newark, Newark, NJ
College Algebra (Fall 2019, Fall 2020, Spring 2021), Calculus (Spring 2020, Spring 2022, Fall 2023) -
Institute of Business Administration, Karachi, Pakistan
Calculus-II (Fall 2013, Spring 2014), Linear Algebra (Fall 2014)