形式化数学——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的方法。
-
安装VS代码。
-
启动VS Code，通过单击“扩展”侧边栏条目并搜索“Lean 4”来安装
Lean 4扩展。
-
通过使用创建新文本文件来打开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'.
-
遵循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 的回复格式如下:
8Lean 返回的错误消息格式如下:
application type mismatch add1 "seven"argument "seven"has type String : Typebut is expected to have type Nat : Type
警告格式如下:
declaration uses 'sorry'Unicode
惯用的Lean代码会使用各种不属于ASCII的Unicode字符。
本文参考
David Thrane Christiansen, 《Lean on functional programming》
Lean-zh 项目组，译
Lean 手册