Installing Lean and mathlib 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
python3(on Debian and Ubuntu also
python3-venv). 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. The alternative is to use Emacs, and its lean-mode.
- 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
leanextension (unique name
jroesch.lean). There is also a
lean4extension, but that one does not work with mathlib.
- 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
Then we install a small tool called
leanprojectthat which will handle updating mathlib according to the needs of your current project. We use pipx to perform the installation.
python3 -m pip install --user pipx python3 -m pipx ensurepath source ~/.profile pipx install mathlibtools
Lean Projects #
You can now read instructions about creating and working on Lean projects