Lean
Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types, the foundational type theory developed with the Coq theorem prover, which was renamed to Rocq in 2024. It is a free and open-source software project hosted on GitHub. Development is currently supported by the nonprofit Lean Focused Research Organization (FRO). Wikipedia
Created Year: 2013Designed by: Microsoft Research
Developed by: Microsoft Research • Leonardo de Moura
Operating systems: cross-platform
Implemented in: C • C++ • Lean
Aliases: Lean prover
Wikidata: Q6509476
Influenced: F*
Influenced by: Rocq prover
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 (HTML)
Search on GitHub
| Name | Description | Last pushed to | Open issues | Forks | Stars | Size |
|---|
Latest data update: 2026-10-26