The Lean Theorem Prover

Many thanks to

• Cody Roux
• Georges Gonthier
• Grant Passmore
• Nikhil Swamy
• Assia Mahboubi
• Bas Spitters
• Steve Awodey
• Ulrik Buchholtz
• Tom Ball
• Parikshit Khanna

Introduction: Lean

• New open source theorem prover
• Platform for
• Software verification & development
• Formalized mathematics
• Education (mathematics, logic, computer science)
• Synthesis (proofs & programs)
• de Bruijn's Principle: small trusted kernel
• Expressive logic based on dependent type theory
• Partial constructions: automation fills the "holes"

Main Goal

Lean aims to bring two worlds together

• An interactive theorem prover with powerful automation
• An automated reasoning tool that
• produces (detailed) proofs,
• has a rich language,
• can be used interactively, and
• is built on a verified mathematical library

Secondary Goals

• Minimalist and high-performace kernel
• Experiment with different flavors of type theory
• Proof irrelevant vs Proof relevant
• Impredicative vs Predicative
• Higher Inductive Types
• Quotient Types
• Observational Type Theory
• Have Fun

What is new?

• Poweful elaboration engine that can handle
• Higher-order unification
• Definitional reductions
• Coercions
• Type classes
• Tactics

"By relieving the brain of all unnecessary work, a good notation sets it free to concentrate on more advanced problems, and in effect increases the mental power of the race." – A. N. Whitehead

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• It does not contain
• Termination checker
• Fixpoint operators
• Pattern matching
• Module management
• Reference type checker
• Implemented by Daniel Selsam
• < 2000 lines of Haskell code
• Code is easy to read and understand
• Type check the whole standard library (35K lines) under 2 mins
• All Lean files can be exported in a very simple format

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
• Process theorems in parallel
• Execute/try tactics (automation) in parallel

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
• Fast incremental compilation

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
• Fast incremental compilation
• Support for mixed declarative and tactic proof style

What is new?

• Poweful elaboration engine that can handle
• Small trusted kernel
• Multi-core support
• Fast incremental compilation
• Support for mixed declarative and tactic proof style
• Quotient types

Two official libraries

• Standard
• Proof irrelevant and impredicative Prop
• Smooth transition to classical logic
• Inductive Families
• Quotient Types
• HoTT
• Proof relevant and no impredicative Prop
• Univalence axiom
• Inductive Families
• HIT
• Easy to implement experimental versions, Example: Steve Awodey asked for proof relevant and impredicative universe

Recursive equations

• Recursors are inconvenient to use.
• Compiler from recursive equations into recursors.
• Two compilation strategies: structural and well-founded recursion
definition fib : nat → nat | fib 0 := 1 | fib 1 := 1 | fib (a+2) := fib (a+1) + fib a example (a : nat) : fib (a+2) = fib (a+1) + fib a := rfl

Recursive equations

• Dependent pattern matching
definition map {A B C : Type} (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n | map nil nil := nil | map (a::va) (b::vb) := f a b :: map va vb definition zip {A B : Type} : Π {n}, vector A n → vector B n → vector (A × B) n | zip nil nil := nil | zip (a::va) (b::vb) := (a, b) :: zip va vb

import algebra.category open eq.ops category functor natural_transformation variables {ob₁ ob₂ : Type} {C : category ob₁} {D : category ob₂} {F G H : C ⇒ D} definition nt_compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := natural_transformation.mk (take a, η a ∘ θ a) (take a b f, calc H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc ... = (η b ∘ G f) ∘ θ a : naturality ... = η b ∘ (G f ∘ θ a) : assoc ... = η b ∘ (θ b ∘ F f) : naturality ... = (η b ∘ θ b) ∘ F f : assoc

definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} := let m := fact (n + 1) in have m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), have m + 1 ≥ 2, from succ_le_succ this, obtain p prime p p ∣ m + 1, from sub_prime_and_dvd this, have p ≥ 2, from ge_two_of_prime prime p, have p > 0, from lt_of_succ_lt (lt_of_succ_le p ≥ 2), have p ≥ n, from by_contradiction (suppose ¬ p ≥ n, have p < n, from lt_of_not_ge this, have p ≤ n + 1, from le_of_lt (lt.step this), have p ∣ m, from dvd_fact p > 0 this, have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ p ∣ m + 1) this, have p ≤ 1, from le_of_dvd zero_lt_one this, absurd (le.trans 2 ≤ p p ≤ 1) dec_trivial), subtype.tag p (and.intro this prime p)

Structures

• Special kind of inductive datatype (only one constructor)
• Projections are generated automatically
• "Inheritance"
• Extensively used to formalize the algebraic hierarchy
• We can view them as parametric modules
structure has_mul [class] (A : Type) := (mul : A → A → A) structure semigroup [class] (A : Type) extends has_mul A := (mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c)) ... structure group [class] (A : Type) extends monoid A, has_inv A := (mul_left_inv : ∀a, mul (inv a) a = one)

Sylow theorem

variables {A : Type} [ambA : group A] [finA : fintype A] [deceqA : decidable_eq A] include ambA deceqA finA theorem cauchy_theorem : ∀ p, prime p → p ∣ card(A) → ∃ g : A, order(g) = p theorem first_sylow_theorem : ∀ p, prime p → ∀ n, p^n ∣ card(A) → ∃ (H : finset A) (sg : is_finsubg H), card(H) = p^n

Category Theory

theorem yoneda_embedding (C : Precategory) : C ⇒ set ^c Cᵒᵖ theorem contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C

Future work

• Auto tactic based on equational reasoning, matching, heuristic instantiation, …
• Decision procedures for arithmetic
• Efficient evaluator
• Better support for proof by reflection
• Better libraries (ongoing work)
• Machine learning