Lean
Interactive theorem prover and functional programming language — increasingly popular for formalising mathematics.
static
compiled
since 2013
functionaldependent-types
Lean 4 is both a proof assistant and a full-featured functional programming language with dependent types. The Mathlib library contains tens of thousands of formalised mathematical results. Projects like the Liquid Tensor Experiment demonstrated that professional mathematicians can use Lean to formalise cutting-edge research, driving significant growth in its community.