Back Lean (programovací jazyk) Czech Lean (Beweisassistent) German Lean Spanish لین (دستیار اثبات) Persian Lean (assistant de preuve) French Lean (証明アシスタント) Japanese Lean (bewijsassistent) Dutch Lean (linguagem de programação) Portuguese Lean Russian Lean Ukrainian
&sq=Google&lang=en&file=File:Lean_logo2.svg){kind=logo} | |
| Paradigm | Functional programming, Imperative programming |
|---|---|
| Family | Proof assistant |
| Developer | Lean FRO |
| First appeared | 2013 |
| Stable release | 4.16.0[1] 
/ 3 February 2025 |
| Typing discipline | Static, strong, inferred |
| Implementation language | Lean, C++ |
| OS | Cross-platform |
| License | Apache License 2.0 |
| Website | lean-lang |
| Influenced by | |
| ML Coq Haskell | |
Lean is a proof assistant and a functional programming language.[2] It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. It was developed primarily by Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services, and has had significant contributions from other coauthors and collaborators during its history. Development is currently supported by the non-profit Lean Focused Research Organization (FRO).
- ^ "Release 4.16.0". 3 February 2025. Retrieved 25 February 2025.
- ^ Moura, Leonardo de; Ullrich, Sebastian (2021). "The Lean 4 Theorem Prover and Programming Language". In Platzer, André; Sutcliffe, Geoff (eds.). Automated Deduction – CADE 28. Lecture Notes in Computer Science. Vol. 12699. Cham: Springer International Publishing. pp. 625–635. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5.