Installing Lean (and VSCode) on Windows from scratch

This post is now very old and out of date so I deleted it; for instructions on installing Lean see the Lean community website here.

About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in Technical assistance. Bookmark the permalink.

5 Responses to Installing Lean (and VSCode) on Windows from scratch

  1. Pingback: Proving trivial things with Lean | Xena

  2. Philip Thiede says:

    I got an error when installing it on macOS, something along the lines of that it couldn’t run “lean –version”. This is what I did to fix it!

    1. Install homebrew from
    2. Install the program gmp using homebrew, by typing “brew install gmp” into your terminal.

    I figured this out by searching online, and following the directions from this post on StackOverflow:

    It worked for me and some other people using macs during the first meeting (Thurs 5th Oct)!

    Liked by 1 person

  3. Elliott Macneil says:

    If you are trying to install Lean on macOS using the steps outlined above (in addition to Philip Thiede’s comment) and you’re still stuck on step 4 (“Tell the VSCode Lean extension where Lean is”) then be aware of the type of quotation marks in this webpage.

    If you’re copying the executable path from the webpage, then the use of the ‘curly’ “” quotation marks will not work. Instead, replace this with ‘straight’ “” quotation marks, and this should work now.


  4. xenaproject says:

    I made an html error. I think they’re fixed now. Thanks Elliott.


  5. xenaproject says:

    Peiran Wu sent me a very helpful email, saying that they had managed to get VS Code working with Lean installed in C:\Program Files (i.e. a path name with a space in). Their trick was that instead of setting “lean.executablePath” in the VS Code User Settings, one can add the directory of the Lean binary to the system path by modifying the Windows system environment variable. I’m sure google will be able to tell you how to change system environment variables in any recent version of Windows, so this sounds like a great solution.

    Thanks Peiran!


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s