Controlled installation of Lean and mathlib on MacOS #
This document explains a more controlled installation procedure for Lean and mathlib on MacOS. There is a quicker way described in the main install page but it requires more trust.
If you get stuck, please come to the chat room to ask for assistance.
We'll need to set up Lean, an editor that knows about Lean, and
mathlib (the standard library).
Rather than installing Lean directly, we'll install a small program called
automatically provides the correct version of Lean on a per-project basis. This is recommended for
We'll also install
which, amongst other things, let you download compiled binaries for
elan and mathlib supporting tools #
Install Homebrew if you do not already have it installed.
brew install elan-init mathlibtoolsin a terminal window to install
elan, as well as the supporting toolset for working with
Note that Homebrew also contains a formula named simply
lean, but that it installs a fixed version of Lean, rather than one provisioned with
elanas per the above. Using this formula is as mentioned not recommended.
elanto install the latest stable version of
elan toolchain install stable. You can also set the newly-installed version to be the default version of
leanyou get when running outside of a project (discussed below) by running
elan default stable.
Installing and configuring an editor #
There are two editors you can use with Lean, VS Code and emacs. This document describes using VS Code (for emacs, look at https://github.com/leanprover/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 ⇧ Shift⌘ CommandX) 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
Lean Projects #
You can now read instructions about creating and working on Lean projects
Aside: Migrating From Older Installations #
Older versions of this installation guide recommended a different method
of installation, involving manually installing
elan directly from
pipx and using that to install
If you have installed things this way, you can migrate to the newer installation mechanism by running:
pipx uninstall mathlibtools && brew install mathlibtools
elan self uninstall && brew install elan-init