by Microsoft Research
Open source theorem prover and programming language

From https://leanprover.github.io/about/

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.
View Comments