Skip to content

The origins of Lean

Lean is younger than most of the game theory these notes assume, and its history explains several things a newcomer notices: why it feels like a programming language, why its mathematics lives in a separate community library, and why older material online often does not compile.

A theorem prover from Microsoft Research

Leonardo de Moura launched the Lean project in 2013 at Microsoft Research in Redmond. De Moura had previously created Z3, an automated solver widely used to verify software, and the stated aim of Lean was to bridge the gap between automated and interactive theorem proving: to combine a system in which a person writes the proof with the automation that makes long proofs bearable.

Like Coq, now renamed Rocq, Lean is founded on dependent type theory, a variant of the calculus of inductive constructions. This is the setting in which, as chapter 3 of the tutorial put it, a statement is a type and a proof is a value of that type.

The first versions, later known as Lean 1 and Lean 2, were experimental. They included features, such as support for homotopy type theory, that were later dropped. Lean 3, released in January 2017, was the first version stable enough for sustained use.

Mathematicians arrive

Lean 3 attracted mathematicians rather than only computer scientists, and the community library that became Mathlib grew up around it. Kevin Buzzard's Xena project at Imperial College London brought undergraduates into formalisation and argued publicly for checking mathematics by machine.

The turning point in visibility was the Liquid Tensor Experiment. In December 2020 Peter Scholze challenged the community to verify a central theorem of his work with Dustin Clausen on condensed mathematics, a result he was not fully confident of himself. The formalisation was completed on 14 July 2022, a year and a half after the challenge was posed. It showed that Lean and Mathlib could handle research mathematics at the frontier, not only textbook results.

Lean 4

Lean 4 is a reimplementation rather than an upgrade. De Moura and Sebastian Ullrich described it in 2021 as a theorem prover and programming language, and it is largely written in Lean itself. It is fast enough to be used for ordinary programs, which is why the tutorial could #eval an action in chapter 2, and why tactics such as norm_num are ordinary Lean code that anybody can read or write.

Lean 4 was not backwards compatible with Lean 3, so Mathlib had to be translated, partly by an automatic tool and partly by hand. The port was declared complete on 16 July 2023, and Lean 4.0.0 was released on 8 September 2023. This is why material written for Lean 3, with syntax such as begin and end around proofs, does not work today, and it is worth checking which version any tutorial found online was written for.

In July 2023 the Lean Focused Research Organization was formed as a non-profit, under Convergent Research, with de Moura as its chief architect. Its purpose is to develop Lean's core systems and guide the project towards long-term sustainability. Lean now ships a new release roughly every month, and Mathlib tracks each one, which is why these notes pin both.

Why this matters here

For a game theorist, the history explains the division of labour described in Lean and Mathlib. Lean itself is a general-purpose system built by a small core team. The mathematics, including the real numbers every payoff in these notes relies on, comes from a large community that took shape around Lean 3 and was carried over to Lean 4. At the version these notes pin, Mathlib contains no Nash equilibria and no evolutionary stability at all. That is one reason projects such as elazarg/GameTheory exist outside it, and why a set of notes like these still starts from nothing.

Sources

The dates and events on this page are drawn from the following.