Interactive Theorem Proving using Lean, Summer 2025🔗

Peter Pfaffelhuber

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 summer semester of 2025 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.

Note: Yet another description how to install Lean is found here.

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.

  1. 1. Table of Contents
  2. 2. Introduction
    1. 2.1. Goals
    2. 2.2. Other material and Theorem provers
    3. 2.3. Some notes on Lean and Mathlib
    4. 2.4. How to use this course
  3. 3. Lean
    1. 3.1. Notes on Lean
    2. 3.2. Proofs in Lean
  4. 4. Tactics
    1. 4.1. Tactics Cheatsheet
    2. 4.2. apply
    3. 4.3. apply?
    4. 4.4. assumption
    5. 4.5. by_cases
    6. 4.6. by_contra
    7. 4.7. calc
    8. 4.8. cases'
    9. 4.9. change
    10. 4.10. clear
    11. 4.11. congr
    12. 4.12. constructor
    13. 4.13. exact
    14. 4.14. exfalso
    15. 4.15. have
    16. 4.16. induction
    17. 4.17. intro
    18. 4.18. left
    19. 4.19. linarith
    20. 4.20. norm_num
    21. 4.21. nth_rewrite
    22. 4.22. obtain
    23. 4.23. push_neg
    24. 4.24. rcases
    25. 4.25. refine
    26. 4.26. revert
    27. 4.27. rfl
    28. 4.28. right
    29. 4.29. ring
    30. 4.30. rintro
    31. 4.31. rw
    32. 4.32. simp
    33. 4.33. specialize
    34. 4.34. tauto
    35. 4.35. triv
    36. 4.36. use
  5. 5. Projects
    1. 5.1. Induction (Luis Jaschke und Felicitas Kissel)
    2. 5.2. Own addition on ℚ (Adrian Eckstein und Debora Ortlieb)
    3. 5.3. Fixed points and contractions (Jule Kiesele, Anna Vitiello)
    4. 5.4. Path-connected spaces (Jasper Ganten)
    5. 5.5. Parallel inequality (Moritz Graßnitzer, Natalie Jahnes)
    6. 5.6. There is only one prime triplet (Patrick Nasdala, Max Lehr)
    7. 5.7. An equivalence on sets (Emma Reichel, Luisa Caspary)