Interactive Theorem Proving using Lean, Summer 2025
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 openvscode
, 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 tomyExercises
. Otherwise, an update of the repository may overwrite the local files. -
To update the course materials, enter
git pull
from within theleancourse
directory.
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. Table of Contents
- 2. Introduction
- 3. Lean
-
4. Tactics
- 4.1. Tactics Cheatsheet
-
4.2.
apply
-
4.3.
apply?
-
4.4.
assumption
-
4.5.
by_cases
-
4.6.
by_contra
-
4.7.
calc
-
4.8.
cases'
-
4.9.
change
-
4.10.
clear
-
4.11.
congr
-
4.12.
constructor
-
4.13.
exact
-
4.14.
exfalso
-
4.15.
have
-
4.16.
induction
-
4.17.
intro
-
4.18.
left
-
4.19.
linarith
-
4.20.
norm_num
-
4.21.
nth_rewrite
-
4.22.
obtain
-
4.23.
push_neg
-
4.24.
rcases
-
4.25.
refine
-
4.26.
revert
-
4.27.
rfl
-
4.28.
right
-
4.29.
ring
-
4.30.
rintro
-
4.31.
rw
-
4.32.
simp
-
4.33.
specialize
-
4.34.
tauto
-
4.35.
triv
-
4.36.
use