Formalising Mathematics in Lean - Utrecht Summerschool 2026

An interactive theorem prover is a computer program to assist with the development of mathematical proofs. By checking and automating proof steps, the machine aides the user in creating proofs in a formal language understandable to the program.

Formalizing mathematics is the process of typing mathematical proofs into the interface of an interactive theorem prover. In the past years, more and more mathematics, from undergraduate level to the frontiers of modern research have been formalized in a variety of proof assistants.

While there are many interactive theorem provers, this course focuses on Lean and its mathematical library mathlib, which already contains a substantial number of proofs of mathematical theorems and infrastructure for proof automation.

Registration

For registration please head to the registration page.

Note that the cost for students is 200€.

Target audience

The course is targeted to students familiar with rigorous mathematical proofs (e.g. careful proofs by induction) that have an interest in theorem proving in Lean.

Students in science (mathematics, computer science, physics, etc) that are coursing the second half of their bachelor, or are doing a MSc or a PhD will be well prepared for this course.

Aim of the course

Participants will learn how to formalize mathematics in Lean. The acquired knowledge will not only enable participants to contribute to Lean's mathematical library mathlib - it will also strengthen their understanding of mathematics.

Study load

The course takes one week, with a few hours of lectures per day. We will offer supervised lab sessions to practice with the material taught in the lectures.

In the second part of the week, participants will work on self-chosen formalization projects in teams with assistance and supervision by experienced Lean users.

The schedule is available here.