Thursday 10am in Southwick 350V, or on Zoom as needed
- Install VSCode and the Lean 4 extension
- Install git
- Clone or fork this repository
- Mathematics in Lean (MIL): https://leanprover-community.github.io/mathematics_in_lean
- Theorem Proving in Lean (TPL): https://lean-lang.org/theorem_proving_in_lean4/
- Lean courses at other universities, for example:
- University of Bonn: https://github.com/fpvandoorn/LeanCourse24/
- Imperial College London: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024
- Fordham University: https://github.com/hrmacbeth/math2001
- Lean community website: https://leanprover-community.github.io/
- Zulip chat: https://leanprover.zulipchat.com/
More advanced resources on Lean internals and metaprogramming:
- Lean Language Reference: https://lean-lang.org/doc/reference/latest/
- Metaprogramming in Lean 4: https://leanprover-community.github.io/lean4-metaprogramming-book/
- Functional programming in Lean: https://leanprover.github.io/functional_programming_in_lean/
There will not be any exams in this course. Your grade will be based on homework assignments.
- Week 1 (Thu, Feb 6): Rewriting, calculations (MIL Ch. 1, 2)
- Week 2: Logic (MIL Ch. 3)
- Week 3: Sets and Functions (MIL Ch. 4)
- Week 4: Induction and Coercions (MIL Ch. 5.2)
- Week 5: Structures and Typeclasses (MIL Ch. 6, 7)
- Week 6: Limits and filters (MIL Ch. 10.1)
- Week 7: Derivatives (MIL Ch. 11.1)
- Week 8: Integrals (MIL Ch. 12.1)
- Week 9: Formalization practice: Riemann-Lebesgue lemma
- No class on Thu, Apr 17
- Week 10: Macros and monads
- Week 11 (Apr 30): Wrap-up