Carnegie Mellon University
Browse
- No file added yet -

The Lean Theorem Prover (system description)

Download (117.77 kB)
journal contribution
posted on 2015-08-01, 00:00 authored by Leonardo de Moura, Soonho Kong, Jeremy AvigadJeremy Avigad, Floris Van Doorn, Jakob von Raumer

Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work.

History

Publisher Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-21401-6_26

Date

2015-08-01

Usage metrics

    Categories

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC