Lean 语言参考手册🔗

这是Lean语言参考手册。它旨在对Lean进行全面而精确的描述，是Lean用户查找详细信息的参考资料，而不是给新用户的入门教程。如需其他文档，请参阅Lean文档总览(英文) 或 lean中文文档。本手册涵盖Lean 4.21.0-rc3版本。

Lean是一种基于依值类型论的交互式定理证明器，既可用于前沿数学也可用于软件验证。 Lean的核心类型理论(core type theory)足够丰富，能够描述非常复杂的数学对象，但又足够简单，允许有独立实现，从而降低影响健全性的bug风险。核心类型理论通过一个最小的内核(kernel)实现，内核除了校验证明项外不做其他任何事情。这一核心理论与内核由高级自动化机制支持，该机制体现在一种富有表现力的策略语言之中。每个策略都会产生一个核心类型理论中的项，由内核检查，因此即使策略中出现bug，也不会威胁到整个Lean的健全性。除了许多其他Lean组件外，策略语言也是用户可扩展的，因此能根据形式化项目的需求不断完善。策略本身用Lean编写，定义后即可使用，无需重建证明器或加载外部模块。

Lean同时也是一种纯函数式编程语言，具有基于引用计数的运行时系统，能够高效处理打包数组结构、多线程和单子IO等特性。作为一门编程语言，Lean主要由自身实现，包括语言服务器、构建工具、繁释器和策略系统。本手册正是用Verso编写的，Verso是用Lean开发的文档创作工具。

熟悉Lean的编程特性，即使对主要关注证明编写的用户来说也非常有价值，因为Lean程序用于实现新的策略和证明自动化。因此，本参考手册不会人为地将两者分开描述，而是将它们合在一起讲解，以便互为补充，相互启发。

Lean 语言参考手册🔗

Contents