Lean For The Curious Mathematician 2024
25-29 March 2024
This is the main repository for the conference Lean For The Curious Mathematician 2024.
- All the files needed during the lectures are in the subfolder
LFTCM2024
. See below for the instructions to install everything you need. - Here is the schedule of the conference.
Installation
Note: to get this repository, you will need to download Lean's mathematical library, which takes about 5 GB of storage space.
- You have to install Lean, and two supporting programs: Git and VSCode (including the Lean4 extension). Follow these instructions to do this. You do not have to follow the last step (creating Lean projects). Instead, use either VSCode or a terminal to get this repository.
Get the Repository using VSCode
-
Open Visual Studio Code.
-
If no file is open, create a new empty text file (
File ... > New Text File
). -
In the top-right (or top-middle) of the screen there is a Lean menu marked by
∀
. In it, chooseOpen Project... > Project: Download Project
. If you don't see the∀
, the Lean extension is not installed, go back to the previous step or ask for help. -
Type
https://github.com/riccardobrasca/LFTCM2024.git
and press enter (note that VSCode suggests you to download mathlib, that is not this repository).
-
Choose a name for the folder where you want to have this repository (for example
LFTCM2024
). This downloads the project, including mathlib, and will take a bit of time. -
Press
Open Project Folder
when asked if you want to open the folder. -
If VSCode asks
Do you trust the authors of the files in this folder?
clickYes, I trust the authors
. -
Open the file
LFTCM2024/Test.lean
using the explorer button in the top-left. -
VSCode will pause for a bit (10-40 seconds, depending on your computer), showing a
Starting Lean language client
pop-up. -
When the pop-up
Imports of 'Test.lean' are out of date and must be rebuilt.
appears, click onRestart File
and wait a couple of seconds (this part should be very quick). -
Everything should be ready now. If you see a blue squiggle under
#eval
, Lean is running correctly.
Get the Repository using a terminal
-
Open a terminal (I recommend
git bash
on Windows, which was installed as part of git in the first step). -
Use
cd
to navigate to a directory where you would like to create theLFTCM2024
folder. -
Run the following three commands.
git clone https://github.com/riccardobrasca/LFTCM2024.git
cd LFTCM2024
lake exe cache get!
The last one downloads mathlib, and will take a bit of time.
-
On Windows, if you get an error that starts with
curl: (35) schannel: next InitializeSecurityContext failed
it is probably your antivirus program that doesn't like that we're downloading many files. The easiest solution is to temporarily disable your antivirus program. -
Run
lake build +LFTCM2024.Common
This should take less than 1 minute. If you get more than a few lines of output, then you're rebuilding Mathlib from scratch, which means that one of the steps above (
lake exe cache get!
) went wrong. You can quit the execution (by typingCtrl c
) and ask for help. -
Launch VS Code, either through your application menu or by typing (note the dot!)
code .
MacOS users need to take a one-off extra step to be able to launch VS Code from the command line.
-
If you launched VS Code from a menu, on the main screen, or in the File menu, click "Open folder" (just "Open" on a Mac), and choose the folder
LFTCM2024
(not one of its subfolders). -
If VSCode asks
Do you trust the authors of the files in this folder?
clickYes, I trust the authors
-
Test that everything is working by opening
LFTCM2024/Test.lean
. It is normal if it takes 10-40 seconds for Lean to start up. -
Everything should be ready now. If you see a blue squiggle under
#eval
, Lean is running correctly.
Update the repository
If you have already followed the steps above, and want to update the repository, open a terminal in your local copy of this repository (e.g. cd LFTCM2024
) and then run
git pull
This gives you the new exercises.
Error Lens extension
Optional: some users find it useful to download the Error Lens
extension. This displays Lean messages directly in your source file.
To get it, in the left bar of VSCode, click on the Extensions
button (4-th or 5-th button), and search and install the extension Error Lens
. It will start automatically.
Alternative ways to use Lean
You can use Codespaces if you have trouble installing Lean locally. These work fine, but not as well as a locally installed copy of Lean.
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.
To restart a previous codespace, go to https://github.com/codespaces/.
Troubleshooting
If you get the error unknown package 'Mathlib'
and a red squiggle under import Mathlib.Tactic
then you probably didn't open the right folder (what you see might be slightly different from the screenshot below depending on the extensions you have installed, but the red squiggle shouldn't be there).
- Make sure to select
File/Open Folder
(notFile/Open File
) and to select the root folder calledLFTCM2024
(or the name you chose during the installation). Note that this folder contains another folder also calledLFTCM2024
: you have to select the first one (not the oneLFTCM2024/LFTCM2024
). - If the error persists you can use Codespaces as described above and ask for help.