Days:
previous day
next day
all days
| 09:00-10:00 |
The Lean Theorem Prover: Design, Evolution, and Impact (abstract) 60 min
ABSTRACT. Lean is an open-source theorem prover and dependently-typed programming language that has seen rapid adoption across mathematics, software verification, and AI research. Its Mathlib library is among the largest formalized mathematical developments in existence. Lean's design emphasizes extensibility: the system is implemented in Lean itself, and a powerful meta-programming framework enables users to build custom automation and domain-specific tools. This talk traces Lean's history from its origins in 2013 through four major rewrites to the present day, discusses the design decisions that shaped the system and the lessons learned along the way, and concludes with current priorities at the Lean Focused Research Organization. |