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

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/"))
(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:

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

Testing your installation

To test the installation of Lean and mathlib, create a file with the following code, which loads a library from mathlib:

import data.real.basic

This should return no errors.


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

:PlugInstall

You will also need to install lean-language-serverAUR, which is available from the AUR.

Next, create a configuration file at $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/.