Theorem provers need a combination of expressive type theory, efficient proof automation, and a practical programming language, but existing systems typically compromise on one or more of these aspects.

Lean is designed as both a theorem prover and programming language based on dependent type theory with a cumulative hierarchy of non-cumulative universes. It supports inductive types, type classes for ad-hoc polymorphism, and a tactic framework for proof automation. The paper describes the system architecture including the kernel, elaboration engine, and proof automation infrastructure.

Lean is released as an open-source system developed at Microsoft Research, providing a unified environment for formal verification and functional programming with a small trusted kernel and extensible automation.