Click here for the Schedule.

Click here to return to Workshop Homepage.

Invited Speaker

Author: Jeremy Avigad (Carnegie Mellon University)
Title: The Lean Theorem Prover
Slides: Click here for the slides.
Abstract: Lean is a new interactive theorem prover that is based on dependent type theory. The system is designed to combine interactive theorem proving, computation, and automation within the same logical framework. Dependent type theory provides an expressive language for reasoning about concrete and abstract mathematical structures, and the fact that it has a computational interpretation means that Lean can be used as a programming language as well. With a suitable interface to the system internals, it can also be used as a metaprogramming language, that is, a language with which one can extend the functionality of the system itself. I will survey all these aspects of the system in this talk, and consider ways that Lean can be used as a platform to unify symbolic combination, automated reasoning, and verified proof. In particular, I will describe a Lean-Mathematica connection developed by Robert Y. Lewis, which takes advantage of Lean's metaprogramming capabilities.

Full Papers

Extended Abstracts

Presentations Without Publication