Introduction

Introduction#

These are lecture notes for the doctoral course Selected topics in computational mathematics: formalized mathematics and proof assistants, taught at the Faculty of Mathematics and Physics, University of Ljubljana, in the fall semester of 2024/25.

The course is targeted at graduate students in mathematics and other mathematicians who are interested in learning formalized mathematics. We shall pay attention both to the theoretical underpinnings of proof assistants and to practical aspect of formalization. The goal is not only to teach the craft of formalized mathematics, but also to explain what happens inside a proof assistant.

Basic course information:

Further resources and reading material are given within each lecture.

Discord#

Most communication will take place on the departmental Discord server. Please join it by visiting the course Moodle page where you will find an invitation link.

How to participate#

If you are a PhD or MSc student at the Faculty of Mathematics and Physics, you may enrol in the course and visit the lectures.

Outside participants are welcome to follow the course by watching the video lectures and participating in the Discord server. If you plan to do so, please introduce yourself to the lecturer and let him know of your intentions.

Course prerequisites#

The students need not have any prior knowledge of type theory, formalized mathematics, or proof assistants. However, this being a doctoral course, a certain level of mathematical maturity is expected. Course work will involve installing and using academic-grade software, which requires a bit of experience or enough tenacity and willingness to learn.

Course requirements#

To pass the course, you will complete a small formalization project of your own choosing. Instructions will be posted in due course.

Lectures#

The following is an outline of the lectures.

Contents