Machine-checked mathematics


Course Objective

This course will provide an introduction to the practice of formalizing
mathematics in dependent type theory, using an interactive proof
assistant and its library. The course will be based on the proof
assistant Coq and its Mathematical Components library.

Course Content

Proof assistants are pieces of software for doing machine-assisted
mathematics and for developing digital libraries of formalized
mathematics. This course will provide an introduction to the foundations
and practice of the Coq proof assistant. It will include a primer to
dependent type-theory, the logical formalism underlying a family of
popular proof assistants like Lean, Agda, Matita, and Coq. The course
will start with a gentle introduction to the art of writing formal
statements and proofs. Then, it will present the concepts and
formalization techniques at stake in the representation of mathematics
in dependent type theory. Hands-on sessions will address concrete
formalization examples, both in computational mathematics and in purely
deductive proofs.

Teaching Methods

Intensive course interleaved with hands-on sessions 5h a day for 3 days.
Personal laptop mandatory (but no software installation required).
Lectures will take place 17-19-21 Feb.

Method of Assessment

Two small hand-in examinations, to be handed on 19 and 21 Feb.
respectively, count for 30% of the final grade. A final on-site hands-on
test, on Feb. 28th, counts for 70% of the final grade.


Course notes.

Target Audience

MSc students in Mathematics. Interested MSc students from other
disciplines, especially (Theoretical) Computer Science, are also
welcome. As are advanced motivated BSc students.

Recommended background knowledge

No previous experience with formal verification and no background in
functional programming is required. Ability to understand and write down
detailed mathematical proofs in general, is expected.

General Information

Course Code XM_0081
Credits 2 EC
Period P4
Course Level 400
Language of Tuition English
Faculty Faculty of Science
Course Coordinator dr. A.S. Mahboubi
Examiner dr. A.S. Mahboubi
Teaching Staff dr. A.S. Mahboubi

Practical Information

You need to register for this course yourself

Last-minute registration is available for this course.

Teaching Methods Seminar, Computer lab, Lecture
Target audiences

This course is also available as: