Lean（定理证明器）

概述

Lean 是一门基于依赖类型论的函数式编程语言兼交互式定理证明器，由 Leonardo de Moura 在微软研究院发起，现由 Lean FRO 基金会主导开发，当前主版本为 Lean 4。

特点

Lean 4 将「证明助手」与「通用编程语言」统一：编译器和大部分系统本身用 Lean 编写，支持元编程与可扩展语法，证明与程序共用同一套语言。其理论基础与 Coq 同属构造演算一系。

mathlib 与数学形式化

社区维护的 mathlib 是规模庞大的形式化数学库，覆盖从基础代数到现代数学的大量内容，吸引了众多职业数学家参与，多个前沿数学成果的机器验证项目选择在 Lean 中进行。

应用

除数学形式化外，Lean 也被用于程序验证研究，并成为 AI 自动定理证明研究的常用目标系统。