Lean Theorembeweiser

Visiting student from Karlsruhe Institute of Technology, sponsored by the Baden- Württemberg-Stipendium. 2L. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer requiring that every claim is supporting by a proof in a suitable axiomatic foun- dation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. In fact, most such systems provide fully elaboratedproof objectsthat can be communicated to other systems and checked independently. Constructing such proofs typically requires much more input and interaction from users, but it allows us to obtain deeper and more complex proofs. TheLean Theorem Prover 3 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 speci- fied axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains. Lean is released under the Apache 2.0 license, a permissive open source license that permits others to use and extend the code and mathematical libraries freely. At Carnegie Mellon University, Lean is already being used to formalize cate- gory theory, homotopy type theory, and abstract algebra. Lean is an ongoing, long-term effort, and much of the potential for automation will be realized only gradually over time. Lean’s small, trusted kernel is based on dependent type theory, with sev- eral configuration options. It can be instantiated with an impredicative sort or propositions,Prop, to provide a version of the Calculus of Inductive Con- structions (CIC) [ 5,6]. Moreover,Propcan be marked proof-irrelevant if desired. Without an impredicativeProp, the kernel implements a version of Martin-Löf type theory [12,23]. In both cases, Lean provides a sequence of non-cumulative type universes, with universe polymorphism. Lean is meant to be used both as a standalone system and as a software library. SMT solvers can use the Lean API to create proof terms that can be independently checked. The API can be used to export Lean proofs to other systems based on similar foundations (e.g., Coq [ 3] and Matita [1]). Lean can also be used as an efficient proof checker, and definitions and theorems can be checked in parallel using all available cores on the host machine. When used as a proof assistant, Lean provides a powerful elaborator that can handle higher-order unification, definitional reductions, coercions, overloading, and type classes, in an integrated way. Lean allows users to provide definitions and theorems using a declarative style resembling Mizar [ 20] and Isabelle/Isar [24]. Lean also provides tacticsas an alternative (more imperative) approach to constructing (proof) terms as in Coq, HOL-Light [ 10], Isabelle [17] and PVS [19]. Moreover, the declarative and tactic styles can be freely mixed together. Lean includes two libraries of formally verified mathematics and basic data- structures. The standard library uses a kernel instantiated with an impredicative and proof-irrelevantProp. This library supports constructive and classical users, and the following axioms can be optionally used: propositional completeness, function extensionality, and strong indefinite description. Lean also contains a 3 4L. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer known as placeholders) are internally represented as metavariables that must be replaced by closed terms that are synthesized by the system. Since metavari- ables can only be assigned closed terms, a metavariable that occurs in a context records the parameters it must depend on. For example, we encode a hole in the context(x:nat) (y:bool)as?mxy, where?mis a fresh metavariable. As with free variables, every metavariable has a type. We also have universe metavariables to represent “holes” in