Abstract is: Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types. The Lean project is an open source project, hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013. Lean has an interface that differentiates it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols. (These can be typed using LaTeX-like sequences, such as " imes" for "×".) Lean also has an extensive support for meta-programming. Lean has gotten attention from mathematicians Thomas Hales and Kevin Buzzard. Hales is using it for his project, Formal Abstracts. Buzzard uses it for the Xena project. One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean.
| programming language | Q9143 |
| open-source software | Q1130645 |
| proof assistant | Q11387554 |
| P4162 | AUR package | lean-bin |
| lean-git | ||
| P973 | described at URL | http://www.andrew.cmu.edu/user/avigad/Papers/lean_system.pdf |
| P7427 | FreeBSD port | math/lean |
| P2037 | GitHub username | leanprover |
| P2671 | Google Knowledge Graph ID | /g/11j7dt82fy |
| P8443 | Homebrew formula name | lean |
| P1401 | issue tracker URL | https://github.com/leanprover/lean4/issues |
| P4215 | nLab ID | Lean |
| P856 | official website | http://leanprover.github.io/ |
| P1972 | Open Hub ID | lean |
| P6931 | Repology project name | lean |
| P1324 | source code repository URL | https://github.com/leanprover/lean4 |
| P1482 | Stack Exchange tag | https://stackoverflow.com/tags/lean |
| P275 | copyright license | Apache Software License 2.0 | Q13785927 |
| P6216 | copyright status | copyrighted | Q50423863 |
| P178 | developer | Microsoft Research | Q1144725 |
| P366 | has use | automated theorem proving | Q431667 |
| P571 | inception | 2013-01-01 | |
| P737 | influenced by | Coq | Q1131652 |
| Isabelle | Q460340 | ||
| P407 | language of work or name | English | Q1860 |
| P306 | operating system | cross-platform | Q174666 |
| P400 | platform | cross-platform | Q174666 |
| P277 | programmed in | C++ | Q2407 |
| C | Q15777 | ||
| P577 | publication date | 2013-01-01 | |
| P348 | software version identifier | 4.5.0 | |
| 3.4.2 | |||
| P7078 | typing discipline | dependent type | Q997433 |
| Q5423569 | F* | influenced by | P737 |
| Q111738341 | Formalizing Geometric Algebra in Lean | main subject | P921 |
| Lean (programovací jazyk) | wikipedia | |
| Lean (Beweisassistent) | wikipedia | |
| Lean (proof assistant) | wikipedia | |
| Lean | wikipedia | |
| Persian (fa / Q9168) | لین (دستیار اثبات) | wikipedia |
| Lean (assistant de preuve) | wikipedia | |
| Lean (証明アシスタント) | wikipedia | |
| Lean (bewijsassistent) | wikipedia | |
| Lean | wikipedia | |
| Lean | wikipedia | |
| Lean (trợ lý chứng minh) | wikipedia | |
| Lean | wikipedia |
Search more.