Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. 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: 2013
Designed 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 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"

Free Lean books, articles, documentation

• PureScript By Example - Phil Freeman (HTML)

Search on GitHub