← All papers
The Lean 4 Theorem Prover and Programming Language
cs.LO
Jul 11, 2021 · v1
TL;DR
Presents Lean 4's architecture as both a dependently-typed programming language and interactive theorem prover.
Abstract
Lean 4 is a reimplementation of the Lean interactive theorem prover in Lean itself. It addresses the performance limitations of the previous version and features a new compiler that generates efficient native code. The system serves both as a programming language with dependent types and as an interactive theorem prover, featuring a powerful macro system and hygienic notation.
Problem
The previous version of the Lean theorem prover had performance limitations that hindered its use as both a programming language and an interactive theorem prover at scale.
Approach
Lean 4 is a complete reimplementation of the Lean interactive theorem prover in Lean itself. It features a new compiler that generates efficient native code, serves as both a programming language with dependent types and an interactive theorem prover, and includes a powerful macro system with hygienic notation.
Results
Lean 4 addresses the performance limitations of previous versions and provides a self-hosted system that unifies dependently-typed programming with interactive theorem proving.