Soonho Kong (CMU), Jeremy Avigad (CMU),

Floris van Doorn (CMU), Jakob von Raumer (KIT),

Rob Lewis (CMU), Haitao Zhang,

Daniel Selsam (Stanford)

http://leanprover.github.io

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

- 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"

- It is an ongoing and
**long long term**effort - At CMU, it is already being used for formalizing
- Homotopy Type Theory
- Category Theory
- Algebraic Hierarchy
- Nonabelian Algebraic Topology
- Number Theory

- Interactive theory proving course at CMU
- Haitao Zhang is formalizing Group Theory
- Floris van Doorn implemented propositional truncation as a non-recursive HIT

**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

**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**

- Poweful
**elaboration engine**that can handle- Higher-order unification
- Definitional reductions
- Coercions
- Ad-hoc polymorphism (aka overloading)
- 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

- 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

- It does

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

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

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

- 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**

**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

**Recursors**are**inconvenient**to use.- Compiler from
**recursive equations**into**recursors**. - Two compilation strategies:
**structural**and**well-founded**recursion

- Dependent pattern matching

- 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**

- Developed by Floris van Doorn and Jakob von Raumer
- In the HoTT library

**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

- Website: http://leanprover.github.io/
- Source code: https://github.com/leanprover/lean
- Theorem proving in Lean: https://leanprover.github.io/tutorial/index.html