Lean logo2.svg
ParadigmFunctional programming, Imperative programming
DeveloperMicrosoft Research
First appeared2013; 9 years ago (2013)
Stable release
3.48.0 / 17 September 2022; 3 months ago (2022-09-17)
Preview release
4.0.0-m5 / 7 August 2022; 4 months ago (2022-08-07)
Typing disciplineStatic, strong, inferred
Implementation languageC++, Lean
LicenseApache License 2.0
WebsiteStable: leanprover-community.github.io
Preview: leanprover.github.io
Influenced by

Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types.

The Lean project is an open source project, hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013.[1]

Lean has an interface that differentiates it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols. (These can be typed using LaTeX-like sequences, such as "\times" for "×".) Lean also has an extensive support for meta-programming.

Lean has gotten attention from mathematicians Thomas Hales[2] and Kevin Buzzard.[3] Hales is using it for his project, Formal Abstracts.[4] Buzzard uses it for the Xena project.[5] 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.


Here is how the natural numbers are defined in Lean.

inductive nat : Type
| zero : nat
| succ : nat  nat

Here is the addition operation defined for natural numbers.

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 :=
    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 }

See also


  1. ^ "Lean Prover About Page".
  2. ^ Hales, Thomas (18 September 2018). "A Review of the Lean Theorem Prover". Retrieved 6 October 2020.
  3. ^ Buzzard, Kevin. "The Future of Mathematics?" (PDF). Retrieved 6 October 2020.
  4. ^ "Formal Abstracts". Github.
  5. ^ "What is the Xena project?". Xena. 8 May 2019.