Lean 1 to Lean 3

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Lean was started in 2013 by Leonardo de Moura at Microsoft Research. Its first three major versions were written in C++ and developed mainly at Microsoft Research and Carnegie Mellon University. This page covers them: the system described in 2015, the second version's mode for homotopy type theory and why it did not survive, the third version and its metaprogramming in Lean, and the community's maintenance of that version after its developers turned to Lean 4.

The start, 2013

The Lean 4 system description dates the project's start to 2013, as an interactive theorem prover based on the Calculus of Inductive Constructions. A 2017 paper by three of its early users adds that de Moura started it, and that it was developed mainly at Microsoft Research and Carnegie Mellon University under the Apache 2.0 licence.

The Lean reference manual records that Lean 0.1, the first version, appeared officially on 16 June 2014. It states the project's goal as combining the trust that comes from a small logical core, the Lean kernel, which others can implement independently, with the convenience and automation of tools such as SMT solvers. The first versions were mainly C++ libraries in which client code could construct proofs that could be checked independently; the design then moved towards a conventional interactive prover, first with tactics written in the scripting language Lua and later with a syntax of its own.

The 2015 system description

The first published account is "The Lean Theorem Prover (system description)" by de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer, presented at the 25th Conference on Automated Deduction (CADE-25) in 2015. It states the aim in one line: to bridge the gap between interactive and automated theorem proving, by placing automated tools inside a framework that supports user interaction and the construction of fully specified axiomatic proofs.

The paper describes Lean's small trusted kernel, written in two layers of C++: a type checker and the operations on terms in about 6,000 lines, and inductive families in about 700 more. The logic could be configured. With an impredicative sort of propositions, which could also be made proof-irrelevant, it gave a version of the Calculus of Inductive Constructions; without one, a version of Martin-Löf type theory. In both cases the universes were non-cumulative and definitions could be polymorphic in universe levels. Above the Lean kernel sat an elaborator that handled higher-order unification, coercions, overloading and type classes together. Proofs could be written as terms, in a declarative style resembling Mizar and Isabelle/Isar, or with tactics. Editing ran in Emacs with continuous checking, and JavaScript bindings let Lean run in a web browser. At Carnegie Mellon it was being used to formalise category theory, homotopy type theory and abstract algebra, and for a course in the spring of 2015.

The paper ends with plans: more search and decision procedures, better support for homotopy type theory, and an independent type checker, which it says Lean's small kernel makes simpler to write. Independent checkers for Lean now exist; see Proof export and independent checkers.

The second version and homotopy type theory

The version described in 2015 is the one now called Lean 2; its published source describes itself as a snapshot of Lean 0.2, kept separately because it has special support for homotopy type theory.

Lean 2's kernel had two modes. In the standard mode the lowest universe, Prop, was proof-irrelevant: any two proofs of a proposition were equal by definition. Proof irrelevance is incompatible with homotopy type theory, in which equality corresponds to paths in a space, so a second mode without proof irrelevance was added, and a library for homotopy type theory was written in it.

The third version did not keep that mode. Van Doorn, von Raumer and Buchholtz give two design decisions as reasons: Lean 3's virtual machine erases proofs, and its mechanism for defining functions by pattern matching relies on axiom K. In 2017 the library therefore remained in Lean 2, which was still maintained but no longer developed. The reason the standard mode is proof-irrelevant is set out at Proof irrelevance and subsingleton elimination.

Lean 3

Version 3.0.0 of Lean is dated 20 January 2017, the date the reference manual also gives. The 2017 homotopy paper places the third major version in 2016, and records that many of Lean's components were rewritten for it and that its unification was restricted, because the full higher-order unification of Lean 2 could produce timeouts and error messages unrelated to the user's mistake.

The change that mattered most was metaprogramming in Lean itself. Ebner, Ullrich, Roesch, Avigad and de Moura described it in 2017. Definitions marked meta may use an interface to Lean's internal structures and procedures, and may recurse without proof of termination. They are compiled to bytecode and run in a virtual machine. Tactics become ordinary Lean programs in a tactic monad, written in the same files and with the same library as the mathematics. The paper's examples range from small interactive tactics to a simplifier and a superposition prover. The idea is followed backwards at LCF and the tactic idea and forwards at Metaprogramming in Lean.

In 2017, on Lean 3, a community of users started the mathematical library mathlib. Its history is at Mathlib and its community.

The community's Lean 3

The last official version of Lean 3 was 3.4.2, dated 18 January 2019. The developers turned to a reimplementation, and the original Lean 3 source now carries a notice that it is frozen and that Lean 4 is the official line.

Mathlib's users still needed Lean 3, and they continued it themselves. Version 3.5.0c of 26 December 2019 is recorded as the first community version, and the community line ran to 3.51.1c of 24 May 2023. The community's edition describes itself as a fork of Lean 3 maintained by the Lean community, and now warns that Lean 3 is no longer actively maintained and that Lean 4 should be used instead. Mathlib's own move to Lean 4 is told at Lean 4.

The Lean 4 system description names the limits that led to the rewrite. Many parts of Lean 3 could not be changed without editing its C++ source, and proof automation written as Lean 3 metaprograms ran slowly, chiefly because of the overhead of interpreting it in the virtual machine.

Provenance: the 2015, 2017 and 2021 papers were read, as were the README files and the community change log. The date of version 3.0.0 is the date on its tag; the 2017 homotopy paper's "2016" is reported as that paper states it. Nothing here is quoted except one line of the Lean 2 README file, in the references.

Next

Lean 4