Back Lean (programovací jazyk) Czech Lean (Beweisassistent) German Lean Spanish لین (دستیار اثبات) Persian Lean (assistant de preuve) French Lean (証明アシスタント) Japanese Lean (bewijsassistent) Dutch Lean Russian Lean Ukrainian Lean (trợ lý chứng minh) Vietnamese
&sq=Albert Einstein&lang=en&file=File:Lean_logo2.svg){kind=logo} | |
| Paradigm | Functional programming, Imperative programming |
|---|---|
| Developer | Lean FRO |
| First appeared | 2013 |
| Stable release | 4.8.0
/ 5 June 2024 |
| Preview release | 4.9.0-rc2
/ 14 June 2024 |
| 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 | |
Preview warning: Page using Template:Infobox programming language with unknown parameter "genre"
Preview warning: Page using Template:Infobox programming language with unknown parameter "language"
Preview warning: Page using Template:Infobox programming language with unknown parameter "repo"
Lean is a proof assistant and a functional programming language.[1] 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).
- ^ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, André; Sutcliffe, Geoff (eds.). "The Lean 4 Theorem Prover and Programming Language". Automated Deduction – CADE 28. Cham: Springer International Publishing: 625–635. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5.