Lean is a programming language with dependent types that is popular for the formalisation of mathematics (using the old version, Lean 3). The latest version (Lean 4) is also suitable for writing functional programs (similarly to Haskell).