Lean (proof assistant)
| Lean | |
|---|---|
 | |
| Paradigm | Strict purely functional, dependently typed |
| Family | Proof assistant |
| Designed by | Leonardo de Moura |
| Developer | Lean FRO |
| First appeared | 2013 |
| Stable release | 4.33.1 
/ 21 August 2026 |
| Typing discipline | static, strong, inferred |
| Implementation language | Lean, C++ |
| Platform | x86-64, AArch64 |
| OS | Cross-platform: Linux, macOS, Windows |
| License | Apache 2.0 |
| Website | lean-lang |
| Influenced by | |
| ML, Rocq (formerly named Coq), Haskell | |
Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types (specifically, the Calculus of Inductive Constructions), the foundational type theory developed with the Coq theorem prover, which was renamed to Rocq in 2024. It is a free and open-source software project hosted on GitHub. Development is currently supported by the nonprofit Lean Focused Research Organization (FRO).