Lean (proof assistant)

Initially launched by Leonardo de Moura at Microsoft Research in 2013.[1]

The Lean 3 was implemented as a virtual machine which made it less efficient due to overhead associated with interpretation making it less competitive with other proof assistants such as Coq.

In 2021 the Lean 4 was released with a reimplementation of the Lean theorem prover capable to produces C code which is then compiled, enabling the development of efficient domain-specific automation.[2] Another improvement over previous version was ability to avoid touching C++ code in order to obtain certain features.

Lean 4 is not backwards-compatible with Lean 3.[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

Lean has gotten attention from mathematicians Thomas Hales[8] and Kevin Buzzard.[9] Hales is using it for his project, Formal Abstracts.[10] Buzzard uses it for the Xena project.[11] 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.[12]

• Dependent type
• List of proof assistants
• mimalloc
• Type theory
• Focused Research Organization

• Lean Website
• Lean Community Website
• Lean FRO
• The Natural Number Game- An interactive tutorial to learn lean