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