Interactive Theorem Proving (Laurea Magistrale in Matematica)

Information

This course aims to introduce students to interactive theorem proving and formalized mathematics using Lean 4.

All the course material can be found on

• the GitHub repository (to be made available)

The syllabus of the course is available on ESSE3.

Please refer to the Moodle course page for additional information.

Home - Teaching

Roberto Zunino, 2025