1) Prerequisites:
Mathematical maturity (especially concerning proofs) is most important, but this should be satisfied by anyone entering an MSc Mathematics programme. We assume familiarity with basic notions in algebra, topology, and analysis (as taught in most BSc Mathematics programmes), such as groups, rings, vector spaces, metric spaces, and topologicas spaces, together with their associated morphisms, quotiens, and basic invariants.
Some familiarity with programming or computer algebra systems would be helpful, but is not strictly necessary.
2) Aim of the course:
The focus of this course is the theory and practice of proof assistants in mathematics. We will also touch on adjacent topics such as (external) automated theorem provers. The theory part will involve a treatment of the (dependent) type theory on which the underlying logical foundations of proof assistants such as Coq, Lean, and Agda are based. In the practical part, the students will learn how to use a proof assistant, for which we shall focus on Lean, together with its (main) mathematical library "mathlib". In particular, as part of the course, each student will work in a small group on a formalization project on a mathematical topic of their choice.
3) Rules about Homework/Exam:
The final mark will for 30% be based on regular homework exercises and for 70% on a final oral exam, with the extra rule that in order to pass the course the student needs to score at least a 5.0 on the final exam. The oral exam will be about the (contributions to the) formalization project as well as the "overall" understanding of the other course content.
There will be a possibility to retake the final oral exam; homework (for which there is no retake) still counts toward the final grade then.
4) Lecture notes/Literature:
A significant part of the course will use "Mathemmatics in Lean", available at:
https://leanprover-community.github.io/mathematics_in_lean/
Further material will be made available online throughout the course.
5) Lecturers:
Johan Commelin (UU) and Sander Dahmen (VU); we expect some "guest lectures" to be given by Assia Mahboubi (VU/Inria, Nantes).
- Docent: Johan Commelin
- Docent: Sander Dahmen