The Lean 4 Theorem Prover and Programming Language

By Leonardo de Moura, Sebastian Ullrich. CADE, 2021

724 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/c4c0d6ffd70081d143b32be53b06fec1259b3ad8

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Neurosymbolic Program Synthesis (positive): “Thakur et al. [19] use an LLM-guided search for formal theorem-proving in frameworks like Lean [35].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “The Proof Module can output formal unsatisﬁability proofs in three proof formats: Alethe [128], Lean 4 [88], and LFSC [133].”