Lean4 教程一 ｜ 基础安装

发表于 更新于 分类于 阅读次数： 字数： 897 时间 ≈ 3 分钟
Lean 是一个交互式定理证明器，也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。

唠唠闲话

Lean 是一个交互式定理证明器（Interactive Theorem Prover, ITP），也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。用于定理证明的编程语言还有很多，比如 Coq，isabelle，HOL Light 等，但相比之下，Lean 有更多优点且更契合数学习惯。

很多数学家选择使用 Lean 的标准库 mathlib 作为基础，这个仓库被称为未来的数学图书馆。

知乎上有不少关于 LEAN 的讨论，比如：如何评价 MSR 的 Lean Theorem Prover？，或者 计算机辅助证明简介。

LEAN4 的官方文档(Get started)提供了不同平台的安装方式，包括 Windows、MacOS 和 Ubuntu 系统，且都提供了一行脚本运行的方式。但在国内因为网络问题，通常要借助镜像站或手动安装。

当前教程针对 Ubuntu 系统 (TODO: 其他系统)。Windows 可以参考 子鱼的博客，Mac 系统可以按官网教程，使用 homebrew 来快速配置。

安装教程

如果没有网络问题，用一行命令安装：

1
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

该命令执行了一个脚本：install_debian.sh，脚本安装了 VsCode，LEAN 插件，以及 elan。

如果下载不了 GitHub 资源，在安装了 VsCode 和 LEAN 4 拓展后，脚本里只有 elan 是需要手动安装的。

安装 elan

elan 是一个用于管理 LEAN 环境的工具。它的功能类似于 Rust 的 rustup 或 Node.js 的 nvm，用于安装、管理和切换不同版本的 Lean。

在 GitHub release 页面根据系统版本下载新版 elan，比如 linux-x86_64 系统的 elan 安装器地址为：

1
https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz

如果不确定系统架构，执行 uname -s 和 uname -m 查看：

1
2
3
4
❯ uname -s
Linux
❯ uname -m
x86_64

下载文件并解压：

1
2
3
# 如果网络不行就本地下载再上传
curl https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
tar xf elan.tar.gz

解压得到 elan-init 文件，赋予可执行权限并执行：

1
2
chmod +x elan-init
./elan-init

完成后，在 .bashrc 或 .zshrc 中修改环境变量：

1
export PATH="$HOME/.elan/bin:$PATH"

重启终端，检查 elan 版本和默认安装的 Lean 版本：

1
2
3
4
5
❯ elan -V
elan 3.1.1 (71ddc6633 2024-02-22)
❯ elan show
stable (default)
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)

elan 的管理目录为 $HOME/.elan，内容形如

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
❯ tree .elan -L 2
.elan
├── bin
│   ├── elan
│   ├── lake
│   ├── lean
│   ├── leanc
│   ├── leanchecker
│   ├── leanmake
│   └── leanpkg
├── env
├── settings.toml
├── tmp
├── toolchains
│   └── stable
└── update-hashes
    └── stable

下载的 LEAN 版本在 toolchains 目录下，settings.toml 是 elan 的配置文件。

elan 的二进制文件中，lake 经常会用到。

Lake 管理器

lake 全称 Lean Make，是 LEAN4 的包管理器，已合并到 LEAN4 仓库，作为源码的一部分。

下边用一个简单的例子演示 lake 的基本用法。

创建项目，目录为 hello

1
2
3
4
# 创建包
lake new hello
## 或者
mkdir hello && cd hello && lake init hello

文件结构：

1
2
3
4
5
6
7
8
.
├── Hello
│   └── Basic.lean
├── Hello.lean
├── Main.lean
├── lake-manifest.json
├── lakefile.lean
└── lean-toolchain

文件说明：

  • lean-toolchain 记录 lean4 工具链的版本信息
  • lakefile.lean 定义构建配置和依赖管理，以及一些脚本
  • lake-manifest.json 文件，执行 lake build 构建依赖后生成，记录了包的依赖信息，类似于 nodejs 的 package.json

其他命令：

1
2
3
4
5
6
7
8
9
10
# 构建包
lake build
# 运行
lake exec hello # Hello, world!
# 清理构建文件
lake clean
# 更新依赖
lake update
# 运行 lakefile.lean 的脚本
lake run <script>