Lean4

Lean 是微软研究院在 2013 年推出的计算机定理证明器。Lean 4 于 2021 年发布，为 Lean 定理证明器的重新实现，能够生成 C 代码后进行编译，以便开发高效的特定领域自动化。其兼具数学和编程两方面的特性，数学家可以将数学定理转换成代码，并严格验证这些定理的正确性；也具有依赖类型的严格的纯函数式语言性质。