Lean (proof assistant)


Lean is a theorem prover and programming language. It is based on the Calculus of Constructions with inductive types.
Lean has a number of features that differentiate 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. Lean uses its own language for meta-programming. So, if the user wants to write a function that automatically proves some theorems, they write that function in Lean's own language.
Lean has gotten attention from mathematicians Thomas Hales and Kevin Buzzard. Hales is using it for his project, . Buzzard uses it for the . 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.

Examples

Here is how the natural numbers are defined in Lean.

inductive nat : Type

Here is the addition operation defined for natural numbers.

definition add : nat → nat → nat

This is a simple proof in learn 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 → q ∧ p :=
begin
assume h :, -- 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
end