Lean theorem prover/History/Lean 4

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 4 is a reimplementation of Lean, written for the most part in Lean itself. Its development began in 2018, it was described at the Conference on Automated Deduction in 2021, and its first stable version, 4.0.0, appeared on 8 September 2023. In the same year the mathematical library was carried over from Lean 3. This page covers the rewrite, the stable versions, and the port.

Why a rewrite

Lean 3 was written in C++. Its developers name two problems with that in the Lean 4 system description. Users could not change many parts of the system without changing the C++ source. And proof automation written as Lean 3 metaprograms was slow compared with the same procedures written in C++ or OCaml, chiefly because Lean 3 interpreted metaprograms in a virtual machine. The Lean reference manual adds that a C++ implementation limited Lean's flexibility and made it harder to develop, because of the range of skills it required. The earlier versions are described at Lean 1 to Lean 3.

The 2021 system description

Leonardo de Moura and Sebastian Ullrich described the new system at CADE-28 in 2021. Their abstract calls Lean 4 a reimplementation of the Lean interactive theorem prover in Lean itself, and says that users can modify and extend the parser, the elaborator, the tactics, the decision procedures, the pretty printer and the code generator.

The paper lists what was new. A hygienic macro system, designed for theorem provers, lets users add notation without accidental capture of names. Type class resolution uses a tabled procedure, which addressed performance problems reported by users. The compiler produces C code, so that automation written in Lean can be compiled to native code and loaded as a plugin. Memory is managed by reference counting, which lets a function update data in place when nothing else shares it, a style the authors call "functional but in-place". An editor server implements the Language Server Protocol. The paper ends by noting that Lean's trusted kernel is relatively small, and that its interface lets users export their developments to other systems and write their own reference checkers. The paper also states that Lean 4 was made public at the beginning of 2021, with the community already porting mathlib.

The manual gives the result of the rewrite in one figure: from version 4, about 90 per cent of the code that implements Lean is written in Lean. The interface the system uses for itself is open to users. The function that runs a tactic, for example, is an ordinary Lean definition:

import Lean
#eval Lean.versionString
#check @Lean.Elab.Tactic.evalTactic

With version 4.34.1, the version used for the code in this edition, Lean prints "4.34.1" and then Lean.Elab.Tactic.evalTactic : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit: a tactic is run by a function from syntax to an action in the tactic monad. How that machinery works is described at The tactic framework and Metaprogramming in Lean; the macro system at Syntax extension and hygienic macros; the compiler at The compiler and runtime.

The first stable version

Until September 2023 most of the Lean 4 ecosystem worked with nightly versions. Version 4.0.0, dated 8 September 2023, was the first stable version. The announcement on the Lean community blog set out a schedule: a new minor version roughly each month, preceded by a candidate version early in the month, with breaking changes documented but no promise yet of backward compatibility. Versions have followed in sequence since; this edition's examples are checked with version 4.34.1. The manual records that the development of Lean 4 took about as long as all earlier versions together, and that no further rewrite is planned.

The port of mathlib

In December 2021 mathlib, the Lean 3 mathematical library, had more than 700,000 lines. Lean 4 could not run Lean 3 code. The plan, set out on the community blog in December 2021, was a semi-automated port by a tool called Mathport, written mostly by Mario Carneiro and Daniel Selsam. Mathport has two parts. One translates the compiled Lean 3 files into compiled Lean 4 files, so that the whole library could be imported at once; the other makes a best-effort translation of the Lean 3 source text into Lean 4 syntax.

The post explains why the port could not be mechanical. Mathlib kept growing while the port went on, so the plan was not to freeze it until late. Files would move to the new library from the bottom of the import hierarchy up, with Mathport re-run on the still-changing Lean 3 sources and lining up definitions already ported. Mathport did not translate the library's tactics: metaprogramming in Lean 4 differs too much, so they had to be written again by hand.

The manual records that the port was completed in 2023 through a community effort supported by the Lean developers. The community's page tracking the port records it as declared complete as of 16 July 2023. The Lean 3 library is now marked as no longer actively maintained. According to the same manual, mathlib had over one million lines at the end of Lean 3 and has since grown to over 1.5 million, and Lean 4 checks the larger library faster than Lean 3 checked the smaller one. The library and the people who maintain it are the subject of Mathlib and its community.

In July 2023, two months before the first stable version, de Moura and Ullrich founded the Lean Focused Research Organization, whose staff now work on Lean; its work is followed at Lean since 2023.

Provenance: the 2021 system description, the Lean reference manual's history section (as of version 4.34.0), the two community blog posts, the community's porting status page and the Mathport and mathlib README files were read. The quotation "functional but in-place" is the 2021 paper's name for its technique. The date on which the port was declared complete is the one given on the community's porting status page.

Next

Mathlib and its community