Last tinkered with: October 2018. I will attempt to keep these instructions up to date.
I want to try Lean and mathlib.
If you’re sitting in front of a computer and you want to try Lean, there are lots of different ways to do so. Here is an overview of several approaches. You get what you pay for here. Every method here gives you the latest Lean, and a fairly recent version of mathlib.
Using Lean without installing anything.
Option 1: The Lean Web Editor.
By far the simplest way to use Lean is to use the Lean Web Editor. You can run Lean in your browser, and a version of mathlib from around June 2018 or so (NB: this is a guess). Note: if it says “(running)” at the top, it’s compiling.
Advantages: (a) no installation needed — it just works. (b) works fine for small tests.
Disadvantages: (a) it’s slow. (b) version of mathlib is slightly old and you can’t upgrade it (this is not an issue if you’re just learning).
Option 2: Use Lean on CoCalc
If you have an account on CoCalc then you can use Lean straight out of the box (as well as a bunch of other maths packages such as Sagemath). Create a file called
test.lean in a project and just click on it. It just works.
Advantages: (a) no installation needed. (b) if you pay a few dollars a month (or get your institution to pay) you have access to fast servers.
Disadvantages: (a) if you don’t pay, it can sometimes be slow. (b) We are still figuring out how to keep mathlib up to date whilst not annoying the devs too much. I guess it’s worth noting however that if you’re an undergraduate at Imperial then I can solve both of these problems for you (because Imperial paid and I can show you how to install bleeding edge mathlib locally) and you should get in touch with me.
Installing Lean on your own machine.
If you have a computer of your own which you’d like to install Lean and mathlib on, there are again a couple of options. This is the most convenient way to use Lean, once everything is set up correctly.
Option 3: cheap hack to get up and running on Windows 10.
If you are using Windows 10, have never heard of git or the command line, and you want to install Lean on your local machine with the minimum of fuss, then the nearest we have to a “one click install” is explained here. This gives you a version of mathlib from late September.
Advantages: (a) observational studies indicate high success rate.
Disadvantages: (a) the version of mathlib is slightly old and you can’t upgrade it because you cut corners (this is not an issue if you are just learning).
Option 4: correct full installation (any OS).
If you want to bite the bullet and install Lean and mathlib properly, so you have the latest version of mathlib on your machine and can download updates to mathlib easily, then you need to install git, and if you’re on Windows you need to install a terminal too, so you can type commands into your computer instead of just clicking on stuff. Installation instructions vary over operating systems. The community recommends that you use something called “elan” to install and manage Lean itself.
Thank you to Scott Morrison for writing the docs and making the videos.
If you like reading words, then instructions for Windows, Mac and Linux are here
If you like watching videos, then try these:
Mac OS: Lean/mathlib installation video
Windows: Lean/mathlib installation video
Is it all working?
For the online options, the answer is “probably”.
For the local installation versions, the answer is “maybe”. Here’s how to test it.
If you want Lean and mathlib to work on a local installation, you need to open a project. You can tell when a folder contains a Lean project because the folder will have a file called
leanpkg.path and another file called
leanpkg.toml in it. You open the project in VS Code by clicking on
File -> Open Folder and opening the project folder. Just to be completely clear — the name of the thing you should be opening is the name of a folder, and this folder should contain these two
leanpkg.toml files directly in the folder (not in a subfolder or whatever). If you are missing the
leanpkg.path file, your imports will probably not work.
With your project open in VS Code, create a file called
test.lean and put this in it.
import data.int.basic #check id
Then in VS Code you hold down Ctrl, then hold down Shift as well, and then hit “Enter” (this opens a “Lean Messages” window if you’ve not got one open already), and then click on the
#check. What we are hoping for is:
1) no red underlines anywhere
2) output saying
id : ?M_1 → ?M_1 in the Lean Messages window.
If that happens, it’s working.
Q) Why do I see orange bars?
A) Just wait. Lean is starting up; the first time it does this can take a while.
Q) No red underlines but no output at all.
A) Maybe Lean is not running. Are you sure your file is called
something.lean and not
something.lean.txt? You can restart Lean in VS Code with Ctrl Shift P (hold down the first two and press the third) then typing
Lean in the box that just appeared and then clicking on
Lean: Restart. If you see orange bars, this is good.
'Smith\.elan\toolchains\stable\bin\..' is not recognized as an internal or external command,
operable program or batch file.
A) Your last name is Smith, you’re using Windows, and your userid is something like
John Smith with a space in. This is a bug in
leanpkg. The Lean dev team is small and nobody uses Windows. The community is working on trying to fix this bug (Oct 2018) but it is not as easy as you might think. Try installing Lean somewhere in a path with no spaces in 😦 Alternatively, go for the cheap hack method outlined above, which should work fine.
Q) Imports don’t work.
A) Did you open a folder containing a package? Lean looks for instructions about where to import stuff from the
leanpkg.path file which should be in the root directory of the project which you opened using
File -> Open Folder.
Q) It still doesn’t work!
A) Come and ask for help at Zulip. Post in the New Members stream. Someone will be with you shortly. Also, write a comment here explaining the problem and I will add it to the FAQ when we’ve solved it.