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.

  • Local installation of Lean and the associated tools: Please follow these 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

When you type code . within the leancourse folder, navigate to Leancourse/Exercises/01-Logic/01-a.lean, accept to haveELAN installed, as well as the corresponding Lean version. When all is finished. 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: Right click here and open link in new tab to access the repository using Gitpod. You will probably need a github account in order to do this.)

  1. 1. Introduction
    1. 1.1. Goals
    2. 1.2. Other material and Theorem provers
    3. 1.3. Some notes on Lean and Mathlib
    4. 1.4. How to use this course
  2. 2. Lean
    1. 2.1. Notes on Lean
    2. 2.2. Proofs in Lean
  3. 3. Tactics
    1. 3.1. Tactics Cheatsheet
    2. 3.2. apply
    3. 3.3. apply?
    4. 3.4. assumption
    5. 3.5. by_cases
    6. 3.6. by_contra
    7. 3.7. calc
    8. 3.8. cases'
    9. 3.9. change
    10. 3.10. clear
    11. 3.11. congr
    12. 3.12. constructor
    13. 3.13. exact
    14. 3.14. exfalso
    15. 3.15. have
    16. 3.16. induction
    17. 3.17. intro
    18. 3.18. left
    19. 3.19. linarith
    20. 3.20. norm_num
    21. 3.21. nth_rewrite
    22. 3.22. obtain
    23. 3.23. push_neg
    24. 3.24. rcases
    25. 3.25. refine
    26. 3.26. revert
    27. 3.27. rfl
    28. 3.28. right
    29. 3.29. ring
    30. 3.30. rintro
    31. 3.31. rw
    32. 3.32. simp
    33. 3.33. specialize
    34. 3.34. tauto
    35. 3.35. triv
    36. 3.36. use