Lean (proof assistant)
Proof assistant and programming language / From Wikipedia, the free encyclopedia
Dear Wikiwand AI, let's keep it short by simply answering these key questions:
Can you list the top facts and stats about Lean (proof assistant)?
Summarize this article for a 10 year old
SHOW ALL QUESTIONS
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 principally developed 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).
Quick Facts Paradigm, Developer ...
Paradigm | Functional programming, Imperative programming |
---|---|
Developer | Lean FRO |
First appeared | 2013; 11 years ago (2013) |
Stable release | |
Preview release | |
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 |
Close