Courses

2360124 Proving theorems in Lean Winter 2024/2025

In this class, we will learn how to use Lean to prove mathematical theorems.

The first class will include a short introduction to Lean. In the few following weeks, you will learn the hooks by following slides and solving exercises in groups. The instructors will go from group to group, helping you understand the material. At this point, you will divide into groups, each group choosing a project (a certain theorem or a certain mathematical theory). The rest of the semester will be devoted to completing the project, with help from the instructors.

Class materials: