Skip to main content

Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.

Questions with this tag will be relayed to the Lean Zulip Forum stream
Newest questions tagged lean - Proof Assistants Stack Exc...

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.

References:

Related tags