skip to content

The Lean Theorem Prover

Presented by: 
Jeremy Avigad Carnegie Mellon University
Thursday 29th June 2017 - 11:00 to 12:00
INI Seminar Room 2
Lean is a new, open source, interactive theorem prover designed to support mathematical reasoning as well as hardware and software verification. Because its logical foundation, dependent type theory, has a computational interpretation, we can use Lean as a programming language and evaluate expressions with a fast bytecode evaluator. We obtain a metaprogramming language -- that is, a language that we can use to construct expressions and proofs in dependent type theory itself -- by exposing Lean internals through a suitable API. This provides us with a means of extending Lean's functionality and automation within Lean itself. In this talk, I will describe this metaprogramming framework and some of its mechanisms for manipulating expressions efficiently.

The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons