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.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons