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.

Note that the following installation steps are optimized for Ubuntu. Some steps may differ for other distributions.

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 the PATH of your current terminal 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:

  1. 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)

  2. Create a new file by pressing ctrl + N or by selecting File > New Text File

  3. Save the file as Test.lean by pressing ctrl + S or by selecting File > Save. (This step 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.)

  4. Type #eval 1+1 into the newly saved file

Once the toolchain install process is complete, if Lean has been installed correctly there should be no warnings nor errors. Hovering your mouse over the underlined part of the eval statement will show a tooltip with the evaluated result.

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 MyLeanProject and create the necessary Lean project files:

lake new MyLeanProject

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.

Navigate to the MyLeanProject directory and build the project:

cd MyLeanProject && lake build

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

Creating a new Lean project depending on Mathlib

The following steps will generate a new Lean project depending on the Mathlib library.

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 MyMathlibProject and create the necessary Lean and Mathlib project files:

lake +leanprover-community/mathlib4:lean-toolchain new MyMathlibProject 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.

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.

Navigate to the MyLeanProject directory and build the project:

cd MyLeanProject && lake build

You may now open the new project in VS Code by typing code . into the terminal, or by launching the VS Code application, selecting File > Open Folder... and the MyMathlibProject 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, or is Mathlib itself, run

lake exe cache get

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, if your project depends on it. 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

Note: that Homebrew does not provide auto-updates, so installing VS Code via Homebrew requires additional long-term maintenance: In order to keep VS Code updated you must periodically run brew update via a terminal window to ensure that VS Code (and any other Homebrew installed applications) are updated.

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

  1. Open VS Code.

  2. Create a new file by pressing cmd + N or by selecting File > New Text File.

  3. Save the file as Test.lean by pressing cmd + S or by selecting File > Save. (This step 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).

  4. Type #eval 1+1 into the newly saved file.

Once the toolchain install process is complete, if Lean has been installed correctly there should be no warnings nor errors. Hovering your mouse over the underlined part of the eval statement will show a tooltip with the evaluated result.

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 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 MyLeanProject and create the necessary Lean project files:

lake new MyLeanProject

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.

Navigate to the MyLeanProject directory and build the project:

cd MyLeanProject && lake build

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

Creating a new Lean project depending on Mathlib

The following steps will generate a new Lean project depending on the Mathlib library.

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 MyMathlibProject and create the necessary Lean and Mathlib project files:

lake +leanprover-community/mathlib4:lean-toolchain new MyMathlibProject 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.

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.

Navigate to the MyLeanProject directory and build the project:

cd MyLeanProject && lake build

You may now open the new project in VS Code by typing code . into the terminal, or by launching the VS Code application, selecting File > Open Folder... and the MyMathlibProject 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, or is Mathlib itself, run

lake exe cache get

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, if your project depends on it. 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:

  1. Create a new file by pressing ctrl + N or by selecting File > New Text File.

  2. Save the file as est.lean by pressing ctrl + S or by selecting File > Save. (This step 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.)

  3. Type #eval 1+1 into the newly saved file.

If Lean has been installed correctly you should see no warnings or errors. Hovering your mouse over the underlined part of the eval statement will show a tooltip with the evaluated result.

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 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 MyLeanProject and create the necessary Lean project files:

lake new MyLeanProject

Navigate to the MyLeanProject directory and build the project:

cd MyLeanProject && lake build

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

Creating a new Lean project depending on Mathlib

The following steps will generate a new Lean project depending on the Mathlib library.

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 MyMathlibProject and create the necessary Lean and Mathlib project files:

lake +leanprover-community/mathlib4:lean-toolchain new MyMathlibProject 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.

Navigate to the MyLeanProject directory and build the project:

cd MyLeanProject && lake build

You may now open the new project in VS Code by typing code . into the terminal, or by launching the VS Code application, selecting File > Open Folder... and the MyMathlibProject 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 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, or is Mathlib itself, run:

lake exe cache get

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, if your project depends on it. 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