1. 项目概述当机器学习遇见形式化证明如果你是一名机器学习研究者或者对形式化证明和定理自动证明领域感兴趣那么“LeanDojo”这个名字最近可能已经进入了你的视野。简单来说LeanDojo 是一个为 Lean 定理证明器量身打造的 Python 工具包它的核心目标只有一个用机器学习的方法特别是大语言模型来辅助甚至自动化数学定理的证明过程。这听起来像是科幻小说里的情节——让 AI 来帮数学家做证明。但事实上随着像 GPT-4 这类大语言模型在代码生成和逻辑推理上展现出惊人潜力这个交叉领域正以前所未有的速度变得火热。LeanDojo 正是这个浪潮中的关键基础设施。为什么是 Lean在众多交互式定理证明器中Lean尤其是其第四代版本 Lean 4因其活跃的社区和庞大的数学知识库 mathlib4 而脱颖而出。mathlib4 包含了从基础算术到前沿代数几何的成千上万个形式化定理及其证明这为机器学习模型提供了海量、高质量的结构化训练数据。然而直接从 Lean 项目中提取这些数据、并与证明环境进行程序化交互是一个极其繁琐且容易出错的过程。LeanDojo 的出现就是为了填平这道鸿沟让机器学习研究者能像调用一个普通的深度学习库一样轻松地获取证明状态、尝试证明步骤在 Lean 中称为“策略”并评估模型的性能。需要特别注意的是你目前看到的这个原始 LeanDojo 库已被标记为“弃用”。项目团队已经将所有新功能开发转移到了LeanDojo-v2。原仓库的信息仅作为历史参考并且很快会被 v2 版本取代。因此对于所有新项目我的强烈建议是直接转向 LeanDojo-v2。不过理解原始版本的设计思想和核心功能对于掌握整个工具链的演进和背后的原理仍然至关重要。本文的讨论将基于这些核心概念展开它们绝大部分在 v2 版本中依然适用并得到了增强。2. 核心功能与设计哲学拆解LeanDojo 的设计紧紧围绕两个核心功能展开这恰好对应了机器学习研究中的两个关键环节数据准备和模型训练/评估。2.1 数据提取从形式化代码到机器学习数据集在传统机器学习中我们处理的是图像像素、文本单词或音频波形。在定理证明领域我们的“数据”是证明状态、证明步骤策略以及所引用的前提定理、定义。LeanDojo 的数据提取功能本质上是一个高级的“代码解析与状态追踪器”。它具体能提取什么证明状态在证明的任何一个时间点Lean 的“目标”是什么有哪些假设是已知的这类似于游戏中的“当前局面”。策略用户或模型输入了什么命令来改变证明状态比如rewrite [h]使用假设 h 进行重写、apply theorem_name应用某个定理、simp简化表达式等。这些是模型需要学习的“动作”。前提在证明某个定理时它依赖了哪些之前已经证明过的定理或定义这些前提构成了一个可检索的知识库对于构建检索增强的证明模型至关重要。为什么这个过程不简单Lean 项目不是静态的文本文件。它们有复杂的依赖关系需要编译证明过程是动态的、有状态的。直接解析.lean文件只能得到源代码文本却得不到程序执行时的中间状态。LeanDojo 的巧妙之处在于它通过与 Lean 服务器进行交互在代码编译和检查的过程中实时地“钩住”并记录下这些状态变化和策略调用从而构建出结构化的、可供机器学习使用的轨迹数据。这就像给 Lean 的编译过程装了一个精细的仪表盘和飞行记录仪。2.2 程序化交互构建一个可编程的证明环境提取数据是为了训练模型而评估模型则需要一个能让模型“实战”的环境。这就是 LeanDojo 的第二个核心功能提供一个与 Lean 交互的 Python API。这个环境能做什么初始化证明目标给定一个需要证明的定理LeanDojo 可以启动一个 Lean 会话并定位到该定理的证明起始点。执行策略模型可以生成一个策略如intro hLeanDojo 将这个策略发送给 Lean 服务器执行。获取反馈执行后环境会返回新的证明状态是成功了还是产生了新的子目标、可能的错误信息、以及整个过程的用时。回溯与探索模型可以像人类一样在证明树上进行回溯尝试不同的证明分支。这个设计的重要性何在它使得强化学习和在线学习成为可能。模型不再仅仅是离线地学习历史证明数据而是可以在一个模拟环境中进行“试错”根据环境反馈证明状态是否推进、是否出错来调整自己的策略生成。这为开发更强大、更具探索性的证明 AI 打开了大门。2.3 与 Lean 4 的深度绑定及版本考量LeanDojo 与 Lean 4 的版本兼容性是一个需要严肃对待的技术细节。项目明确要求 Lean 4v4.3.0-rc2或更高版本。这是因为 Lean 语言和工具链本身在快速迭代其内部 API 和编译流程可能发生变化。LeanDojo 需要与特定版本的 Lean 服务器协议保持同步才能稳定地进行数据提取和交互。注意虽然项目提供了legacy分支以支持更早的版本包括 Lean 3但对于绝大多数新用户尤其是希望利用最新 mathlib4 特性的研究者坚持使用 LeanDojo-v2 及其指定的 Lean 4 版本是最稳妥的选择。使用旧版本可能会遇到无法解析新语法、依赖解析失败等难以调试的问题。3. 环境配置与安装实战详解要让 LeanDojo 跑起来你需要一个配置得当的基础环境。以下步骤是我在 Ubuntu 系统上反复验证过的流程对于 Windows WSL 和 macOS 也有很高的参考价值。3.1 系统级依赖准备首先确保你的系统满足以下基础要求Git 2.25用于克隆 Lean 仓库如 mathlib4和 LeanDojo 本身。Python 3.9 到 3.12 之间这是当前主流机器学习库稳定支持的版本范围。Python 3.13 尚未经过广泛兼容性测试建议暂时避开。wget一个简单的命令行下载工具通常系统已自带。elan这是 Lean 的版本管理工具类似于 Python 的 pyenv 或 Rust 的 rustup。它是管理多个 Lean 版本的关键。安装 elan 通常是一行命令的事curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh安装完成后重启你的终端运行lean --version检查是否安装成功。elan 会自动帮你安装和管理 Lean 工具链。3.2 关键一步配置 GitHub 访问令牌这是新手最容易踩坑的地方。因为 mathlib4 等仓库托管在 GitHub 上且 Lean 构建过程需要下载很多依赖直接使用 Git 可能会因匿名访问频率限制而失败。生成令牌登录你的 GitHub 账户进入Settings-Developer settings-Personal access tokens-Tokens (classic)。点击Generate new token。设置权限给这个令牌一个描述性名称如 “LeanDojo Access”。在Select scopes部分至少需要勾选repo完全控制仓库和workflow可选如果你需要 GitHub Actions 相关功能。这确保了 Lean 在拉取私有子模块和依赖时有足够的权限。保存令牌生成后立即将令牌字符串复制保存到安全的地方因为它只显示一次。设置环境变量在你的 shell 配置文件如~/.bashrc,~/.zshrc中添加一行export GITHUB_ACCESS_TOKEN你的令牌字符串然后执行source ~/.bashrc或对应配置文件使其生效。你也可以在运行 LeanDojo 脚本前在终端里临时设置export GITHUB_ACCESS_TOKENyour_token。实操心得务必确保令牌具有repo权限。我曾因为只给了public_repo权限导致在构建一些依赖复杂私有子模块的特定分支时失败错误信息非常隐晦排查了很久。3.3 安装 LeanDojo 库由于原版已弃用我们直接讨论如何安装和使用 LeanDojo-v2。通常你可以通过 pip 从 Git 仓库直接安装开发版pip install githttps://github.com/lean-dojo/LeanDojo-v2.git或者更推荐的方式是克隆仓库后进行可编辑安装方便你查看源码和贡献git clone https://github.com/lean-dojo/LeanDojo-v2.git cd LeanDojo-v2 pip install -e .安装完成后建议在 Python 交互环境中快速验证一下导入是否成功import lean_dojo。4. 核心工作流程与代码示例解析让我们通过一个具体的例子来看看如何利用 LeanDojo-v2 进行数据提取和交互。假设我们想研究数学库中关于自然数加法的简单定理。4.1 数据提取实战抓取证明轨迹数据提取通常不是从零开始而是针对一个已有的 Lean 项目如 mathlib4。以下脚本展示了一个简化的提取流程import os from pathlib import Path from lean_dojo import Theorem, LeanGitRepo, Dojo # 1. 指定要分析的仓库和提交版本确保可复现性 repo_url https://github.com/leanprover-community/mathlib4 commit a1b2c3d4e5f67890 # 替换为具体的提交哈希例如 mathlib4 的某个稳定版本 repo LeanGitRepo(repo_url, commit) # 2. 指定我们感兴趣的文件和定理 # 例如mathlib4 中关于 Nat自然数加法的文件 file_path Mathlib/Data/Nat/Basic.lean # 假设我们想提取定理 add_comm (加法交换律) 的证明 theorem_name add_comm # 3. 定位定理对象 theorem Theorem(repo, file_path, theorem_name) # 4. 创建 Dojo 交互环境并提取轨迹 with Dojo(theorem) as (dojo, init_state): print(f初始证明目标: {init_state.goals}) # 模拟运行证明这里我们只是获取并打印轨迹实际提取会保存到文件 # LeanDojo 可以记录下证明过程中应用的每一个策略 trajectory dojo.run_to_completion() # 轨迹包含了状态序列和采取的策略 for step in trajectory: print(f步骤: {step.tactic}) print(f执行后目标: {step.new_state.goals if step.new_state else 证明完成})这个流程的关键在于LeanGitRepo和Theorem对象它们精确地定位了代码的版本和具体定理保证了实验的可复现性。提取出的trajectory对象包含了完整的证明步骤序列是训练监督学习模型的绝佳数据。4.2 交互式证明模拟让模型尝试证明更激动人心的部分是创建一个环境让训练好的模型来尝试证明新定理。下面是一个模拟循环from lean_dojo import Dojo import random def random_prover_model(state): 一个极其简单的随机“模型”从一组常见策略中随机选择一个。 在实际中这里应该替换为你的神经网络模型。 tactics [ intro h, apply h, simp, rw [h], exact h, constructor, left, right, reflexivity, ] # 这里应该根据 state.goals 的内容智能选择策略此处仅为演示 return random.choice(tactics) # 从一个定理开始 with Dojo(theorem) as (dojo, init_state): current_state init_state max_steps 50 for step_num in range(max_steps): if current_state.is_solved: print(f成功在 {step_num} 步内完成证明。) break # 模型根据当前状态生成一个策略 tactic random_prover_model(current_state) print(f第 {step_num} 步尝试策略: {tactic}) try: # 在环境中执行策略 result dojo.step(current_state, tactic) if result.error is not None: print(f 错误: {result.error}) # 处理错误例如回溯或尝试其他策略 break else: current_state result.new_state print(f 新目标数: {len(current_state.goals)}) except Exception as e: print(f 执行异常: {e}) break else: print(f在 {max_steps} 步内未完成证明。)这个模拟清晰地展示了 LeanDojo 作为“环境”的角色它接收模型的动作策略返回新的状态和奖励信号是否解决、是否出错。这正是强化学习框架的标准接口。4.3 检索增强的集成LeanDojo 论文的核心贡献之一是ReProver检索增强的证明器。其思想是在生成策略时模型不仅看当前的证明目标还会从一个大型前提知识库从 mathlib 中提取的所有定理中检索出最相关的前几个定理作为额外上下文。这极大地提高了模型调用正确定理的能力。在 LeanDojo-v2 中检索功能被更紧密地集成。你可能会用到类似下面的模式from lean_dojo import Retriever # 初始化一个检索器它需要预先构建好的前提索引 retriever Retriever(index_path./path_to_premise_index) with Dojo(theorem) as (dojo, init_state): current_state init_state while not current_state.is_solved: # 1. 检索相关前提 retrieved_premises retriever.retrieve(current_state, top_k5) # 2. 将检索到的前提作为额外的上下文/提示和当前状态一起输入给模型 # model_input 拼接(current_state, retrieved_premises) # tactic your_llm_model(model_input) # 3. 执行策略... # ... 后续步骤与上面类似这种“检索-生成”范式将大规模知识库的记忆负担从模型的参数中分离出来让相对较小的模型也能具备强大的证明能力是当前 AI for Theorem Proving 非常有效的技术路径。5. 常见问题与深度排错指南在实际使用 LeanDojo尤其是与庞大的 mathlib4 交互时你几乎一定会遇到各种环境问题。以下是我在多次部署中总结出的核心问题和解决方案。5.1 构建失败与依赖问题问题现象在初始化LeanGitRepo或运行Dojo时进程卡在“Building Lean project...”很久最后报错退出错误信息涉及lakeLean 的构建工具或找不到某些依赖。根本原因Lean 项目使用 Lake 管理依赖这些依赖通常是 Git 子模块或其他 Lean 包。构建过程需要从 GitHub 下载。网络问题、GitHub 访问限制、或依赖项版本冲突都可能导致失败。排查步骤检查令牌首先确认GITHUB_ACCESS_TOKEN环境变量已设置且有效。可以运行echo $GITHUB_ACCESS_TOKEN检查或直接在 Python 脚本开头用os.getenv(GITHUB_ACCESS_TOKEN)打印。手动构建进入你本地克隆的 mathlib4 仓库目录尝试手动运行lake exe cache get和lake build。这能更清晰地暴露错误。常见的网络问题可以通过配置 Git 代理或重试解决。清理缓存Lake 有缓存机制有时缓存损坏会导致奇怪错误。可以尝试删除lakefile.olean文件和./build目录然后重新构建。版本锁定确保你使用的 mathlib4 提交哈希与 LeanDojo-v2 测试过的版本兼容。查看 LeanDojo-v2 仓库的示例或测试文件它们通常会指定一个已知能工作的 commit。5.2 内存不足与进程崩溃问题现象在处理大型定理或复杂文件时Python 进程内存占用飙升最终被系统杀死。原因分析Lean 服务器本身是一个内存消耗大户尤其是当加载了完整的 mathlib4 时。每个Dojo会话都会启动一个 Lean 服务器进程。如果你并行运行多个会话内存压力会成倍增加。解决方案限制并发避免同时创建大量Dojo实例。使用资源池或队列来管理并发数。及时清理确保Dojo在with语句块结束后被正确关闭或者手动调用dojo.__exit__()来终止 Lean 服务器进程。使用轻量级上下文如果可能只导入定理所在的最小必要文件而不是整个 mathlib4。这需要对 Lean 项目的结构有深入了解。增加系统交换空间为你的虚拟机或物理机增加足够的交换空间作为最后的内存缓冲。5.3 策略执行与状态同步错误问题现象模型生成的策略在dojo.step()中执行返回的错误信息难以理解或者执行后状态没有按预期更新。排查思路理解 Lean 错误Lean 的错误信息有时很晦涩。将模型生成的策略复制到一个真正的 Lean IDE如 VS Code with lean4 插件中相同的位置执行看是否能得到更清晰的错误提示。常见的错误有未知标识符、类型不匹配、策略在当前目标下不适用等。检查状态一致性确保你传递给dojo.step()的state对象是当前最新的状态。在多步推理中必须使用上一步返回的result.new_state。验证策略语法模型有时会生成不合法的策略字符串。增加一个简单的语法检查层过滤掉明显无效的策略例如以不存在的命令开头。启用详细日志按照项目说明设置环境变量VERBOSE1这会让 LeanDojo 和底层的 Lean 服务器输出更详细的日志有助于定位通信或执行问题。5.4 性能优化技巧批量处理如果你需要提取成千上万个定理的数据不要用一个接一个的串行循环。设计一个工作队列并行地处理多个定理但要注意上面提到的内存限制。缓存中间结果提取出的定理轨迹数据Trajectory可以序列化如用pickle或json保存到磁盘。后续训练模型时直接加载这些文件避免重复进行昂贵的 Lean 编译和提取过程。索引预计算对于检索增强模型为整个前提库构建向量索引是一个耗时操作。一旦构建完成就将索引文件保存下来供后续所有实验重复使用。6. 生态相关工具与进阶研究方向LeanDojo 不是一个孤立的工具它是一个生态的起点。了解其相关项目能帮你更好地定位自己的研究方向。LeanDojo Benchmark这是论文中使用的标准数据集包含了从 mathlib 中提取的定理-证明对。它是评估新证明模型性能的基准。v4 版本对应 Lean 4 和 mathlib4。ReProver这是官方实现的检索增强证明器模型代码。研究它的架构、训练方式以及如何集成检索器是理解当前 state-of-the-art 方法的最佳途径。Lean Copilot一个非常有趣的项目它尝试将大语言模型如 GPT-4直接作为 Lean 的证明辅助工具Copilot在 IDE 中提供实时的策略建议。这展示了 LeanDojo 基础设施的另一种应用方向——人机协作证明。LeanDojo ChatGPT Plugin一个将定理证明能力接入 ChatGPT 的插件原型让更多人能通过自然语言与形式化证明交互。对于想要深入的研究者以下几个方向值得探索更好的检索器当前基于嵌入的检索是否最优能否结合符号匹配、图神经网络来更好地理解定理之间的逻辑关系更高效的策略生成将证明生成视为一个序列决策问题如何设计更有效的强化学习算法蒙特卡洛树搜索MCTS如何应用于这个领域课程学习与课程数据从简单的定理开始训练模型逐步增加难度能否让模型学会更通用的证明技巧解释性与交互性模型生成的证明步骤对人类来说是否可理解能否设计一种交互模式让模型在卡住时向人类用户请求提示LeanDojo 及其生态将形式化证明这个曾经高度专业化、需要极深领域知识的领域变成了一个对机器学习社区开放、可编程、可大规模实验的 playground。它所解决的工程挑战——可靠的数据提取和稳定的交互环境——是这个领域得以快速发展的基石。虽然原版库已进入维护状态但 LeanDojo-v2 的持续开发意味着这条道路正在被拓宽和加固。对于任何有志于探索 AI 前沿特别是逻辑推理与代码生成交叉领域的研究者和工程师来说熟练掌握这套工具链无异于获得了一把打开宝库的钥匙。