This is the repository for the summerschool on Formalising Mathematics in Lean at Utrecht University in 2026. It contains the course material, including lectures, exercises and project sketches.
To try out Lean and to follow the content of the first day, you don't need a local Lean installation. Instead, you can use the online Lean editor.
We will also play the Natural Number Game on the first day to learn the basics of Lean.
From the second day on, to follow the lectures, to do the exercises and to work on projects, you will need a local Lean installation. The recommended way is to install VS Code and the Lean extension following the first 3 steps of these instructions.
Now, open VS Code and click on the forall symbol on the right hand side of the screen and select
Open Project > Project: Download Project:
There will appear a text box, in which you copy the following URL:
https://github.com/formal-methods-nl/uu-summerschool-2025
After selecting a path where the project should be installed on your computer, wait for a few minutes for everything to download and compile.
You will find the course material in the UuSummerschool2026 directory.