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=Apple&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.18.0[1] 
/ 1 April 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.[2] 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).
- ^ "Release 4.18.0". 1 April 2025. Retrieved 27 April 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.
© MMXXIII Rich X Search. We shall prevail. All rights reserved. Rich X Search