Bonn Lean Course WiSe 24/25
In this repository
You will find the Lean files in the LeanCourse
directory:
- The
Lectures
folder contains all lectures (I will post 2 versions of each lecture file: the one before - The
Assignments
folder contains the assignments that you have to hand in via eCampus. - The
MIL
folder contains the exercises from the book Mathematics in Lean. You can find the textbook online here: Mathematics in Lean (or as a pdf document).
Installation
-
You have to install Lean, and two supporting programs: Git and VSCode. Follow these instructions to do this.
-
This will guide you to install VSCode (a text editor which supports Lean), git (a version control system) and elan (the Lean package manager).
-
(On Windows, antivirus programs can cause slowdowns or errors when downloading a Lean project. Consider temporarily disabling your antivirus program in the step Set up Lean 4 project)
-
In the step Set up Lean 4 project click on Download an existing project (third bullet point). Choose
Git repository URL
, enterhttps://github.com/fpvandoorn/LeanCourse24
and then select a folder where you want to download this repository, and specify a folder name. Then pressCreate project folder
and wait a few minutes. -
When you have downloaded the repository a message appears allowing you to open the project folder. To test that everything is working, open the repository and open the file
LeanCourse/Test.lean
. The file should be ready a few seconds later. If you see a blue squiggle under#eval
, Lean is running correctly. -
A useful (but optional) extension is the VSCode extension
Error Lens
. If you install this, you will see messages from Lean right in the file where you're typing.
Troubleshooting
Note: To get this repository, you will need to download Lean's mathematical library, which takes about 5 GB of storage space.
It might be tricky to get Lean running on a laptop that is more than 10 years old or on a chromebook, since Lean does use a moderate amount of recourses. You can still run Lean in your browser by using Codespaces or Gitpod, see the the instructions at the bottom of this file.
- If you get errors such as
curl: (35) schannel
oruncaught exception: no such file or directory (error code: 2)
take a look here.
Update repository
If you want to get the latest version of this repository (e.g. the latest exercises), then you can pull the changes. (I mentioned before you have to commit first, this is not, in fact, necessary)
You can do this either via a terminal (git pull
)
or via VSCode, in the Source Control
tab (third icon in the top-left, or ctrl+shift+G
/cmd+shift+G
),
under ⋯
(More actions) you can click Pull
to get the latest changes.
Note: you should not press Sync
, since that will try to upload your changes to the assignment files to Github (you don't have the rights to do this).
We might at some point update the version of Lean for the repository (we will tell you when this happens). In that case, after running git pull
you have to get the new Mathlib cache. In this case, do not restart a Lean file (which will prompt Lean to rebuild Mathlib on your laptop).
Instead press ∀ > Project Actions... > Fetch Mathlib Build Cache
and wait for the cache to download.
After it has finished, you might have to restart the Lean file, and then Lean should be compiling your file in less than a minute.
If this fails, try the following steps:
- Close VSCode (if it is open)
- In your terminal, in the
LeanCourse24
folder, runlake exe cache get!
(or~/.elan/bin/lake exe cache get!
iflake
cannot be found). - Wait until the command finishes with downloading and decompressing. If you get an error, run it again.
- Now you can reopen VSCode and restart the file (if prompted).
Temporary ways to use Lean
You can temporarily use Codespaces or Gitpod if you have trouble installing Lean locally.
Using Codespaces
You can temporarily play with Lean using Github codespaces. This requires a Github account, and you can only use it for a limited amount of time each month. If you are signed in to Github, click here:
- Make sure the Machine type is
4-core
, and then pressCreate codespace
- After 1-2 minutes you see a VSCode window in your browser. However, it is still busily downloading mathlib in the background, so give it another few minutes (5 to be safe) and then open a
.lean
file to start.
Using Gitpod
Gitpod is an alternative to codespaces that is slightly inconvenient, since it requires you to verify your phone number.
Click this button to get started:
This creates a virtual machine in the cloud,
and installs Lean and Mathlib.
It then presents you with a VS Code window, running in a virtual
copy of the repository.
You can update the repository by opening a terminal in the browser
and typing git pull
followed by lake exe cache get!
as above.
Gitpod gives you 50 free hours every month.
When you are done working, choose Stop workspace
from the menu on the left.
The workspace should also stop automatically
30 minutes after the last interaction or 3 minutes after closing the tab.
To restart a previous workspace, go to https://gitpod.io/workspaces/.
Links
- Mathematics in Lean
- Lean website
- Mathlib website
- Topics in Mathlib
- API documentation for this course
- latest Mathlib API documentation
Some exciting projects using Lean:
- Interesting finished Lean projects: Liquid Tensor Experiment, Freiman-Ruzsa Conjecture, Independence of the continuum hypothesis
- Interesting ongoing Lean projects Fermat's Last Theorem, Carleson's theorem, Equational Theories project
- AlphaProof did well at the international mathematics olympiad using Lean.