Lean (proof assistant)
| Lean | |
|---|---|
| Paradigm | Functional programming, Imperative programming |
| Family | Proof assistant |
| Developer | Lean FRO |
| First appeared | 2013 |
| Stable release | 4.20.1
/ 4 June 2025 |
| Typing discipline | Static, strong, inferred |
| Implementation language | Lean, C++ |
| OS | Cross-platform |
| License | Apache License 2.0 |
| Website | lean-lang |
| Influenced by | |
| ML Rocq (previously known as Coq) Haskell | |
Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. Development is currently supported by the non-profit Lean Focused Research Organization (FRO).