@inproceedings{demoura2021the,
author = {de Moura, Leonardo and Ullrich, Sebastian},
title = {The Lean 4 Theorem Prover and Programming Language},
booktitle = {2021 Conference on Automated Deduction},
year = {2021},
month = {July},
abstract = {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.},
publisher = {Springer, Cham},
url = {http://approjects.co.za/?big=en-us/research/publication/the-lean-4-theorem-prover-and-programming-language/},
pages = {625-635},
}