by Microsoft Research
Open source theorem prover and programming language

Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

``````-- This is a comment
section forall_or_elim
theorem forall_or_elim : ∀ (α : Type) (p q : α → Prop), ( ∀ x : α, p x ∧ q x ) → ∀ y : α, p y :=
assume α : Type,
assume p q : α → Prop,
assume h : ( ∀ x : α, p x ∧ q x ),
assume y : α,
show p y, from (h y).left
end forall_or_elim

section transitivity
universe u
variables (α : Type u) (r : α → α → Prop)
variable  trans_r : ∀ {x y z}, r x y → r y z → r x z

variables (a b c : α)
variables (hab : r a b) (hbc : r b c)

#check trans_r
#check trans_r hab
#check trans_r hab hbc
end transitivity

section and_comm
lemma and_comm_one_way : Π a b : Prop, a ∧ b → b ∧ a :=
λ (a b : Prop) (hab : a ∧ b) , and.intro (and.right hab) (and.left hab)

theorem and_comm_full_1 : Π a b : Prop , a ∧ b ↔ b ∧ a :=
λ (a b : Prop), iff.intro (and_comm_one_way a b) (and_comm_one_way b a)

theorem and_comm_full_2 : Π a b : Prop , a ∧ b ↔ b ∧ a :=
assume a b : Prop,
let
forward := and_comm_one_way a b,
back := and_comm_one_way b a
in
iff.intro forward back
end and_comm

-- The following is taken from https://leanprover.github.io/introduction_to_lean/
section sort
universe u
parameters {α : Type u} (r : α → α → Prop) [decidable_rel r]
local infix `≼` : 50 := r

def ordered_insert (a : α) : list α → list α
| []       := [a]
| (b :: l) := if a ≼ b then a :: (b :: l) else b :: ordered_insert l

def insertion_sort : list α → list α
| []       := []
| (b :: l) := ordered_insert b (insertion_sort l)
end sort

#eval insertion_sort (λ m n : ℕ, m ≤ n) [5, 27, 221, 95, 17, 43, 7, 2, 98, 567, 23, 12]``````
Information updated 04/18/19
Note: This entry has not yet been moderated.