Lean if a theorem prover and programming language based on the calculus of constructions with inductive types.
Here is a interactive introduction to Lean.
Table of Content