Lean is a proof assistant and a functional programming language. 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). Wikipedia
Created Year: 2013Designed by: Leonardo de Moura
Developed by: Leonardo de Moura • Microsoft Research
Operating systems: cross-platform
Implemented in: C • C++ • Lean
Aliases: Lean prover
Wikidata: Q6509476
Influenced: F*
Influenced by: Rocq
Programming paradigms: functional programming
Lean Influence Network
Pan and zoom the graph with your mouse or alternatively your fingers on touch devices.
Hello World in Lean
#print "Hello World"Source: github.com/leachim6/hello-world
Free Lean books, articles, documentation
- PureScript By Example - Phil Freeman
Search on GitHub
| Name | Description | Last pushed to | Open issues | Forks | Stars | Size |
|---|
Latest data update: 2025-08-21