Lean 定理证明器

出自 ArchWiki

Lean 定理证明器是一个由 Microsoft Research 的 Leonardo de Moura 主要开发的证明助手。Lean 数学库 mathlib 是一个社区驱动的努力，旨在构建一个在 Lean 证明助手中形式化的统一数学库。

Lean 的安装

使用 elan 安装 Lean 4

elan 是一个用于管理 Lean 定理证明器安装的工具。它有助于维护多个 Lean 并发版本。此外，由于 Lean 4 正在大力开发中，使用它通常需要安装 nightly build，使用 elan 可以轻松完成此操作。elan 将 Lean 安装在 $HOME/.elan/toolchains 的子目录中，并且不需要 root 访问权限。

安装 elan-leanAUR 软件包。

注意： 这些说明的其余部分解释了如何安装 Lean，但是如果您希望为现有项目（例如 mathlib）做出贡献，则 Lean 安装将自动处理，您可以跳至 项目管理 部分

要安装最新的 Lean 4 稳定版本，请使用

$ elan toolchain install leanprover/lean4:stable

但是，许多应用程序（包括使用 mathlib4）都需要 Lean 4 的开发版本。例如，mathlib4 正在使用的 Lean build 可以在文件 [1] 中找到。要安装所需的 build，请运行

$ elan toolchain install leanprover/lean4:build

其中 build 应替换为所需的 build。

可以使用以下命令列出已安装的 Lean 版本

$ elan show

可以使用以下命令选择默认版本

$ elan default build

使用 Lean 4 时，可以通过 cd 进入项目目录并创建一个文件来为给定项目覆盖默认 build

lean-toolchain
build

将 build 替换为适当的 build 标识符。

要获取当前 Lean build 中可执行文件的路径，请使用

$ elan which name_of_executable


通过 AUR 安装 Lean 3

安装 lean-community-binAUR 或 lean-communityAUR。

要安装 mathlib，您必须首先安装 python-mathlibtoolsAUR，这将安装 'leanproject'。

注意： python-mathlibtoolsAUR 不会安装 mathlib，只会安装下载 mathlib 所需的工具。

要安装 mathlib，您必须创建一个 Lean 项目

$ cd /path/to/project
$ leanproject new name_of_project

这会将 mathlib 下载到 /path/to/project/name_of_project/_target/deps/mathlib。

项目管理

在本节中，我们将描述如何创建 Lean 4 项目并为其做出贡献，包括 mathlib4。

项目结构

Lean 4 项目将包含多个用于管理项目的文件。

  • lakefile.lean：包含有关如何构建项目以及依赖项列表的信息。
  • lean-toolchain：一个单行文件，指定要用于项目的 build。
  • lake-manifest.json：一个自动生成的文件，其中包含有关每个已安装依赖项的特定版本的信息。如果您有 lake-manifest.json 文件，则运行 lake update 将下载 lake-manifest.json 中指定的依赖项版本。这对于避免不兼容的依赖项版本很有用。
  • .lake（或者，在早期版本的 Lean 4 中，是 lake-packages）：这是安装依赖项的位置。
  • build：存储构建的 Lean 文件的目录。
  • Lean 文件，包含 Lean 代码。

创建项目

要创建项目，请安装 elan 和 Lean build，如上面的 使用 elan 安装 Lean 4 部分所述。

注意： 在撰写本文时，稳定 build 不包含 lake，因此要运行以下代码，您需要安装较新的 build，例如 v4.3.0-rc2，并将其设置为默认值

接下来，运行

$ lake new path/to/project

这将创建一个默认的 lakefile.lean 和 lean-toolchain 文件。

这不会下载 mathlib，您可能想要这样做。Mathlib 是 Lean 项目的官方数学库，包含许多您可能需要的定义、引理和定理。如果您想将 mathlib 添加到您的项目中，则必须将其作为依赖项添加到 lakefile 中。有关详细信息，请参见下文。


管理项目

如果您正在处理现有项目，例如从互联网（例如 github）下载的项目，则无需单独安装 Lean，只要您安装了 elan，请参见上面的 使用 elan 安装 Lean 4 部分。只要项目存在适当的 lean-toolchain 文件，您就可以简单地运行

$ lake update

这将下载所需的 Lean 版本以及项目的所有依赖项。

可以通过编辑 lakefile.lean 文件来添加依赖项。例如，要将 mathlib 添加为依赖项，请添加行

lakefile.lean
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

到 lakefile.lean。接下来运行

$ lake update

以下载 mathlib，以及

$ lake exe cache get

以下载预编译库（请参阅下面的 缓存和 olean 文件 部分）。

为 Mathlib 贡献

如果您希望参与将大部分数学形式化的持续努力，您可能希望为 Mathlib 做出贡献，Mathlib 是 Lean 项目的官方数学库。

为此，您首先需要下载 mathlib

$ git clone https://github.com/leanprover-community/mathlib4.git

并 cd 到下载的目录并运行

$ lake update
$ lake exe cache get

如果您希望提交您的工作，您将需要在 mathlib Git 服务器上获取一个分支，并提交一个 pull request。要获取分支，请在 leanprover Zulip chat 上联系社区，介绍您自己和您的项目，并请求一个分支。

自动生成文档

可以自动生成文档，样式与 mathlib 文档 相同。这可以使用 doc-gen4 软件包完成。要安装它，请将其添加到您的 lakefile.lean 中

lakefile.lean
meta if get_config? env = some "dev" then require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"@"main"

（代码的 "dev" 部分确保仅当使用 -Kenv=dev 运行 lake 时才能构建文档，如下所示，以避免仅在尝试构建软件包时生成文档）并下载它

$ lake -Kenv=dev update

可以使用以下命令生成文档

$ lake -Kenv=dev build NameOfProject:docs

其中 NameOfProject 应替换为您的项目名称。这将生成文档并将其放置在 build/doc 目录中。然后，您可以通过在浏览器中打开 build/doc/index.html 来浏览文档。

注意： 不正式支持使用浏览器在本地打开文档文件。相反，建议启动 http 服务器，例如使用 python -m http.server
注意： doc-gen4 假定项目构建正确。如果在构建时出现任何错误，则文档将无法使用。在生成文档之前，请确保 lake build 退出时没有错误

文档还包括搜索功能。要在文档中搜索术语，请使用

file:///path/to/doc/find/index.html?pattern='search_term'#doc

文本编辑器

将 Lean 与 Emacs 一起使用

安装 lean-mode

要将 Lean 与 Emacs 一起使用，您必须安装 lean-mode 软件包。要从 MELPA 存储库安装它，请添加

.emacs
(require 'package)
(add-to-list 'package-archives
  '("melpa" . "https://melpa.org/packages/"))
(package-initialize)
(package-refresh-contents)

到您的 Emacs 配置文件 打开 Emacs，然后键入

M-x package-install RET
lean-mode RET

现在，在 Emacs 中打开扩展名为 .lean 的文件将自动在 Lean 模式下打开。

快捷键绑定

快捷键绑定列表可在 https://github.com/leanprover/lean-mode 上找到。

自动 Unicode 输入

Lean 使用 Unicode 符号作为其语言的一部分。lean-mode 可以通过将标准文本转换为 Unicode 字符来轻松处理此输入，例如，键入 \R 将解析为 Unicode 字符 ℝ。为此，需要选择 Lean 输入法。可以通过将以下内容添加到您的 Emacs 配置文件 来自动完成此操作

.emacs
(add-hook 'lean-mode-hook
  (lambda () (set-input-method "Lean")))

在单独的缓冲区中查看目标

在 Lean 中编写证明时，跟踪“目标”非常有用。可以使用 C-c C-b 快捷键直接在 Emacs 中查看目标，这将打开一个新的缓冲区，其中显示目标。通过添加

.emacs
(add-hook 'lean-mode-hook 'lean-toggle-show-goal)

到您的 Emacs 配置文件，也可以在编辑 .lean 文件时自动打开此缓冲区。

将 Lean 与 Neovim 一起使用

安装 lean.nvim

要将 Lean 与 Neovim 一起使用，您必须安装 lean.nvim 插件。这可以使用 vim-plug 轻松完成，方法是将以下内容添加到您的 Neovim 配置文件

init.vim
call plug#begin()

...

Plug 'Julian/lean.nvim'
Plug 'neovim/nvim-lspconfig'
Plug 'nvim-lua/plenary.nvim'

...

call plug#end()

打开 nvim，然后键入

:PlugInstall

如果您使用的是 Lean 3，您还需要安装 lean-language-serverAUR。（语言服务器内置于 Lean 4 中，因此对于 Lean 4 安装不是必需的）。

接下来，在 $XDG_CONFIG_HOME/nvim/plugin/lean.lua 创建一个配置文件

$XDG_CONFIG_HOME/nvim/plugin/lean.lua
require('lean').setup{
 abbreviations = { builtin = true },
 mappings = true,

}

abbreviatons 启用 Unicode 字符的缩写，mappings 启用许多有用的快捷键绑定，有关完整列表，请参见 https://github.com/Julian/lean.nvim/。更多配置选项可在 https://github.com/Julian/lean.nvim/ 中找到。

技巧和窍门

缓存和 olean 文件

为了使用 mathlib 中的定理和引理，需要构建（即编译）mathlib。这是一个漫长的过程。为了避免这种情况，mathlib 社区提供了一个预编译的 mathlib 文件（也称为“oleans”）存储库。要使用 Lean 4 下载它们，请使用

$ lake exe cache get

并使用 Lean 3，请使用

$ leanproject get-cache
注意： 为了使用 olean 文件，它们必须已使用与项目使用的 Lean 版本相同的版本（如果您使用的是 nightly build，则为相同的 nightly build）预编译。

使用 Lean 4 时，确保项目始终使用与 mathlib 相同的版本的一种简单方法是将 mathlib lean-toolchain 文件链接到项目目录

$ ln -sf lake-packages/mathlib/lean-toolchain ./
$ lake update

Lean 文档

学习 Lean 4 中定理证明的一个很好的资源是 [2]。特别值得注意的是，从 [3] 可以获得 Lean 4 中定理证明的有用命令的简洁“速查表”。

Lean 4 中 mathlib 的文档可在 [4] 中找到。

由于文档仍然相当稀疏，因此直接向 Lean 社区提出问题通常会更有效率。最受欢迎的论坛是 leanprover Zulip chat。

Retrieved from "https://wiki.archlinux.org.cn/index.php?title=Lean_Theorem_Prover&oldid=814994"