从数学证明到代码：LeanDojo如何用机器学习自动化定理证明

1. 从数学证明到代码：为什么我们需要 LeanDojo？

如果你接触过形式化验证或者定理证明，大概率听说过 Lean 这个名字。它不仅仅是一个编程语言，更是一个交互式定理证明器。简单来说，你可以用它把数学定理写成代码，然后让计算机来验证你的证明每一步都是严丝合缝、逻辑正确的。这听起来很酷，对吧？但现实是，在 Lean 里写证明，尤其是面对 mathlib（Lean 庞大的数学库）里那些复杂的定理时，门槛相当高。你需要精确地知道在当前的证明状态下，该使用哪个定理（在 Lean 里叫“前提”或“引理”），以及该调用哪个策略（tactic）来推进证明。

这就引出了一个核心问题：这个过程能否自动化，或者至少得到智能辅助？这正是机器学习，特别是大语言模型（LLM）可以大显身手的地方。想象一下，有一个模型可以像经验丰富的数学家一样，观察当前的证明目标，从成千上万个已知定理中快速检索出最相关的几个，并建议下一步该用什么策略。这不仅能帮助新手学习，也能极大提升专业研究者的效率。

LeanDojo 就是为了搭建这座桥梁而生的。它不是一个独立的证明器，而是一个 Python 工具包，专门为“基于机器学习的定理证明”这个场景服务。它的核心价值在于两件事：第一，它能从 Lean 的代码仓库（比如 mathlib4）里高效地、结构化地提取训练数据，包括证明状态、使用的策略、依赖的前提等等；第二，它提供了一个程序化接口，让你的 Python 代码能够像人类用户一样与 Lean 交互，提交策略、获取新的证明状态。这样一来，研究人员就可以方便地构建数据集、训练模型，并评估模型在真实定理证明任务上的性能。

我最初接触 LeanDojo 是为了尝试复现一些检索增强证明的论文。在摸索过程中发现，虽然它的概念很前沿，但想要真正用起来，光看官方文档和论文是不够的，有很多环境配置、数据提取的细节和实际使用的“坑”需要趟过去。这篇文章，我就结合自己的实践，带你深入拆解 LeanDojo，从设计理念、环境搭建、核心功能使用到实战中的经验技巧，让你能快速上手这个强大的工具。

注意：本文主要基于 LeanDojo 最初的版本进行剖析，其设计思想和核心架构具有很高的参考价值。原仓库现已标记为 deprecated，官方推荐使用全新的 LeanDojo-v2 。但理解 v1 的运作机制是掌握 v2 乃至整个技术脉络的坚实基础。下文中的操作如无特别说明，均指代原版 LeanDojo。

2. LeanDojo 核心架构与设计哲学解析

在开始敲命令之前，我们有必要先理解 LeanDojo 是怎么工作的。它的设计不是凭空而来的，而是紧密围绕“为机器学习提供燃料和试验场”这个目标展开的。

2.1 数据提取：把证明过程变成可学习的样本

机器学习需要数据，而对于定理证明来说，数据就是一个个已经完成的证明过程。Lean 的.lean文件里包含了定理的陈述和证明脚本，但这对于模型来说还是太“原始”了。LeanDojo 的数据提取器（Data Extractor）扮演了“解剖师”的角色，它的任务是把一个线性的证明脚本，还原成一系列“状态-动作”对。

这个过程大致是这样的：LeanDojo 会启动一个 Lean 进程，然后逐步执行证明文件中的每一个策略（tactic）。每执行一步前，它会记录下当前的“证明状态”（Goal State），也就是需要证明的子目标是什么，有哪些可用的假设。执行完这一步策略后，它再记录下这个策略是什么，以及这个策略成功应用所依赖的“前提”（Premises）——也就是具体调用了 mathlib 中的哪个定理或定义。这样，一个完整的证明就被分解成了(证明状态, 所用策略, 所需前提)这样的三元组序列。这些三元组正是训练模型的核心样本，模型学习的目标就是：给定一个证明状态，预测出下一步应该采取的策略以及可能需要检索的前提。

这里有个关键细节：提取“前提”并不是简单地解析代码文本。LeanDojo 需要与 Lean 的编译器/服务器（Lean Infoverse）深度交互，获取策略执行时实际访问到的内核级对象信息，从而精确地定位到前提在 mathlib 中的具体位置（文件、行号、名称）。这种精确性对于后续的检索任务至关重要。

2.2 程序化交互：让 Python 成为 Lean 的遥控器

数据提取是“回放”历史，而程序化交互（Programmatic Interaction）则是“直播”未来。这是 LeanDojo 另一个核心组件：交互式环境（Interactive Environment）。它允许你的 Python 脚本创建一个 Lean 工作区，加载特定的定理，然后以编程方式不断地尝试各种策略。

这个环境的工作原理是封装了 Lean 的lean --server模式。Lean 服务器运行在后台，通过标准输入输出（stdin/stdout）或更高效的网络协议与前端通信。LeanDojo 的 Python 客户端则实现了与这个服务器的通信协议。你可以通过它发送“运行到某一行”、“在当前状态执行某个策略”等命令，并接收服务器返回的新的证明状态、错误信息或成功信号。

这个设计的美妙之处在于，它为机器学习模型提供了一个标准的、可重复的测试平台。你可以把训练好的模型接入这个环境，让模型根据当前状态生成策略建议，由环境执行并反馈结果，从而评估模型的证明成功率、平均步骤数等指标。这完全模拟了人类在编辑器（如 VS Code 的 Lean 插件）中交互证明的过程。

2.3 版本管理：与 Lean 生态共舞

Lean 语言本身和 mathlib 库都在快速迭代。LeanDojo 必须处理好版本兼容性问题。它通过依赖elan（Lean 的工具链管理器）来动态切换和管理不同版本的 Lean。在数据提取或运行交互环境时，LeanDojo 会根据项目配置的leanpkg.toml或lakefile.lean文件，自动使用elan切换到正确的 Lean 版本和对应的包依赖。

这种设计使得 LeanDojo 能够处理不同时间点的 Lean 仓库快照，例如为特定的研究论文提取固定版本的数据集（如 LeanDojo Benchmark）。对于研究者来说，这意味着实验的可复现性得到了保障。

3. 实战入门：搭建你的 LeanDojo 工作环境

理论讲完了，我们动手把环境搭起来。官方推荐使用 Linux 或 macOS，Windows 用户可以通过 WSL2 获得接近原生的体验。以下步骤我都在 Ubuntu 22.04 和 WSL2 (Ubuntu) 环境下验证过。

3.1 基础依赖安装

首先，确保系统有基本的编译工具和 Git。

# 对于 Ubuntu/Debian sudo apt update sudo apt install -y build-essential curl git wget python3-pip python3-venv # 检查 Git 版本，需 >= 2.25 git --version

接着安装elan。它是管理 Lean 多版本的工具，类似于 Rust 的rustup。

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

安装完成后，重启你的终端，或者执行source $HOME/.bashrc（或对应 shell 的配置文件）。然后运行elan show应该能看到默认安装的 Lean 版本。

3.2 配置 GitHub 访问令牌

因为 LeanDojo 在运行时会自动克隆 Lean 相关的 Git 仓库（如 mathlib4），而 GitHub 对匿名克隆有速率限制。为了避免中途失败，必须配置一个 Personal Access Token (PAT)。

1. 登录你的 GitHub 账号，进入Settings->Developer settings->Personal access tokens->Tokens (classic)。
2. 点击Generate new token (classic)。给它一个描述性的名字（如 “LeanDojo”），在权限（scopes）部分，只需要勾选repo和read:packages就足够了。过期时间可以设置成 “No expiration”（非生产环境可选，方便些）。
3. 生成后，务必立即复制这个 token，关闭页面后就看不到了。

然后，将这个 token 设置为环境变量。建议写入你的 shell 配置文件（如~/.bashrc或~/.zshrc），这样每次打开终端都有效。

# 将 YOUR_GITHUB_TOKEN 替换为你刚才复制的真实 token echo 'export GITHUB_ACCESS_TOKEN="YOUR_GITHUB_TOKEN"' >> ~/.bashrc source ~/.bashrc # 验证是否设置成功 echo $GITHUB_ACCESS_TOKEN

重要安全提示：这个 token 具有读取你所有仓库的权限。请妥善保管，不要上传到公开的代码仓库或分享给他人。如果意外泄露，立即去 GitHub 上撤销它。

3.3 安装 LeanDojo Python 库

官方推荐使用 Python 3.9 到 3.12 的版本。我强烈建议使用虚拟环境（venv）来管理依赖，避免污染系统 Python 环境。

# 创建一个新的虚拟环境，例如在项目目录下 python3 -m venv leandojo_venv # 激活虚拟环境 source leandojo_venv/bin/activate # Linux/macOS # 如果是 Windows PowerShell，则使用： leandojo_venv\Scripts\Activate.ps1 # 升级 pip 和 setuptools pip install --upgrade pip setuptools wheel # 安装 LeanDojo pip install lean-dojo

安装过程会自动拉取一些必要的依赖。如果一切顺利，运行python -c "import lean_dojo; print(lean_dojo.__version__)"应该能打印出版本号。

3.4 验证安装与常见踩坑点

安装完成后，不要急着跑复杂例子。我们先做一个最简单的验证，确保核心交互功能是通的。LeanDojo 提供了一个快速验证脚本的思路，我们可以自己实现一个最小化测试。

创建一个 Python 脚本test_basic.py：

import os from lean_dojo import * # 1. 指定一个要交互的定理。我们用一个 mathlib4 中极其简单的例子。 # 这里使用一个已知存在的仓库和文件路径。mathlib4 的 URL 和 commit。 repo_url = "https://github.com/leanprover-community/mathlib4" commit = "29dcec074de168ac2bf835a77ef68bbe069194c5" # 一个较旧的稳定 commit file_path = "Mathlib/Data/Nat/Basic.lean" # 我们尝试定位一个非常简单的定理，比如 `Nat.succ_ne_self` theorem_name = "Nat.succ_ne_self" try: # 2. 连接到仓库和定理 repo = LeanGitRepo(repo_url, commit) theorem = Theorem(repo, file_path, theorem_name) print(f"Theorem loaded: {theorem}") # 3. 创建交互环境 with Dojo(theorem) as (dojo, init_state): print(f"Initial proof state: {init_state}") # 尝试一个最简单的策略：`rfl`（自反性），但这个定理可能不适用。 # 我们换一个更通用的策略 `intro h`，尝试引入假设。 tactic = "intro h" result = dojo.run_tactic(init_state, tactic) if result is None: print("Tactic failed or state didn't change as expected.") else: new_state, _, _ = result print(f"New state after `{tactic}`: {new_state}") except Exception as e: print(f"An error occurred: {type(e).__name__}: {e}") import traceback traceback.print_exc()

运行这个脚本：python test_basic.py。你可能会遇到以下几种情况：

1. 成功：看到输出了定理信息和初始状态。这是最理想的情况。
2. 网络错误/克隆仓库失败：检查你的GITHUB_ACCESS_TOKEN是否设置正确，网络是否通畅。第一次运行会克隆整个 mathlib4 仓库，可能需要较长时间和数 GB 磁盘空间。
3. Lean 版本不匹配错误：提示类似 “Lean version X.X.X not found”。这是因为指定的 mathlib4 commit 需要特定版本的 Lean。LeanDojo 和elan会自动处理，但可能需要下载。确保网络畅通，耐心等待。
4. 导入错误或模块找不到：可能是虚拟环境问题，或者 LeanDojo 库没有正确安装。尝试重新安装，并确保在激活的虚拟环境中操作。

我踩过的一个大坑：在 WSL2 中，如果你的项目路径位于 Windows 文件系统（如/mnt/c/...），可能会因为文件系统权限或性能问题，导致 Lean 服务器启动异常。最佳实践是将项目完全放在 WSL2 的 Linux 原生文件系统内（如~/projects/）。

4. 深入核心功能：数据提取与交互环境实战

环境搞定后，我们来深入两个核心功能，看看它们在实际项目中如何运用。

4.1 数据提取实战：构建自己的微调数据集

假设你想研究某个特定数学分支（如实数分析）的定理证明，希望从 mathlib4 中提取相关文件来训练一个更专业的模型。LeanDojo 的lean_dojo.data_extraction模块就是干这个的。

下面是一个示例脚本，展示如何提取单个文件中的所有证明步骤：

import json from pathlib import Path from lean_dojo import * from lean_dojo.data_extraction import * # 配置 repo_url = "https://github.com/leanprover-community/mathlib4" commit = "29dcec074de168ac2bf835a77ef68bbe069194c5" target_file = "Mathlib/Analysis/Calculus/Deriv/Basic.lean" # 一个分析学相关的文件 output_dir = Path("./extracted_data") output_dir.mkdir(parents=True, exist_ok=True) # 初始化仓库对象 repo = LeanGitRepo(repo_url, commit) # 提取单个文件 print(f"Extracting from {target_file}...") try: # extract_file 会返回一个生成器，产出每个定理的提取结果 extracted_data = list(extract_file(repo, target_file)) print(f"Successfully extracted {len(extracted_data)} theorems/definitions from {target_file}.") # 保存结果 output_file = output_dir / f"{Path(target_file).stem}.jsonl" with open(output_file, 'w') as f: for data in extracted_data: # data 通常包含定理名称、完整证明、以及分解后的步骤 # 我们需要将其转换为可序列化的格式 serializable_data = { "file_path": target_file, "theorem_name": data.get("theorem_name", "unknown"), "proof_steps": data.get("proof_steps", []), # 这是一个列表，包含状态、策略、前提 # ... 其他你感兴趣的字段 } f.write(json.dumps(serializable_data) + '\n') print(f"Data saved to {output_file}") except Exception as e: print(f"Failed to extract {target_file}: {e}") import traceback traceback.print_exc()

这个脚本会遍历指定文件中的每个定理或定义，将其证明过程分解。extracted_data中的每一项可能包含非常丰富的信息。你需要仔细查看lean_dojo.data_extraction模块的文档或源码，了解其返回的具体数据结构，以便按需处理。

一个重要提示：全量提取整个 mathlib4 非常耗时，可能需要数小时甚至更久，并且会产生巨大的中间文件。建议在拥有足够磁盘空间（>50GB）和良好性能的机器上进行。更好的策略是只提取你关心的那部分文件或目录。你可以使用extract_repo函数并配合过滤条件。

4.2 交互环境实战：模拟一个自动证明智能体

交互环境是评估证明模型的核心。下面我们模拟一个极其简单的“智能体”：它面对一个证明目标时，只会随机从一个小策略库中选取一个策略尝试。虽然愚蠢，但可以帮你理解整个交互循环。

import random from lean_dojo import * # 策略池（非常基础） TACTIC_POOL = [ "intro", "apply", "exact", "simp", "rfl", "contradiction", "assumption", ] def simple_proving_agent(theorem, max_steps=20): """一个简单的随机策略证明智能体""" with Dojo(theorem) as (dojo, init_state): current_state = init_state proof_trace = [] # 记录证明路径 print(f"Starting to prove: {theorem}") print(f"Initial goal: {current_state.goals}") for step in range(max_steps): if not current_state.goals: # 没有目标了，证明成功！ print(f"🎉 Theorem proved in {step} steps!") print(f"Proof trace: {proof_trace}") return True, proof_trace # 随机选择一个策略 tactic = random.choice(TACTIC_POOL) print(f"Step {step+1}: Trying tactic `{tactic}`") try: result = dojo.run_tactic(current_state, tactic) if result is None: print(f" -> Tactic `{tactic}` failed.") # 失败后可以尝试其他策略，这里我们简单跳过 else: new_state, _, _ = result if new_state != current_state: # 状态确实改变了 current_state = new_state proof_trace.append(tactic) print(f" -> Success. New goals: {current_state.goals}") else: print(f" -> Tactic succeeded but state unchanged.") except Exception as e: print(f" -> Error executing tactic: {e}") # 达到最大步数仍未证明 print(f"❌ Failed to prove after {max_steps} steps. Remaining goals: {current_state.goals}") return False, proof_trace # 使用一个简单的定理进行测试 repo_url = "https://github.com/leanprover-community/mathlib4" commit = "29dcec074de168ac2bf835a77ef68bbe069194c5" file_path = "Mathlib/Data/Bool/Basic.lean" theorem_name = "Bool.not_not_eq" # 一个简单的定理：¬¬b = b repo = LeanGitRepo(repo_url, commit) theorem = Theorem(repo, file_path, theorem_name) success, trace = simple_proving_agent(theorem)

运行这个脚本，你会看到智能体在盲目地尝试策略，大概率会失败。但这演示了核心循环：获取状态 -> 选择策略 -> 执行 -> 更新状态。一个真正的机器学习模型（如 ReProver）会在这个循环中，用神经网络来替换random.choice，根据当前状态和历史信息智能地选择策略和检索前提。

4.3 与检索器（Retriever）集成

LeanDojo 的强大之处在于它强调了“检索增强”。证明过程中，模型常常需要引用已有的定理。LeanDojo Benchmark 提供了所有前提的索引。在你的模型中，你可以加载这个索引，当模型需要时，快速检索出与当前证明目标最相关的几个前提。

虽然原版 LeanDojo 库不直接包含检索模型，但它提供了数据接口。通常的流程是：

1. 从 LeanDojo Benchmark 下载前提的嵌入向量（embeddings）和索引。
2. 使用向量数据库（如 FAISS）或检索库加载索引。
3. 在交互证明的每一步，将当前的证明状态编码成向量，去索引中搜索最相似的 N 个前提。
4. 将这些前提作为额外上下文，与证明状态一起输入给策略预测模型。

这个过程在 ReProver 项目 中有完整的实现。如果你要构建自己的检索增强证明器，ReProver 的代码是极好的起点。

5. 常见问题、故障排查与性能调优

在实际使用 LeanDojo 的过程中，你肯定会遇到各种问题。下面我整理了一些典型问题和解决方法。

5.1 环境与依赖问题

问题：安装lean-dojo时编译扩展失败（特别是multiprocess相关依赖）。排查：这通常是因为系统缺少 Python 开发头文件或 C 编译器。确保安装了python3-dev和build-essential。解决：

sudo apt install -y python3-dev build-essential # 然后重新安装 pip install lean-dojo

问题：运行时报错elan: command not found。排查：elan没有正确安装或没有加入 PATH。解决：重新运行elan-init.sh脚本，并确保终端配置已重载（source ~/.bashrc）。可以运行which elan检查。

问题：克隆 mathlib4 仓库时速度极慢或失败。排查：网络连接问题，或 GitHub 令牌未生效。解决：

1. 确认echo $GITHUB_ACCESS_TOKEN输出正确。
2. 尝试配置 Git 使用 SSH 密钥，但 LeanDojo 内部调用可能仍用 HTTPS。一个变通方法是先手动克隆仓库到本地，然后修改 LeanDojo 的代码或配置，让其指向本地路径。但这需要修改源码，比较复杂。
3. 耐心等待，首次克隆 mathlib4（约 1GB+ 历史）确实需要时间。

5.2 运行时报错与调试

问题：Dojo初始化失败，提示 Lean 服务器错误或超时。排查：这是最常见也最棘手的一类问题。原因可能是 Lean 版本冲突、文件路径问题、内存不足等。解决：

1. 启用详细日志：在运行脚本前设置环境变量VERBOSE=1。这会让 LeanDojo 和底层的 Lean 服务器输出大量调试信息。

VERBOSE=1 python your_script.py

2. 检查 Lean 版本：确保elan中有项目所需的精确 Lean 版本。可以进入项目目录（如果有lakefile.lean），运行lake env查看所需版本，然后用elan default <version>设置。
3. 检查磁盘空间和内存：Lean 编译需要大量内存。确保可用内存充足（建议 >8GB）。同时检查/tmp分区是否有足够空间。
4. 简化复现：尝试用一个绝对简单的定理和最小的脚本复现问题，排除其他代码干扰。

问题：提取数据时进程被杀死（Killed），尤其是使用多进程时。排查：大概率是内存耗尽（OOM）。数据提取，特别是并行提取多个文件，非常消耗内存。解决：

1. 减少同时提取的进程数。查看lean_dojo.data_extraction中是否有num_workers之类的参数，将其设为 1。
2. 在内存更大的机器上运行。
3. 分批次提取文件，而不是一次性提取整个仓库。

5.3 性能调优建议

1. 缓存是关键：LeanDojo 在首次运行时会编译 Lean 文件和下载依赖，这个过程很慢。但编译结果会被缓存。确保缓存目录（通常在~/.cache/lean或~/.lean）有足够的空间，并且不要轻易清除。重复运行相同仓库和 commit 的脚本会快很多。
2. 使用本地镜像：如果你需要频繁切换不同的 mathlib4 commit，可以考虑在本地建立一个 bare git 仓库镜像，然后修改 LeanDojo 的源码，让其从这个镜像拉取，可以节省大量网络克隆时间。
3. 交互环境复用：创建Dojo对象是有开销的。如果你的实验需要多次尝试证明同一个定理，最好在一个with Dojo(...)上下文内完成所有尝试，而不是每次都新建。
4. 策略执行超时：在自动证明循环中，有些策略可能会陷入长时间计算（如simp处理复杂目标）。建议为dojo.run_tactic设置超时机制，可以使用 Python 的signal或multiprocessing来实现，避免整个程序卡死。

6. 从 LeanDojo 到 LeanDojo-v2：演进与迁移考量

正如项目开头所述，原版 LeanDojo 已进入维护状态，官方力推全新的LeanDojo-v2。作为实践者，了解两者的主要区别和迁移路径非常重要。

LeanDojo-v2 的核心改进：

1. 性能大幅提升：v2 重写了与 Lean 服务器的通信层和内部数据结构，数据提取和交互的速度比 v1 快了一个数量级。这对于需要大规模实验的研究至关重要。
2. 更简洁的 API：v2 的 API 设计更加直观和 Pythonic，降低了学习成本。
3. 更好的 Lean 4 支持：v2 紧跟 Lean 4 的最新发展，兼容性更好。
4. 集成了更多基准测试和工具：v2 可能直接包含了更多开箱即用的评测脚本和数据集处理工具。

迁移建议：

• 对于新项目：毫无疑问，应该直接使用LeanDojo-v2。从它的 GitHub 仓库开始，按照新的文档进行安装和配置。
• 对于已有基于 v1 的项目：需要评估迁移成本。如果项目严重依赖 v1 的某些特定行为或内部 API，迁移可能需要一些工作量。建议先在一个分支上尝试用 v2 运行核心流程，对比结果是否一致。通常，数据提取的格式和交互的基本逻辑是相似的，但函数名和调用方式可能变了。
• 学习目的：阅读和理解本文以及 v1 的架构，仍然非常有价值。它揭示了这类工具的核心挑战和解决方案。理解了 v1，再看 v2 的改进，你会更有体会。

无论选择哪个版本，LeanDojo 所代表的“将交互式定理证明转化为机器学习可处理问题”的思路，已经深刻影响了这个领域。它不仅仅是一个工具，更是一个研究范式的推动者。

最后，分享一个我个人的小技巧：在开发基于 LeanDojo 的自动证明系统时，不要只盯着最终的证明成功率。多花时间分析模型的“失败案例”。看看模型是在哪一步卡住的，它提出的策略为什么不对，是检索的前提不对，还是策略预测的分布有问题？这些 case-by-case 的分析，往往比单纯的指标提升更能带来实质性的算法改进。定理证明的评估，很多时候是二元的（证出来/没证出来），但理解失败的原因，才是进步的开始。