这篇博客是 2021 年写的，近期(2023)做了更新，由于 ChatGPT 的出现，一些原来没有填的坑这里也顺便写了。特别留意，教程部分内容来自 ChatGPT 的回答。

唠唠闲话

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

证明辅助

Lean 的百科词条名为 Lean(proof assistant)，说明了 Lean 的主要作用是辅助推导，而非完全的自动证明。但有一点注意，计算机证明依照严格的类型论逻辑，结论远比手推可靠（由哥得尔不完备定理，数学没有绝对的正确）。未来如果能结合自动推导，或许会给数学带来新的革命。

相关阅读
LEAN 官方文档：LEAN
知乎：Lean 的前世今生
知乎：如何评价 MSR 的 Lean Theorem Prover？
知乎：计算机辅助证明简介
量子位：菲尔兹奖得主舒尔茨没做到的事，现在被计算机证明了
B站：Kevin Buzzard 关于未来数学的演讲

安装及使用

参考官方教程。

安装

  1. 下载并执行安装脚本

    1
    2
    3
    4
    5
    # wget 下载 .sh 脚本
    wget https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh

    # bash 运行脚本
    bash install_debian.sh

    安装完成：
    20230404212545

  2. 该脚本同时也自动安装了 LEAN 的 VsCode 扩展，新建 .lean 文件，用 vscode 打开测试一下代码

    1
    #check "Hello world!"

    正确安装的显示内容如下
    20230404221926

注：下载脚本默认抑制了输出，有可能因下载失败导致安装不完整，但报错信息没有被输出。所以执行脚本时，需确保能正常连接 GitHub

可能的问题

  1. 如果 vscode 提示插件获取失败，则使用下边命令

    1
    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh && echo && read -n 1 -s -r -p "Press any key to start Lean" && exit

    这个是旧笔记写的内容，目前没遇到

  2. 如果安装后，提示执行 elan default stable，可能是因为没有设置环境变量，执行下边命令即可

    1
    2
    echo 'export PATH="$HOME/.elan/bin:$PATH"' >> ~/.bashrc
    source ~/.bashrc

  3. Mac Intel 系统使用下边脚本进行安装：

    1
    /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)"

    Windows 系统暂不考虑，应该比较简单。Mac M1 系统设置相对麻烦，这里也不考虑了。

基本使用

leanproject

leanproject 是 Lean 语言的官方命令行工具，用于创建、管理和构建 Lean 项目。使用 leanproject，您可以轻松地开始一个新的 Lean 项目，将其提交到 GitHub 或 GitLab 上的版本控制存储库，并与其他人协作开发项目。

leanproject 提供了多种实用功能，例如：

  • 创建 Lean 项目并自动下载依赖项（如 Lean Mathlib 工具包）。
  • 将本地 Lean 项目发布到 GitHub 或 GitLab 上的存储库中。
  • 向 Lean 项目添加文件和目录，包括 .lean、.olean 和 .leanpkg.toml 等文件。
  • 构建 Lean 项目并生成 PDF 文档。
  • 执行 Lean 文件中的测试，并输出测试结果。

除此之外，leanproject 还允许用户自定义 Lean 配置文件，例如更改 Lean 编译器、Mathlib 版本或 Lean 输出格式等选项。

使用教程

LEAN3 教程手册

使用 leanproject 下载练习题：

1
leanproject get tutorials

下载包括了一些常用库，文件可能比较大
20230404222149

将练习题复制到 src 目录下

1
2
cp -r tutorials/src/exercises tutorials/src/my_exercises
code tutorials

参考答案在 tutorials/src/solutions 目录下，可以对照练习。

在线使用链接：An introduction to Lean。

演示视频

使用教程待更新，演示视频：素数无穷多。

LEAN 4 教程