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 selectingFile > New Text File
-
Save the file as
test.lean
by pressingctrl + S
or by selectingFile > 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.
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_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 selectingFile > New Text File
-
Save the file as
test.lean
by pressingcmd + S
or by selectingFile > 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 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.
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.
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.
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 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 selectingFile > New Text File
-
Save the file as
test.lean
by pressingctrl + S
or by selectingFile > 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
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 my_lean_project
and create the necessary Lean project files:
lake new my_lean_project
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.
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.
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 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
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