The Lean Theorem Prover (System Description)

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 e 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.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
• Keywords: CADE 2015, Logical Reasoning