Discussing "The Lean Theorem Prover (System Description)"

(Link)

Authors: Leonardo de Moura (Microsoft Research Redmond)), Soonho Kong (Carnegie Mellon University), Jeremy Avigad (Carnegie Mellon University), Floris van Doorn (Carnegie Mellon University), and Jakob von Raumer (Carnegie Mellon University)

Reference: de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J. (2015). The Lean Theorem Prover (System Description). In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_26

Why this paper? Cited by Encoding Dependently-Typed Constructions into Simple Type Theory and A Type-Based Approach to Divide-and-Conquer Recursion in Coq

Lean is something of a new kid on the block in the world of interactive theorem proving, coming out just 10 years ago, compared to 34 years for Coq and 36 for Isabelle. Nonetheless it has clearly had impact; for example this year’s CPP (Certified Programs and Proofs) conference, which I had the privilege to be a member of the program committee for, by my count had 7 of 25 accepted papers using Lean.

This short conference paper gives a brief and high-level description of the aims and design principles of the new theorem prover. It is neither a tutorial (see pdf) nor in-depth description of the nitty gritty of the implementation (for which see e.g. here). It does, perhaps, give some sense of why developing a new prover was thought to be desirable rather than simply using the established technologies, although it is rather polite and implicit about any comparisons with other provers. Lean, which like Coq is based on Martin-Löf dependent type theory, has a few features emphasised: its small trusted code base, its support for different proving styles (declarative à la Isabelle, or imperative-style tactics to generate proof terms), its flexible framework for supporting automation and talking to other software, its user interface, and its relatively fast speed and support for parallelism. Homotopy type theory is highlighted as one of the motivating application areas. The bulk of the paper is an informal description of the elaboration algorithm, which compiles definitions and proofs written in various styles down to the proof terms that the small trusted kernel can accept.