Lean Theorem Prover

From ArchWiki

The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura at Microsoft Research. The Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant.

Installation of lean and mathlib

Lean 4 using elan

elan is a tool to manage installs of the lean theorem prover. It facilitates maintaining several concurrent versions of lean. In addition, as lean 4 is under heavy development, using it often requires installing nightly builds, which is made easy using elan. elan installs lean in subdirectories of $HOME/.elan/toolchains, and does not require root access.

Install elan-leanAUR from the AUR. To install the latest stable version of lean 4, use

$ elan toolchain install leanprover/lean4:stable

However, many applications (including using mathlib4) require development versions of lean4, which can be installed using

$ elan toolchain install leanprover/lean4:nightly-yyyy-mm-dd

where yyyy-mm-dd should be replaced with the desired date of the nightly build.

The installed versions of lean can be listed with

$ elan show

and a default can be selected with

$ elan default <build>

When using lean 4, the default can be overridden for a given project by cd-ing to the project directory and creating a file


(replace <build> with the appropriate build identifier. To get the path to an executable in the current lean build, use

$ elan which <name_of_executable>

To download mathlib, create a project:

$ $(elan which lake) new <path/to/project> math

which will create a new directory at path/to/project. Inside it will be a file named lakefile.lean which lists the dependencies of the project. Specifying math in the command above will make mathlib a dependency. To download mathlib, run

$ $(elan which lake) update
$ $(elan which lake) exe cache get

Lean 3 via the AUR

Install lean-community-binAUR or lean-communityAUR from the AUR.

To install mathlib, you must first install python-mathlibtoolsAUR from the AUR, which will install 'leanproject'.

Note: python-mathlibtoolsAUR will not install mathlib, just the tools needed to download mathlib.

To install mathlib, you must create a lean project:

$ cd /path/to/project
$ leanproject new name_of_project

which will download mathlib to /path/to/project/name_of_project/_target/deps/mathlib.

Text editors

Using Lean with Emacs

Install lean-mode

To use lean with emacs, you must install the lean-mode package. To install it from the MELPA repository, add:

(require 'package)
(add-to-list 'package-archives
  '("melpa" . "https://melpa.org/packages/"))

to your Emacs configuration file open emacs, and type

M-x package-install RET
lean-mode RET

Opening a file in emacs with the .lean extension will now automatically be opened in Lean mode.


A list of keybindings is available at https://github.com/leanprover/lean-mode.

Automatic unicode input

Lean uses unicode symbols as part of its language. lean-mode can handle this input easily by translating standard text to unicode characters, for instance, typing \R will resolve to the unicode character . To do this, the Lean input method needs to be selected. This can be done automatically by adding the following to your Emacs configuration file:

(add-hook 'lean-mode-hook
  (lambda () (set-input-method "Lean")))

Viewing goal in separate buffer

Keeping track of the "goal" is very useful when writing proofs in Lean. The goal can be seen directly in emacs using the C-c C-b keybinding, which will open a new buffer in which the goal is shown. This buffer can also be opened automatically when editing a .lean file by adding:

(add-hook 'lean-mode-hook 'lean-toggle-show-goal)

to your Emacs configuration file.

Using Lean with Neovim

Install lean.nvim

To use lean with Neovim, you must install the lean.nvim plugin. This can be done easily using vim-plug byadding the following to your Neovim Configuration file:

call plug#begin() 


Plug 'Julian/lean.nvim'
Plug 'neovim/nvim-lspconfig'
Plug 'nvim-lua/plenary.nvim'


call plug#end()

open nvim, and type


If you are using lean 3, you will also need to install lean-language-serverAUR, which is available from the AUR. (The language server is built into lean 4, so it is not necessary for lean 4 installs).

Next, create a configuration file at $XDG_CONFIG_HOME/nvim/plugin/lean.lua:

 abbreviations = { builtin = true },
 mappings = true,

abbreviatons enables abbreviating unicode characters, and mappings enables a number of useful keybindings, see https://github.com/Julian/lean.nvim/ for a full list. More configuration options are available at https://github.com/Julian/lean.nvim/.

Tips and tricks

Caches and oleans

In order to use the theorems and lemmas in mathlib, mathlib needs to be built (i.e. compiled). This is a long process. To avoid this, the mathlib community provides a repository of pre-compiled mathlib files (also called "oleans"). To download them using lean 4, use

$ $(elan which lake) exe cache get

and using lean 3, use

$ leanproject get-cache
Note: In order for the oleans to be used, they have to have been pre-compiled with the same version of lean (i.e. the same nightly build if you are using those) as is used by the project.

When using lean 4, a simple way of ensuring that the project always uses the same version as mathlib is to link the mathlib lean-toolchain file to the project directory:

$ ln -sf lake-packages/mathlib/lean-toolchain ./
$ $(elan which lake) update

Lean documentation

As of this writing, the documentation for lean and mathlib is incomplete, and difficult to find (this is especially true of lean 4). There is some documentation for lean 4 available at [1] and for lean 3 at [2]. Of particular note, a succinct "cheatsheet" for useful commands for theorem proving in lean 4 is available from [3] and for lean 3 from [4].

The documentation for mathlib in lean 4 is available at [5], and for lean 3 at [6].

Since the documentation is still rather sparse, it is often more productive to address questions to the lean community directly. The most popular forum for this is the leanprover Zulip chat.