Lean 4是由微软研究院开发的开源函数式编程语言与交互式定理证明器，是Lean语言的第四代版本。它将编程语言与形式化数学验证能力融为一体，支持依值类型系统（dependent type theory），可用于构建数学证明、验证程序正确性以及开发通用软件。Lean 4在数学形式化社区（如Mathlib项目）中被广泛使用，具备元编程、宏系统及高性能编译等特性。