# How do I install Lean 4?

I want to get started with Lean 4, but I need to install it. The download page links to binaries to download, but I don't know what to do with them. Is there a "best practice" way to install Lean, or should I just download them and put them in my \$PATH?

I'm using Arch Linux (x86-64).

• I agree with the answer by k4rtik. If you're going to ask how to install something, it would be nice if you could show us what you have tried so far. Feb 8 at 18:06
• @NikeDattani "The download page links to binaries to download, but I don't know what to do with them". I was going to install Lean by just copying the binaries somewhere, but I wanted to know if there was a better ("best practice") method of doing so. And now I know about elan, which I missed in my initial search. Feb 8 at 19:49
• Since there is no documentation on how to install the basic binaries (without elan) I would say this is on topic. On linux, /user/local/bin is a good place to put binaries.
– Couchy
Mar 4 at 1:15
• How can installing a proof asssistant be "off topic" on the Proof assistants Q & A site?! Come on people, don't be like those other sites. At least pick a plausible reason for closing the question. Better yet, don't close the question and tell the OP how to ask better. I am disappointed. May 22 at 20:58
• Apologies for digging a three month old question from its grave. May 22 at 22:28

## 2 Answers

1. Install the latest Lean 4 nightly through elan: in any bash-compatible shell, run:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly


On Windows, instead run in cmd

curl -O --location  https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1  powershell -f elan-init.ps1 --default-toolchain leanprover/lean4:nightly  del elan-init.ps1

2. Install VS Code.

3. Open VS Code and install the lean4 extension.

4. Create a new file with the extension .lean and add the following code:

#eval Lean.versionString


You should get a syntax-highlighted file with a "Lean Infoview" on the right that tells you the installed Lean version when placing your cursor on the last line.

5. You are set up! You can now also run lake init foo from the command line to create a package, followed by lake build to get an executable version of your Lean program.

###### Source: Quickstart - Lean Manual
• Thanks, this is helpful. Is there a simple way to use Lean without installing VS code though? Feb 8 at 18:13
• You can use Lean 4 from the command line like any other compiler, either via elan or from the release tarballs. There are Emacs and Neovim extensions as well. Currently there is no online version. Feb 8 at 18:20
• For posterity I would note that Lean changes rapidly and these instructions might not be correct in a few months time. For a future visitor, I'd recommend double checking that the instructions on leanprover.github.io are the same. Feb 9 at 5:32

Lean 4 has a separate repository.

(As an aside, I am not sure if this is the best place to ask such questions here that can be answered easily using a search engine while setting up the tone for the new community.)

• Search results can vary in reliability, and experience can be an asset. I guess we'll see how the Community judges such posts. Feb 8 at 19:47
• Please do try to not base your answers around hyperlinks, in case the page gets removed / edited. Feb 8 at 20:04
• IMHO there is no point in having the installation instructions duplicated here on the SE site as they could change/become outdated, while only the source repo/homepage is expected to keep that info updated. There is something to be said about what kind of knowledge is worth preserving and answering here especially if longevity is a concern. My larger point about the usefulness of the question remains. Feb 8 at 22:12
• I do think that questions whose best answer could be written as a primer on how to use a relevant tool should be welcome. They may help to develop the board as the place to check about proof assistant. Feb 9 at 18:51