Documentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt
Use this file to discover all available pages before exploring further.
Lean 4 is distributed through elan, the official Lean toolchain version manager. Elan handles downloading, caching, and switching between Lean releases, so you never need to manage binaries by hand. This page covers installing elan on every supported platform, setting up your editor, and managing toolchains day-to-day.
Install elan
Run the elan installer script:curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
- Download the elan binary to
~/.elan/bin/
- Add
~/.elan/bin to your PATH in ~/.profile (or ~/.bash_profile, ~/.zshenv, etc.)
- Optionally download a default Lean toolchain
Restart your shell or run: Option 1 — curl installer (recommended):curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source ~/.elan/env
brew install elan-init
elan-init
The Homebrew formula installs elan but does not run the initialiser automatically. After brew install, run elan-init once to set up your shell and download a default toolchain.
Open PowerShell and run:curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -f elan-init.ps1
del elan-init.ps1
%USERPROFILE%\.elan\bin to your PATH. Restart your terminal (or open a new PowerShell window) before continuing.On Windows you must enable “Developer Mode” or run as Administrator the first time, because elan creates symbolic links in its bin directory.
Verify the Installation
lean --version
# Lean (version 4.x.x, commit xxxxxxxx, Release)
lake --version
# Lake version x.x.x (Lean version 4.x.x)
~/.elan/bin is in your PATH.
Editor Support
VS Code (Recommended)
Install the official extension from the VS Code marketplace:
- Extension ID:
leanprover.lean4
- Name: Lean 4
# Install via the command line
code --install-extension leanprover.lean4
ext install leanprover.lean4
- Real-time type checking and error messages
- Lean Infoview panel showing tactic goal states
- Hover for types and docstrings
- Go-to-definition (F12) across packages
- Breadcrumbs, outline, and find-all-references
Open the Lean Infoview panel with Ctrl+Shift+Enter (or via the command palette: “Lean 4: Open Infoview”). Place your cursor inside any by block to see the live proof state.
Emacs
Install lean4-mode from MELPA:
;; In your init.el / .emacs
(use-package lean4-mode
:ensure t
:commands lean4-mode)
straight.el:
(straight-use-package 'lean4-mode)
elan to locate the correct lean binary automatically. Make sure ~/.elan/bin is in Emacs’s exec-path, or set:
(setq lean4-rootdir "~/.elan")
Neovim
Use your plugin manager to install lean.nvim:
{
"Julian/lean.nvim",
dependencies = {
"neovim/nvim-lspconfig",
"nvim-lua/plenary.nvim",
},
opts = {
lsp = { on_attach = on_attach },
mappings = true,
},
}
use {
"Julian/lean.nvim",
requires = {
"neovim/nvim-lspconfig",
"nvim-lua/plenary.nvim",
},
config = function()
require("lean").setup { mappings = true }
end
}
:LeanInfoviewToggle.
A Minimal Lean 4 File
Once installed, verify everything works end-to-end by running lean directly on a file:
-- Save as hello.lean and run: lean --run hello.lean
def main : IO Unit :=
IO.println "Lean 4 is installed and working!"
lean --run hello.lean
# Lean 4 is installed and working!
# Install the stable release
elan toolchain install leanprover/lean4:stable
# Install a specific version
elan toolchain install leanprover/lean4:v4.14.0
# Install the nightly channel
elan toolchain install leanprover/lean4:nightly
Set the Global Default
elan default leanprover/lean4:stable
lean-toolchain file is found in the current directory tree).
elan toolchain uninstall leanprover/lean4:v4.12.0
lake new creates a project, it generates a lean-toolchain file in the project root:
Elan reads this file and automatically uses the pinned toolchain for all lean, lake, and related commands run inside that directory. This ensures every contributor uses the same Lean version.
# Override the toolchain for a single command
lean +leanprover/lean4:v4.13.0 --version
# Show which lean binary elan resolves to
elan which lean
You can also use a GitHub fork toolchain in lean-toolchain by writing <github-user>/lean4:<tag>. This is useful for testing against pre-release builds.
Building Lean from Source
If you need to build Lean itself (for contributing or debugging), see the official build instructions in the repository. Building from source requires CMake, a C++ compiler, and an existing Lean stage-0 binary.
Building from source is not required for using Lean 4. Unless you are contributing to the compiler itself, install via elan.
