Lean is an interactive theorem prover. It can verify proofs written in Lean by humans. Mathlib is a monolithic library of classical mathematics written in Lean. Mathematicians contributing to Mathlib love it because it has all the interconnected subdisciplines they need in one place, and most of them aren't huge fans of constructive mathematics or univalent mathematics.

Lean is also a strict pure functional programming language with dependent types. You can write correct and maintainable programs in Lean. You can also write proofs showing that a program terminates or it computes the desired answer, etc. Some computer scientists and programmers praise Lean's extensible syntax and editor support.

See also: https://leanprover.zulipchat.com/#narrow/stream/113488-gener...