01
Lean: From Interactive Theorem Proving to a Community Library of Formal Mathematics
Lean combined a small dependent-type-theory kernel with extensible proof automation and a practical functional programming language, then grew through Mathlib into a major community platform for machine-checked mathematics.
↗