Install

Manual Installation

We strongly advise using the recommended install procedure to install Lean. This guide provides detailed steps to perform a manual installation of Lean and VS Code using primarily the command prompt; however, these instructions will not work reliably for all environments, and you may be required to adapt them to your specific system.

This manual includes steps for installing VS Code. If you prefer to use an alternative editor, Neovim and the lean.nvim plugin are well-supported for Lean development. Other editor options include VSCodium and Cursor for which there is unofficial editor support via the Lean 4 extension on the Open VSX Registry. Please visit their respective websites for install procedures.

Install dependencies

Lean requires that both git and curl are installed. Open a terminal window and enter the following command to install both simultaneously (press Y when prompted, or include the -y flag on apt to skip prompts):

sudo apt install git curl

Next install elan, the Lean version manager, which will handle updating Lean according to individual project requirements. The following command will install elan to $HOME/.elan and will add a line to $HOME/.profile.

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Choose 1 to accept the default install option when prompted.

Make sure to add the relevant elan executables to path by running the following command:

source $HOME/.elan/env

Note: If you skip this last step and attempt to run lake later, your distribution may suggest trying to install lake via sudo apt install elan. You should ignore this suggestion and instead make sure to add elan to path as described above.

Install VS Code and the Lean 4 extension

The following commands will install VS Code and the Lean 4 extension:

wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868
sudo apt install ./code.deb
rm code.deb
code --install-extension leanprover.lean4

Note: If asked whether VS Code can install apt certificates for auto-updating, the recommended response is yes.

Note: Make sure to copy the complete code invocation (line 4) above, including the leanprover.lean4 part, as this is necessary to install the official Lean 4 extension for VS Code. If you do not include this part, the Lean extension will not be installed, and no warnings or errors will be issued.

You may now verify Lean is working by taking the following steps:

If not already open, open a new VS Code window by running the code command in the terminal (or by launching it from your applications menu)
Create a new file by pressing ctrl + N or by selecting File > New Text File
Save the file as test.lean by pressing ctrl + S or by selecting File > Save
Type #eval 1+1 into the newly saved file

Note: Steps 3 and 4 above will install a complete Lean toolchain in the background, represented by a small pop-up in the bottom right of the VS Code window. During this time the Lean InfoView, tooltips and other interactive Lean features in VS Code will be unavailable.

Once the toolchain install process is complete, if Lean has been installed correctly there should be no warnings nor errors. Hovering your mouse over parts of the eval statement will show tooltip menus with more information about the code.

Creating a new Lean project

All Lean code must live inside a Lean project (or package), which is a folder containing a git repository, either a lakefile.lean or lakefile.toml file containing dependency information about the project, and other necessary files. Lean projects are initialized and managed by lake, the Lean package manager that comes bundled with Lean.

Open a new terminal window in a folder location where you would like to create a new project subfolder: You may do so by opening a new terminal window and navigating to the desired folder using the cd command, or by navigating to the desired folder location using a file manager, then right-clicking and selecting Open in Terminal (or Open in Terminal Here).

Once in the terminal at the desired folder location, enter the following command to generate a new subfolder named my_lean_project and create the necessary Lean project files:

lake new my_lean_project

If you get an error message saying lake is an unknown command you may need to first type source ~/.profile or source ~/.bash_profile, then try the command above again.

You may now open the new project in VS Code by typing code my_lean_project into the terminal, or by launching the VS Code application, selecting File > Open Folder... and the my_lean_project folder. Select "Trust authors" when prompted by VS Code.

Creating a new Lean project depending on Mathlib

If you would instead like to create a new project depending on the Mathlib library the process is the same as above, but append math to the end of the lake command.

Once in the terminal at the desired folder location, enter the following command to generate a new subfolder named my_mathlib_project and create the necessary Lean and Mathlib project files:

lake +leanprover-community/mathlib4:lean-toolchain new my_mathlib_project math

If you get an error message saying lake is an unknown command you may need to first type source ~/.profile or source ~/.bash_profile, then try the command above again.

You may now open the new project in VS Code by typing code my_mathlib_project into the terminal, or by launching the VS Code application, selecting File > Open Folder... and the my_mathlib_project folder. Select "Trust authors" when prompted by VS Code.

Opening an existing Lean project

To clone an existing Lean project from a remote repository, navigate to the location where you would like to create the project subfolder and enter the following command:

git clone https://github.com/<repository owner>/<repository name>.git

Where <repository owner> is the GitHub username of the repository owner and <repository name> is the name of the repository you would like to clone. You can find both of these by navigating to the GitHub repository in a web browser and copying the URL from the address bar. Or you may simply clone the repository using the GitHub web interface by pressing the green "Code" button and selecting "Open with GitHub Desktop" or copying the URL and using your preferred Git client.

After cloning, navigate into the project folder and if the project is dependent on Mathlib run:

lake exe cache get

otherwise run:

lake update

Launch VS Code by typing code <repository name> into the terminal, or by opening VS Code and selecting File > Open Folder... and selecting the <repository name> folder. Select "Trust authors" when prompted by VS Code.

Updating Mathlib

elan will automatically keep Lean up to date, but you may need to update Mathlib manually. To do this, open a terminal window and enter the following commands:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update

It is recommended to then check that all files in your project repository still compile. Enter the following command:

lake exe mk_all && lake build

Install dependencies

Lean requires that both git and curl are installed. On macOS version 10.9 and higher Xcode Command Line Tools will install git automatically when the git command is activated. Open a terminal window and enter the following command:

git --version

This will either return the version of git installed, or prompt you to install git.

Install Homebrew and elan

Homebrew is a popular third-party package manager for macOS and provides a convenient method for installing VS Code. To install Homebrew enter the following command into a terminal window:

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

Next install elan, the Lean version manager, which will handle updating Lean according to individual project requirements. elan is stored in $HOME/.elan and adds a line to $HOME/.profile. Enter the following into the terminal window:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Choose 1 to accept the default install option when prompted.

Make sure to add the relevant elan executables to path by running the following command:

source $HOME/.elan/env

Install VS Code and the Lean 4 extension

The following commands will install VS Code via Homebrew and the official Lean 4 extension:

brew install --cask visual-studio-code
code --install-extension leanprover.lean4

You may now verify Lean is working by taking the following steps:

Open VS Code
Create a new file by pressing cmd + N or by selecting File > New Text File
Save the file as test.lean by pressing cmd + S or by selecting File > Save
Type #eval 1+1 into the newly saved file

Creating a new Lean project

Open a new terminal window in a folder location where you would like to create a new project subfolder: You may do so by opening a new terminal window and navigating to the desired folder using the cd command, or by navigating to the desired folder location using Finder, then right-clicking and selecting New Terminal at Folder.

Once in the terminal at the desired folder location, enter the following command to generate a new subfolder named my_lean_project and create the necessary Lean project files:

lake new my_lean_project

If you get an error message saying lake is an unknown command you may need to first type source ~/.profile or source ~/.bash_profile, then try the command above again.

Creating a new Lean project depending on Mathlib

If you would instead like to create a new project depending on the Mathlib library the process is the same as above, but append math to the end of the lake command.

Open a new terminal window in a folder location where you would like to create a new project subfolder: You may do so by opening a new terminal window and navigating to the desired folder using the cd command, or by navigating to the desired folder location using Finder, then right-clicking and selecting New Terminal at Folder.

Once in the terminal at the desired folder location, enter the following command to generate a new subfolder named my_mathlib_project and create the necessary Lean and Mathlib project files:

lake +leanprover-community/mathlib4:lean-toolchain new my_mathlib_project math

If you get an error message saying lake is an unknown command you may need to first type source ~/.profile or source ~/.bash_profile, then try the command above again.

Opening an existing Lean project

To clone an existing Lean project from a remote repository, navigate to the location where you would like to create the project subfolder and enter the following command:

git clone https://github.com/<repository owner>/<repository name>.git

After cloning, navigate into the project folder and if the project is dependent on Mathlib run:

lake exe cache get

otherwise run:

lake update

Updating Mathlib

elan will automatically keep Lean up to date, but you may need to update Mathlib manually. To do this, open a terminal window and enter the following commands:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update

It is recommended to then check that all files in your project repository still compile. Enter the following command:

lake exe mk_all && lake build

Install VS Code

The recommended approach to developing in Lean is with VS Code. Download the installer from the VS Code website then run it and complete the setup wizard. Make sure that both "Register Code as an editor for supported file types" and "Add to PATH" are checked in the installer options.

Install dependencies

Open a new Command Prompt (i.e. terminal) window and ensure both Git and curl are installed: Navigate to the Start menu and select "Windows System > Command Prompt" or click on the Search icon (magnifying glass), type "cmd" into the search bar and choose "Command Prompt" from the results. Once the Command Prompt window opens, enter the following commands:

git --version
curl --version

If either command returns an error you will need to install the relevant software via their respective websites.

Note: If you install Git, it is recommended that you choose Visual Studio Code as the default editor for Git. Accept all other default options presented in the Git installer.

After completing installs for either Git or curl, you must close and reopen the terminal window for the changes to take effect.

Install elan

elan is the Lean version manager. Open a new terminal window and enter the following command to download the elan-init.ps1 script via curl:

curl -O   --location https://elan.lean-lang.org/elan-init.ps1

Next, run the elan-init.ps1 script to install elan:

powershell -ExecutionPolicy Bypass -f elan-init.ps1

When prompted, choose "1" to proceed with the default installation.

Finally, delete the elan-init.ps1 file:

del elan-init.ps1

And close the terminal window (or type exit).

Install the VS Code Lean 4 extension

Open VS Code and navigate to the Extensions view (Ctrl + Shift + X). Install the Lean 4 extension by searching for lean4 in the extension search bar and clicking Install on the official Lean 4 extension authored by leanprover. Choose "Trust Publisher & Install", if prompted. Once the install is complete the Lean 4 Setup guide will will open. This guide covers many of the steps in this manual installation guide.

You may now verify Lean is working by taking the following steps:

Create a new file by pressing ctrl + N or by selecting File > New Text File
Save the file as test.lean by pressing ctrl + S or by selecting File > Save
Type #eval 1+1 into the newly saved file

Note: Steps 2 and 3 above will install a complete Lean toolchain in the background, represented by a small pop-up in the bottom right of the VS Code window. During this time the Lean InfoView, tooltips and other interactive Lean features in VS Code will be unavailable.

If Lean has been installed correctly you should see no warnings or errors. Hovering your mouse over parts of the statement will show tooltip menus with more information about the code.

Creating a new Lean project

Open a new terminal window in a folder location where you would like to create a new project subfolder: You may do so by opening a new terminal window and navigating to the desired folder using the cd command, or by right-clicking on the desired folder location in Explorer and selecting Open in Terminal (or Open PowerShell window here).

Once in the terminal at the desired folder location, enter the following command to generate a new subfolder named my_lean_project and create the necessary Lean project files:

lake new my_lean_project

Creating a new Lean project depending on Mathlib

If you would instead like to create a new project depending on the Mathlib library the process is the same as above, but append math to the end of the lake command.

Open a new terminal window in a folder location where you would like to create a new project subfolder: You may do so by opening a new terminal window and navigating to the desired folder using the cd command, or by right-clicking on the desired folder location in Explorer and selecting Open in Terminal (or Open PowerShell window here).

Once in the terminal at the desired folder location, enter the following command to generate a new subfolder named my_mathlib_project and create the necessary Lean and Mathlib project files:

lake +leanprover-community/mathlib4:lean-toolchain new my_mathlib_project math

Note: If this is the first time you are creating a Lean project depending on Mathlib there may be an extended wait time while Mathlib is downloaded.

Opening an existing Lean project

To clone an existing Lean project from a remote repository, navigate to the location where you would like to create the project subfolder and enter the following command:

git clone https://github.com/<repository owner>/<repository name>.git

Where <repository owner> is the GitHub username of the repository owner and <repository name> is the name of the repository you would like to clone. You can find both of these by navigating to the repository in a web browser on GitHub, and copying the URL from the address bar. Or you may simply clone the repository using the GitHub web interface by pressing the green "Code" button and selecting "Open with GitHub Desktop" or copying the URL and using your preferred Git client.

After cloning, navigate into the project folder and if the project is dependent on Mathlib run:

lake exe cache get

otherwise run:

lake update

Updating Mathlib

elan will automatically keep Lean up to date, but you may need to update Mathlib manually. To do this, open a terminal window and enter the following commands:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update

It is recommended to then check that all files in your project repository still compile. Enter the following command:

lake exe mk_all && lake build