形式化数学——Lean的介绍与安装

Lean是Microsoft Research开发的交互式定理证明器，基于依值类型论。依值类型论将程序和证明的世界统一了起来，因此Lean也是一门编程语言。Lean认真地对待其双重性质，并且被设计为适合作为通用编程语言使用，Lean甚至是用它自己实现的。

作为一门编程语言，Lean是一种具有依值类型的严格纯函数式语言。学习使用Lean编程很大一部分内容在于学习这些属性是如何影响程序编写方式的，以及如何像函数式程序员一样思考。

严格性(Strictness) 意味着Lean中的函数调用与大多数语言中的工作方式类似：在函数体开始运行之前，参数会被完全计算。
纯粹性(Purity) 意味着Lean程序除非明确声明，否则无法产生副作用，例如修改内存中的位置、发送电子邮件或删除文件等。Lean是一种函数式(Functional) 语言， 这意味着函数就像任何其他值一样是一等值， 并且执行模型受数学表达式的求值启发。依值类型(Dependent type)是Lean最不寻常的特性，它使类型成为语言的一等部分， 允许类型包含程序，而程序计算类型。

在编写并运行Lean所编写的程序之前，你需要在自己的计算机上设置 Lean。Lean工具包括以下内容：

elan :用于管理 Lean 编译器工具链，类似于 rustup 或 ghcup 。
lake :用于构建 Lean 包及其依赖项，类似于 cargo 、 make 或 Gradle。
lean :用于对 Lean 文件进行类型检查和编译，并向程序员工具提供当前正在编写的文件的相关信息。通常lean是由其他工具而非用户直接调用的。
 

编辑器插件，如 Visual Studio Code 或 Emacs，可与 Lean 通信并方便地显示其信息。

这些说明将引导您将Lean 4与VS Code一起设置为Lean 4的编辑器。请参阅设置，了解支持的平台和其他设置Lean 4的方法。

1. 安装VS代码。

2. 启动VS Code，通过单击“扩展”侧边栏条目并搜索“Lean 4”来安装Lean 4扩展。

   

3. 通过使用创建新文本文件来打开Lean 4设置指南'File > New Text File' (Ctrl+N/ Cmd+N), clicking on the ∀-symbol in the top right and selecting 'Documentation… > Docs: Show Setup Guide'.

   

4. 遵循Lean 4设置指南。 它将：

   引导您浏览精益学习资源，

   教你如何在平台上设置Lean的依赖性，

   单击按钮即可为您安装Lean 4，

   帮助你设置你的第一个项目。

   

---

支持的平台

由CI构建和测试的平台，通过elan作为二进制版本提供（见下文）

• x86-64 Linux与glibc 2.26+

• x86-64 macOS 10.15+

• aarch64（苹果硅）macOS 10.15+

• x86-64 Windows 11（任何版本）、Windows 10（版本1903或更高版本）、Windows Server 2022、Windows Server 2025

平台交叉编译，但未经过CI测试，可作为二进制版本提供

由于缺乏自动测试，发布可能会被无声破坏。欢迎问题报告和修复。

• aarch64 Linux与glibc 2.27+

• x86（32位）Linux

• Emscripten网络组件

设置Lean

另请参阅以VS Code作为编辑器的标准设置的快速启动说明。

所有受支持平台的发布版本可在<https://github.com/leanprover/lean4/releases>上找到。然而，与其下载这些并手动设置路径，不如使用精益版本管理器elan：

$ elan自我更新#，以防你有一段时间没有更新elan#下载并激活最新的Lean 4稳定版本（https://github.com/leanprover/lean4/releases）$ elan默认leanprover/lean4:稳定

lake

Lean 4附带一个名为lake的软件包管理器。使用lake init foo初始化当前目录中的精益包foo，并使用lake build进行类型检查和构建它及其所有依赖项。Uselakelake help了解进一步的命令。软件包foo的一般目录结构是

lakefile.lean # 软件包配置精益工具链#指定要使用的精益版本Foo.lean #主文件，通过`import Foo`导入foo/A.lean #进一步的文件，通过例如`import Foo.A`导入A/... # 进一步嵌套.lake/ # `lake` 构建输出目录

运行lake build后，您将看到一个名为的二进制文件./.lake/build/bin/foo，当你运行它时，你应该会看到输出：

Hello, world!

编辑

Lean实现了语言服务器协议，可用于Emacs、VS Code和其他编辑器中的交互式开发。

必须保存更改才能在其他文件中显示，然后必须使用编辑器命令使这些文件无效（请参阅上面的链接）。

---

排版约定

作为输入提供给 Lean 的代码示例格式如下:

def add1 (n : Nat) : Nat := n + 1#eval add1 7

上面最后一行(以 #eval 开头)是指示 Lean 计算答案的命令。Lean 的回复格式如下:

8

Lean 返回的错误消息格式如下:

application type mismatch    add1 "seven" argument    "seven" has type    String : Type but is expected to have type    Nat : Type

警告格式如下:

 declaration uses 'sorry'

Unicode

惯用的Lean代码会使用各种不属于ASCII的Unicode字符。

---

本文参考

David Thrane Christiansen, 《Lean on functional programming》

Lean-zh 项目组，译

Lean 手册

---