Conference Papers: The Lean 4 Theorem Prover and Programming Language

[demoura21lean4]Leonardo de Moura, Sebastian Ullrich, The Lean 4 Theorem Prover and Programming Language, Platzer, André and Sutcliffe, Geoff (Ed.), Automated Deduction -- CADE 28, pp. 625--635, Springer International Publishing, Cham, 2021.


Lean 4 is a reimplementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom proof automation procedures in Lean itself.




Authors at the institute

Scientific Staff
Sebastian Ullrich