20230821-Lean交互式定理证明器简介

唠唠闲话

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

证明辅助

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

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


安装及使用

参考官方教程

安装

  1. 下载并执行安装脚本

    1
    # 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
    echo 'export PATH="$HOME/.elan/bin:$PATH"' >> ~/.bashrcsource ~/.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
cp -r tutorials/src/exercises tutorials/src/my_exercisescode tutorials

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


在线使用链接:An introduction to Lean

演示视频

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

打赏
  • 版权声明: 本博客所有文章除特别声明外,著作权归作者所有。转载请注明出处!

扫一扫,分享到微信

微信分享二维码
  • Copyrights © 2015-2024 TeX_baitu
  • 访问人数: | 浏览次数:

请我喝杯咖啡吧~