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

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

**Education**- Interactive courses
**Proving**should be as easy as**programming**

**Have Fun**

Formalized Mathematics

- Some projects at Microsoft Research
- Disclaimer:
**this projects were developed before Lean existed** - They used Boogie/Z3 and Coq.

Formalized Mathematics

- Similar problems
**Proof stability****Scalability**issues- Libraries are big
- Finding existing functions/theorems

- 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

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

- Before we started Lean, we have studied different theorem provers: ACL2, Agda, Automath, Coq, HOL (family), Isabelle, Mizar, PVS
**Dependent type theory**is really**beautiful**- Some advantages
- Bultin computational interpretation
- Same data-structure for representing proofs and terms
- Reduce code duplication, example:
- We implemented a compiler for Haskell-like recursive equations, we can use it to construct proofs by induction

- Mathematical structures (such as Groups and Rings) are first-class citizens

- Some references
- In praise of dependent types (Mike Shulman)
- Type inference in mathematics (Jeremy Avigad)

- Constants

- Function applications

- Lambda abstractions

- Function spaces

- What is the type of
`nat`

?

- What is the type of
`Type`

?

Is Lean inconsistent? **NO**

- Lean has a noncumulative universe hierarchy

- Supports
**universe polymorphism**

- In ordinary situations you can ignore the universe parameters and simply write
`Type`

, leaving the "universe management" to Lean - examples/ex1.lean

- Propositions are types

- The inhabitants/elements of a proposition
`P`

are the proofs of`P`

`Prop`

is the type of all propositions

- Kernel is implemented in two layers for easy customization
- 1st layer, dependent lambda calculus + options:
- Proof irrelevance
- Impredicative Prop

Π (x : nat), x = x -- is a Proposition ∀ (x : nat), x = x -- Alternative notation - 2nd layer: Inductive families, Quotient types, HITs

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

**Curly braces**indicate that argument should be**inferred**rather than entered explicitly.

- Elaborator uses
**higher-order unification**.

- Support
**constructive**and**classical**mathematics **Constructive**results are**more informative**- Computation is important to mathematics
**Core**parts of the standard library are**constructive****Separation of concerns**:- Methods to write computer programs
- Freedom to use a nonconstructive theories and methods to reason about them

**Semi constructive axioms**:- Function extensionality
- Proposition extensionality
- Quotient types (implies function extensionality)

- Computationally compatible axioms: proof irrelevant excluded middle, axiom of choice
**Anti constructive**: Hilbert's choice (aka magic)- consequence: all propositions are decidable

- We cannot generate code for
**anti constructive**axioms such as Hilbert's choice - Lean provides a mechanism for checking whether a definition depends on
**anti constructive**axioms or not.

- It prevents
**anti constructive**axioms from accidentally leaking inside definitions we want to compute with (generate code for).

- The standard library contains 3 axioms

- The first two axioms are semi-constructive.
- Most of the standard library does not use these axioms.

We use `propext`

and `quot.sound`

for defining sets, finite sets and bags.

- The choice axiom is used to define real division and to prove that the reals are Cauchy complete.
- The analysis library will also be classic.

- Option: type check imported modules.
**Macros**: semantic attachments for speeding up type checking and evaluation.- Macros can be eliminated (expanded into pure Lean code).
- Each macro provides a function for computing the type and evaluating an instance.
- Each macro can be assigned a
**trust level**. - Many applications: interface with the GNU multiprecision arithmetic (GMP) library.

**Relaxed**mode- Trust the imported modules have not been tampered
- Trust all macros

**Paranoid**mode- Retype check all imported modules (someone may have changed the binaries)
- Expand all macros (the developers may have made mistakes, GMP may be buggy)

**Stronger guarantee**Retype check everything using Lean reference type checker- Daniel Selsam implemented a reference type checker in Haskell

- Implemented by Daniel Selsam
- < 2000 lines of Haskell code
- Available at github
- Code is easy to read and understand
- It can type check the whole standard library (35K lines of Lean code) under 2 mins

- All Lean files can be exported in a very simple format
- Documentation is available on github
- Communicate with other tools
- Interface with the Lean reference type checker

- It is possible to
**construct**a substantial**edifice of mathematics**based on nothing more than the**type universes**,**function spaces**, and**inductive types**; everything else follows from those.

- Lean automatically generates several auxiliary definitions whenever a new inductive family is declared.
- examples/ex4.lean

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

- Proofs by induction

- Dependent pattern matching

- Elaborator must respect the computational interpretation of terms

- In Lean, we can associate
**attributes**to definitions. **Coercion**is one of the available attributes.

- We can group definitions, metadata (e.g., notation declarations and attributes) into namespaces.
- We can
**open**namespaces

- We can use namespaces to avoid unwanted ambiguity.
- We can
**override**overloading

`have x : T, from P, C`

is notation for`(λ x : T, C) P`

`have T, from P, C`

is notation for`have this : T, from P, C`

`take x : T, C`

, is notation for`λ x : T, C`

`assume x : T, C`

, is notation for`λ x : T, C`

`suppose T, C`

, is notation for`λ this : T, C`

`obtain w hw, from ex, C`

is notation for

`exists.rec (λ h hw, C) ex`

`obtain`

supports any inductive datatype with a single constructor`show T, from P`

is notation for`(P : T)`

``p``

is notation for`show p, by assumption`

**Synthesis**procedure- It can be viewed as a
**lambda-Prolog**interpreter - Big picture
- Mark some inductive families as
**classes** - Mark some definitions as (generators of)
**instances** - Indicate that some implicit arguments must be synthesized using type classes

- Mark some inductive families as
**Instances**are treated as**Horn clauses**

- An element of
`Prop`

is said to be

decidable if we can decide whether it is true or false.

- Having an element
`t : decidable p`

is stronger than having an element`t : p ∨ ¬p`

- The expression
`if c then t else e`

contains an implicit argument`[d : decidable c]`

. - If Hilbert's choice is imported, then all propositions are decidable (smooth transition to classical reasoning).

- Automation such as rewrite engined, simplifiers and decision procedures are integrated into the system as tactics.
- A placeholder/hole can be viewed as a
**goal** - A
**proof state**is a sequence of goals, substitution (already solved holes), and postponed constraints. - A
**tactic**is a function from proof state to a**lazy stream of proof states**(very similar to Isabelle). **Tacticals**are tactic combinadors:**andthen**,**orelse**,**par**, …

- We can switch to
**tactic mode**using**begin … end**or**by …**

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

- Is
`int`

a`add_group`

?**Yes**

- Let
`A`

be any type, and let`R`

be an equivalence relation on`A`

. It is mathematically common to form the "quotient"`A / R`

, that is, the type of elements of`A`

"modulo"`R`

. - Set theoretically, one can view
`A / R`

as the set of equivalence classes of`A`

modulo`R`

. - If
`f : A → B`

is any function that respects the equivalence relation in the sense that for every`x y : A`

,`R x y`

implies`f x = f y`

, then`f`

"lifts" to a function`f' : A / R → B`

defined on each equivalence class`[x]`

by`f' [x] = f x`

.

The quotient package consists of the following constructors:

- Quotients are used to prove function extensionality
- They are used to define finite sets and bags in the standard library

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

- Lua is an efficient embedded programming language
- It is very popular in the computer gaming industry
- Lean provides a Lua API
- We can access terms, create definitions and tactics, type check terms etc
- Lua scripts can be embedded in Lean files
- examples/lua.lean

- Lean has been compiled as a Javascript library
- We have used this library to implement the interactive tutorial
- We can use it to write other applications (e.g., a fancier web IDE)
- examples/ex.html

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