Lean Prover

Lean 是一种基于依赖类型理论的函数式编程语言和交互式定理证明器。依赖类型理论将程序与证明的世界统一起来，因此 Lean 也是一种编程语言。Lean 重视其双重特性，旨在作为通用编程语言使用——Lean 甚至用自身实现。
Lean 由微软研究院于 2013 年开发，最初旨在帮助数学家和工程师解决复杂的数学问题。Lean 是一个用于形式化数学（也称机器可检查数学）的开源开发环境，全球活跃的数学家社区广泛使用并持续贡献于此。