Lean (proof assistant)

Lean is an interactive theorem prover and dependently typed functional programming language originally developed by Leonardo de Moura at Microsoft Research beginning in 2013, designed to combine formal mathematical proof verification with a modern, fast, and extensible functional programming language usable for general software development. Lean's later major version, Lean 4, is notable for being substantially self-hosted, with much of its own compiler and tooling written in Lean itself, and the language has been adopted by a large mathematical community for the Mathlib project, an extensive, community-built formalized mathematics library.