Installing Lean 4 on Linux #
This document explains how to get started with Lean and mathlib on a generic Linux distribution (there is a specific page for Debian and derived distributions such as Ubuntu).
All commands below should be typed inside a terminal.
Lean itself doesn't depend on much infrastructure, but supporting tools needed by most users require
curl. So the first step is to get those.
The next step installs a small tool called
elanwhich will handle updating Lean according to the needs of your current project (hit Enter when a question is asked). It will live in
$HOME/.elanand add a line to
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
You will also need a code editor that has a Lean plugin. The recommended choice is Visual Studio Code which currently has the best Lean support. The alternatives are to use Emacs and its lean-mode or neovim and its lean.nvim extension.
- Install VS Code.
- Launch VS Code.
- Click on the extension icon
(or in older versions) in the side bar on the left edge of
the screen (or press ShiftCtrlX) and search for
- Select the
lean4extension (unique name
- Click "install" (In old versions of VS Code, you might need to click "reload" afterwards)
- Verify Lean is working, for example by saving a file
#eval 1+1. A green line should appear underneath
#eval 1+1, and hovering the mouse over it you should see
Lean Projects #
You can now read instructions about creating and working on Lean projects