Full description
The Lean theorem prover is a proof assistant developed principally
by Leonardo de Moura at Microsoft Research. Lean is a functional
programming language that makes it easy to write correct and
maintainable code. You can also use Lean as an interactive theorem
prover. Lean programming primarily involves defining types and
functions. This allows your focus to remain on the problem domain and
manipulating its data, rather than the details of programming.
Packages