skip to content

The Lean Theorem Prover

Presented by: 
Jeremy Avigad
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