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

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 the elan-leanAUR package.

Note: The rest of these instructions explain how to install lean, but if you wish to contribute to an existing project, such as mathlib, the lean installation will be handled automatically, and you can skip ahead to the Project Management section

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. For instance, the build of lean that mathlib4 is using can be found in the file [1]. To install the desired build, run 

$ elan toolchain install leanprover/lean4:build

where build should be replaced with the desired 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 build can be overridden for a given project by cd-ing to the project directory and creating a file 

lean-toolchain
build

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


Lean 3 via the AUR

Install lean-community-binAUR or lean-communityAUR.

To install mathlib, you must first install python-mathlibtoolsAUR, 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.

Project Management

In this section, we will describe how to create and contribute to Lean 4 projects, including mathlib4.

Structure of a project

A Lean 4 project will contain several files that are used to manage the project.

  • lakefile.lean: contains information on how to build the project, as well as a list of dependencies.
  • lean-toolchain: a single-line file specifying the build to be used for the project.
  • lake-manifest.json: an automatically generated file that contains information on the specific version of each of the installed dependencies. If you have a lake-manifest.json file, running lake update will download the versions of the dependencies specified in lake-manifest.json. This is useful to avoid incompatible dependency versions.
  • .lake (or, in earlier versions of lean 4, lake-packages): this is where dependencies are installed.
  • build: directory where built lean files are stored.
  • Lean files, containing the lean code.

Creating a project

To create a project, install elan and a lean build, as described in the Lean 4 using elan section above.

Note: As of this writing, the stable build does not include lake, so to run the code below, you will need to install a newer build, such as v4.3.0-rc2, and make it the default

Next, run 

$ lake new path/to/project

This will create a default lakefile.lean and lean-toolchain file.

This will not download mathlib, which you may want to do. Mathlib is the official math library of the Lean project, and contains a lot of definitions, lemmas and theorems that you may need for your project. If you want to add mathlib to your project, you must add it as a dependency in the lakefile. See below for details.


Managing a project

If you are working with an existing project, for instance one you have downloaded from the internet (e.g. github), you do not need to install lean separately, as long as you have elan installed, see the Lean 4 using elan section above. As long as the appropriate lean-toolchain file is present in the project, you can simply run 

$ lake update

which will download the required version of Lean, as well as all the dependencies for the project.

Dependencies can be added by editing the lakefile.lean file. For example, to add mathlib as a dependency, add the line 

lakefile.lean
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

to lakefile.lean. Next run 

$ lake update

to download mathlib, and 

$ lake exe cache get

to download the pre-compiled library (see section Caches and oleans below).

Contributing to Mathlib

If you wish to participate in the ongoing effort to formalize much of mathematics, you may want to make contributions to Mathlib, which is the official math library of the Lean project.

To do so, you will first need to download mathlib: 

$ git clone https://github.com/leanprover-community/mathlib4.git

and cd to the downloaded directly and run 

$ lake update
$ lake exe cache get

If you wish to submit your work, you will need to get a branch on the mathlib Git server, and submit a pull request. To get a branch, contact the community on the leanprover Zulip chat, introduce yourself and your project, and ask for a branch.

Automatically generating documentation

It is possible to automatically generate documentation, in the same style as the mathlib documentation. This is done using the doc-gen4 package. To install it, add it to your lakefile.lean: 

lakefile.lean
meta if get_config? env = some "dev" then require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"@"main"

(the "dev" part of the code ensures that the doc can only be built when running lake with -Kenv=dev, as below, so as to avoid generating the doc when merely trying to build the package) and download it: 

$ lake -Kenv=dev update

The documentation can be generated using 

$ lake -Kenv=dev build NameOfProject:docs

where NameOfProject should be replaced by the name of your project. This will generate the documentation and place it in the build/doc directory. You can then navigate through the documentation by opening build/doc/index.html in a browser.

Note: opening the documentation files locally using a browser is not officially supported. Instead, it is recommended to start an http server, for instance with python -m http.server
Note: doc-gen4 assumes the project builds properly. If there are any errors at build time, the documentation will not be functional. Make sure that lake build exits without errors before generating the documentation

The documentation also includes a search function. To search for a term in the documentation, use 

file:///path/to/doc/find/index.html?pattern='search_term'#doc

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: 

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

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.

Keybindings

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: 

.emacs
(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: 

.emacs
(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: 

init.vim
call plug#begin()

...

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

...

call plug#end()

open nvim, and type 

:PlugInstall

If you are using lean 3, you will also need to install lean-language-serverAUR. (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: 

$XDG_CONFIG_HOME/nvim/plugin/lean.lua
require('lean').setup{
 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 

$ 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 ./
$ lake update

Lean documentation

A good resource to learn theorem proving in lean 4 is [2]. Of particular note, a succinct "cheatsheet" for useful commands for theorem proving in lean 4 is available from [3].

The documentation for mathlib in lean 4 is available at [4].

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.