Lean – a proof assistant and a functional programming language
lean-lang.org