Lean is a proof assistant and programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. It was made by Microsoft Research.
History
Initially launched by Leonardo de Moura at Microsoft Research in 2013.
Lean 3 was implemented as a virtual machine, which made it less efficient due to overhead associated with interpretation, making it less competitive compared to other proof assistants such as Coq.
In 2021, Lean 4 was released with a reimplementation of the Lean theorem prover capable of producing C code which is then compiled, enabling the development of efficient domain-specific automation. Another improvement compared to the previous version was ability to avoid touching C++ code in order to obtain certain features.
Lean 4 is not backwards-compatible with Lean 3.
Overview
Libraries
In 2017, the project adopted a user-maintained library mathlib with the goal to digitize pure mathematics research. As of November 2023, mathlib had formalized over 127,000 theorems and 70,000 definitions in Lean.
Editors integration
Lean integrates with:
Visual Studio Code
Neovim
Emacs
Interfacing is done via a client-extension and Language Server Protocol server.
It has native support for Unicode symbols, which can be typed using LaTeX-like sequences, such as "\times" for "×". Lean can also be compiled to JavaScript and accessed in a web browser and has extensive support for meta-programming.
Examples (Lean 3)
The natural numbers can be defined as an inductive type. This definition is based on the Peano axioms and states that every natural number is either zero or the successor of some other natural number. inductive nat : Type | zero : nat | succ : nat → nat
Addition of natural numbers can be defined recursively, using pattern matching. definition add : nat → nat → nat | n zero := n | n (succ m) := succ (add n m)
This is a simple proof in lean in term mode. theorem and_swap : p ∧ q → q ∧ p := assume h1 : p ∧ q, ⟨h1.right, h1.left⟩
This same proof can be accomplished using tactics. theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := begin assume h : (p ∧ q), -- assume p ∧ q is true cases h, -- extract the individual propositions from the conjunction split, -- split the goal conjunction into two cases: prove p and prove q separately repeat { assumption } end
Usage
Lean has gotten attention from mathematicians Thomas Hales and Kevin Buzzard. Hales is using it for his project, Formal Abstracts. Buzzard uses it for the Xena project. One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean.
In 2021, Lean was used to formalize a new proof by Peter Scholze in the area of condensed mathematics, proving that Lean can be useful at the cutting edge of mathematical research.