Lean: Past, Present, and Future (Invited Talk)

The Lean programming language and theorem prover project is celebrating its tenth birthday this year, having been started by Leonardo de Moura at Microsoft Research and first release as Lean 0.1 in 2014. In this invited talk, I will review Lean’s history and unique features and discuss our roadmap for its bright future. Corresponding to its major versions ranging from Lean 0.1 to the current version of Lean 4, the focus of the Lean project has evolved over the years. Initially intended as a platform for developing white-box automation, in contrast to the usual black-box approach of stand-alone SMT solvers [de Moura and Passmore, 2013], the system gathered more conventional features of dependently-typed interactive theorem provers as well as an initial crowd of interested mathematicians and computer scientists with its first official release as Lean 2 in 2015 [Leonardo de Moura et al., 2015]. Lean 3 in 2017 introduced user-extensible automation by extending Lean from a specification language to an accessible metaprogramming language [Gabriel Ebner et al., 2017], further accelerating growth of its mathematical library that was spun out into the separate Mathlib project [{The mathlib Community}, 2020]. Spurred by the success but also limitations of this extensibility, we started work on the next version Lean 4 in 2018 [Leonardo de Moura and Sebastian Ullrich, 2021] with the goal of turning Lean into a general-purpose programming language that would allow us to reimplement Lean in Lean itself and thereby make many more aspects of the system user-extensible, in a more efficient manner [Sebastian Ullrich, 2023]. This to date largest rework of Lean’s implementation was completed in 2023 with the official release of Lean 4.0.0, further supporting Mathlib’s growth to more than 1.5 million lines of code at the time of writing as well as improving support for many other applications such as software verification. In 2023, Lean also saw its largest organizational change when Leo and I created the Lean Focused Research Organization (FRO) to bundle and support development of Lean in a dedicated organization for the first time. Thanks to gracious support from philanthropic sponsors, an unprecedented number of currently twelve people now work on the evolution of Lean at the Lean FRO. And there is much left to do: with our new team size, we can now support development on much more than only core features, such as documentation, a robust standard library, and user interfaces and experience as well as a return to the original topic of advanced proof automation. The Lean FRO is committed to ensuring and extending Lean’s applicability in education, research, and industry and to leading it into the next decade of Lean development and beyond.