Interactive Theorem Proving using Lean, Winter 2026/27🔗

These are the notes for a course on formal proving with the interactive theorem prover Lean4 (in the following we just write Lean) in the winter semester of 2026/27 at the University of Freiburg. To be able to work through the course in a meaningful way, the following technical preparations are to be made:

• Installation of vscode.

• Open vscode, hit the extensions icon (fifth from the top) on the left, and install the Lean 4 language extension.

• If you haven't done already, install git. For this, the best way is to open vscode, hit the git icon (third from the top on the left), and follow the instructions.

• Installing the course repository: Navigate to a location where you would like to put the course materials and use

git clone https://github.com/pfaffelh/leancourse
cd leancourse
lake exe cache get
code .

Then, vscode should open and you see the course materials.

After having typed code . within the leancourse folder, navigate to Leancourse/Exercises/01-Logic/01-a.lean. Everything is fine once orange and/or red bars disapprear, and navigating in the left hand side of the windom leads to changes in the right hand side (the infoview). You should see some code which looks a bit like mathematics.

• The directory Leancourse/Exercises contains the material for the course. We recommend that you first copy this directory, for example to myExercises. Otherwise, an update of the repository may overwrite the local files.

• To update the course materials, enter git pull from within the leancoursedirectory.

In case you cannot install the course material locally, do the following: Visit this page and click on the green Code-button. Navigate to Codespaces and open the course notes there. You get a window which looks a lot like vscode, so please follow the instructions from above. You will have to Restart Lean and Restart File and wait several minutes until all is set. (If you see a red vertical bar, something is wrong. If you see an orange vertical bar, you will have to wait longer.) You will probably need a github account in order to open the coursenotes in Codespaces.