Gabriel Ebner: The Lean Theorem Prover

Lean is a new, open source, interactive theorem prover designed to support mathematical reasoning as well as hardware and software verification.  One of the goals is to bridge the gap to automated theorem proving by integrating automated reasoning tools such as E-matching, congruence closure, and simplfication.  These are implemented in a white-box fashion, allowing the user to access their internals, for example the equivalence classes of the congruence closure algorithm.  Because its logical foundation, dependent type theory, has a computational interpretation, we can also use Lean as a programming language and evaluate expressions with a fast bytecode evaluator.

In this tutorial, I will give an introduction to the Lean language, show how to write definitions, and how to use tactics to prove properties about them.  I will then showcase the integrated automation tools on examples from software verification.