OpenProver: 基于 Lean 4 的智能体和交互式定理证明

# 使用 Lean 4 的智能体式交互定理证明
来源：https://arxiv.org/html/2607.09217
11institutetext:查尔斯大学，数学物理学院，布拉格，捷克共和国
11email:\{kripner,straka\}@ufal\.mff\.cuni\.cz###### 摘要

在本系统论文中，我们介绍 OpenProver，一个开源系统，用于大语言模型驱动的自动定理证明（ATP），并集成了 Lean 4 形式化验证。OpenProver 采用受近期 ATP 智能体系统（如 Aletheia）启发的规划器-工作者-验证器架构。规划器代理维护一个紧凑的白板草稿纸和一个无界的中间发现仓库，并将数学工作分解为并行的工作者。

OpenProver 完全开源，通过自动形式化验证生成证明提供可复现评估，并提供用于人工指导的证明搜索交互式终端界面。在交互模式下，OpenProver 允许人类操作员监控和引导证明搜索过程，其动机源于交互式代码生成中已建立的人机协同。

为了展示自动形式化验证在定量消融实验中的潜力，我们在 ProofNet 上评估 OpenProver 并与简单基线进行比较。OpenProver 可在 github.com/kripner/OpenProver (https://github.com/kripner/OpenProver) 公开获取。

## 1 引言

随着使用基于可验证奖励的强化学习（RLVR）训练的大语言模型（LLM）\[13 (https://arxiv.org/html/2607.09217#bib.bib13)\] 的整合，自动定理证明（ATP）的能力显著提升。除了解决竞赛数学中最困难的一些问题之外，我们现在开始看到 ATP 系统在前沿数学研究中的实用性火花。

现有的 ATP 系统大致可分为两类。首先，完全自主的定理证明器试图进行端到端的证明生成，无需人工干预，从而保证了跨运行的可复现性。这类系统的例子是 Aletheia \[3 (https://arxiv.org/html/2607.09217#bib.bib3)\]。

其次，交互式定理证明器（ITP）允许用户监控和干预证明搜索过程，其依据是：虽然自主 AI 系统尚未达到专家人类的表现，但两者结合可以极大加速研究。例如，数学家可以制定几种完成某个证明的潜在方法，从 AI 助手处获得详细的相反例子和观察，并利用这些信息迭代调整高层计划。由于人类操作员在回路中，ITP 方法需要精心设计可视化用户界面。与我们的工作同时，一些基于智能体大语言模型的 ITP 工具已经发布，包括 OpenGauss \[6 (https://arxiv.org/html/2607.09217#bib.bib6)\]。

我们介绍 OpenProver，一个自动定理证明器，它弥合了可复现 ATP 研究与交互式数学工具之间的差距。OpenProver 扩展了 Aletheia，最显著的是集成了 Lean 4 的形式化验证能力 \[8 (https://arxiv.org/html/2607.09217#bib.bib8)\]。为了展示 Lean 支持的自动评估，我们提供了 OpenProver 在 ProofNet \[2 (https://arxiv.org/html/2607.09217#bib.bib2)\] 上的性能定量测量，并与简单的线性思维链基线进行了比较。我们希望我们的工作能推进 ATP 系统的发展，使其既能在前沿数学研究中发挥作用，其性能又能被严格衡量。

## 2 系统描述

参见标题图 1：OpenProver 证明搜索循环概览。规划器迭代高层计划，管理持久状态，并将数学工作委派给工作者。验证器为每个工作者的贡献提供独立反馈。OpenProver 是一个自动定理证明器，利用在智能体框架中执行的推理大语言模型，并集成了 Lean 4 形式化验证器。系统以迭代循环方式运行，包含三种类型的代理，如图 1 (https://arxiv.org/html/2607.09217#S2.F1) 所示：一个规划器、并行的工作者和并行的验证器。

### 2.1 架构

在证明搜索过程中，OpenProver 使用三种不同类型的代理：

1. 1. **规划器**：维护全局状态并确定高层计划。
2. 2. **工作者**：独立探索候选证明策略、引理、反例等。
3. 3. **验证器**：独立验证每个工作者的输出，为规划器提供额外上下文。

证明搜索过程被结构化为一系列规划器步骤，详见第 2.3 节 (https://arxiv.org/html/2607.09217#S2.SS3)。

#### 2.1.1 规划器

在每一步，规划器首先生成一段思维链推理轨迹 \[12 (https://arxiv.org/html/2607.09217#bib.bib12)\]，然后生成输出和一系列动作。可用的规划器动作列于表 1 (https://arxiv.org/html/2607.09217#S2.T1)，并将在下文中详细解释。

表 1：规划器动作。在每个规划器步骤中执行一个或多个动作。* 在隔离模式下不可用。

#### 2.1.2 工作者

工作者是由规划器生成的独立代理。对于每个生成的工作者，规划器提供一个纯文本任务描述，仅指定工作者目的。示例任务包括：推进某个具体的证明方向、提出将定理分解为子目标的方案、证明一个引理、探索最小情况、搜索反例或证明定理的简化版本。此外，工作者可以被分配任务，将现有的自然语言证明形式化为 Lean 代码。

重要的是，工作者不观察先前工作者或规划器的推理轨迹或输出。这有助于独立探索不同的证明尝试，每个工作者不受无关上下文的影响。

#### 2.1.3 验证器

对于每个完成的工作者，我们生成一个验证器，其任务是生成独立的自然语言反馈，旨在揭示工作者输出中的缺陷。关键的是，验证器不观察工作者的推理轨迹，从而减少遵循相同但可能有缺陷的思维线路的偏见。

### 2.2 状态与记忆管理

为了在规划器步骤之间保留重要的上下文，OpenProver 管理一个名为**白板**的紧凑 Markdown 文件，由规划器使用 `write_whiteboard` 动作定期更新。虽然白板的内容完全由规划器决定，但根据相应的提示，建议至少包含当前执行的证明计划、所有已探索和失败尝试的历史、以及以后要返回的想法，以及任何有用的简要观察和注释。白板在每个步骤中都作为输入提供给规划器。此设计可视为类似于 **推理缓存** \[14 (https://arxiv.org/html/2607.09217#bib.bib14)\]，扩展了推理大语言模型的有效上下文长度。

此外，规划器偶尔需要存储更长的文本或 Lean 代码片段，如详细的失败证明尝试、引理的证明、文献摘要等。为了防止白板溢出，OpenProver 管理一个**项目仓库**，其中每个**项目**要么是 Markdown 文件，要么是 Lean 文件。项目使用 `write_items` 和 `read_items` 动作以类似文件夹的结构组织，并通过其相对路径（我们称之为**别名**）来引用。在每个规划器步骤中，除了白板，规划器还会观察到仓库中所有项目的别名和单行摘要。关键的是，Lean 项目仅当通过 Lean 形式化验证时才被存储；否则，错误和警告会反馈给规划器。这使得来自形式化验证器的反馈比仅检查最终答案更加紧密。

### 2.3 证明搜索循环

OpenProver 执行一个线性证明搜索循环，如算法 2 (https://arxiv.org/html/2607.09217#S2.F2) 所述，直到找到证明或计算预算耗尽。通过生成多个工作者实现并行化。

输入：`theorem.md`；可选 `theorem.lean`；代币预算 \(B\)
输出：`proof.md`，`discussion.md`；可选 `proof.lean`

1. 初始化白板 \(W \leftarrow \emptyset\)，仓库 \(R \leftarrow \emptyset\)，历史 \(H \leftarrow []\)；
2. **while** 预算未耗尽 且 `proof.md` 尚未生成 **do** |
3. `PlannerStep(W, R, H)`；
4. **end while**
5. （可选，进一步迭代 `PlannerStep` 直到生成 `proof.lean`）；
6. 写入 `discussion.md` 总结证明搜索过程和结果。

算法 1: OpenProver：高层操作
输入/输出：白板 \(W\)，仓库摘要 \(R'\)，历史 \(H\)，定理 \(T\)
1. 用 \((W, R', H_{-n:}, T)\) 查询规划器大语言模型；
2. 生成推理轨迹（CoT）；
3. 生成自由形式输出和动作列表 \(a_1, \dots, a_k\)；
4. 并行运行 \(a_1, \dots, a_k\) 并等待完成；
5. 将每个动作的输出附加到 \(H\)。

算法 2: PlannerStep

图 2: OpenProver 的高层伪代码：主循环（算法 1）重复调用 PlannerStep（算法 2）。

### 2.4 与 Lean 的集成

OpenProver 可选地与 Lean 形式化验证器集成，唯一的输入要求是提供包含一个或多个 `sorry` 关键字的 Lean 文件形式的形式化定理陈述。

首先，在找到自然语言证明后，OpenProver 尝试将其形式化并提交生成的 Lean 证明。如果 Lean 验证器发出错误或警告，OpenProver 会迭代尝试修复证明，可能在发现缺陷时回退到修复自然语言证明。

其次，规划器可以通过将任何中间结果作为 Lean 项目存储在仓库中来验证其正确性。第三，工作者可以执行与 Lean 相关的工具调用 \[10 (https://arxiv.org/html/2607.09217#bib.bib10)\]，可使用以下三个工具：

- **lean_verify** – 验证 Lean 代码片段的正确性。
- **lean_search** – 使用 LeanExplore \[1 (https://arxiv.org/html/2607.09217#bib.bib1)\] 对 Mathlib \[11 (https://arxiv.org/html/2607.09217#bib.bib11)\] 执行语义搜索，获取 \(k\) 个最相关的定义。
- **lean_store** – 将 Lean 代码片段附加到临时文件中，该文件将预先附加到每个后续的 `lean_verify` 输入中。通常包括导入、命名空间打开、定义和已证明的子引理。

形式化 ATP 的一个基本限制在于，形式化通常比非形式化证明搜索更具挑战性。随着已证明构建块的 Lean 生态系统随时间发展，这一差距有望缩小。

## 3 交互式用户界面

OpenProver 提供一个交互式终端用户界面（TUI），用户可以在其中监控和引导搜索过程。具体来说，用户可以：

- 监控所有代理的流式输出。
- 浏览先前规划器步骤的历史，检查其推理轨迹、动作输入、动作输出和白板状态。
- 如果任何工作者的推理方向看起来没有前景，可以中断它。
- 中断规划器并提供文本反馈以引导它。
- 在手动模式下，系统会提示用户接受每组规划器动作，然后才会执行。如果被拒绝（可能附带文本反馈），规划器会调整后再提出新动作。在自主模式下则跳过此步骤。

## 4 实验

表 2：OpenProver 与基线在 ProofNet 上针对不同模型的性能。我们在自主模式下，使用 185 个 ProofNet 形式化定理、不同的底层模型（Kimi K2.5 \[4 (https://arxiv.org/html/2607.09217#bib.bib4)\] 和 Leanstral \[7 (https://arxiv.org/html/2607.09217#bib.bib7)\]）以及每个问题 10 万个代币的预算，测量了 OpenProver 的性能。请注意，OpenProver 是模型无关的，可以在智能体证明搜索中使用任何推理模型作为构建块。作为基线，我们在相同的代币预算下，以线性对话方式展开每个模型，允许模型执行无限数量的 Lean 验证。此设置的总结见表 2 (https://arxiv.org/html/2607.09217#S4.T2)。

## 5 结论

通过介绍 OpenProver，我们希望为智能体定理证明领域的可复现研究铺平道路，这种研究通过自动形式化验证实现的定量评估成为可能。此外，可以想象，这种自动评估反馈可以用作代码或大语言模型提示空间中自主自我改进过程的引导信号，类似于例如反馈下降 \[5 (https://arxiv.org/html/2607.09217#bib.bib5)\] 或 AlphaEvolve \[9 (https://arxiv.org/html/2607.09217#bib.bib9)\]。在高层次上，OpenProver 采用灵活的设计，将许多行为决策从代码转移到提示中，使得纯基于提示的自我改进变得可行。

{credits}

#### 5.0.1 致谢
本项目得到了捷克科学基金会（GAČR）项目编号 25-18031S、查尔斯大学资助局（GAUK）项目编号 458326 以及 CEDMO 2.0 NPO 项目的支持。本研究部分得到了 SVV 项目编号 260 821 的支持。我们感谢捷克共和国俄斯特拉发 VSB – 技术大学 IT4Innovations 国家超级计算中心，授予本项目访问 LUMI 超级计算机的权限。该超级计算机由 EuroHPC 联合事业拥有，由 CSC（芬兰）和 LUMI 联盟托管，并通过捷克共和国教育、青年和体育部通过 e-INFRA CZ（授权号：90254）提供。

#### 5.0.2 \discintname
作者声明，没有与本文内容相关的竞争利益。

## 参考文献

- \[1\] Asher, J.: LeanExplore: A search engine for Lean 4 declarations (2025), https://arxiv.org/abs/2506.11085
- \[2\] Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E.W., Radev, D., Avigad, J.: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023), https://arxiv.org/abs/2302.12433
- \[3\] Feng, T., Trinh, T.H., Bingham, G., Hwang, D., Chervonyi, Y., Jung, J., Lee, J., Pagano, C., hyun Kim, S., Pasqualotto, F., Gukov, S., Lee, J.N., Kim, J., Hou, K., Ghiasi, G., Tay, Y., Li, Y., Kuang, C., Liu, Y., Lin, H., Liu, E.Z., Nayakanti, N., Yang, X., Cheng, H.T., Hassabis, D., Kavukcuoglu, K., Le, Q.V., Luong, T.: Towards autonomous mathematics research (2026), https://arxiv.org/abs/2602.10177
- \[4\] Kimi Team: Kimi K2.5: Visual Agentic Intelligence (2026), https://arxiv.org/abs/2602.02276
- \[5\] Lee, Y., Boen, J., Finn, C.: Feedback Descent: Open-Ended Text Optimization via Pairwise Comparison (2025), https://arxiv.org/abs/2511.07919
- \[6\] Math Inc.: OpenGauss: LLM-based Interactive Theorem Proving System. https://github.com/math-inc/OpenGauss (2026), gitHub repository
- \[7\] Mistral AI: Leanstral: Open-Source Foundation for Trustworthy Vibe-Coding (2026), https://mistral.ai/news/leanstral
- \[8\] Moura, L.d., Ullrich, S.: The Lean 4 theorem prover and programming language. In: International Conference on Automated Deduction. pp. 625–635. Springer (2021)
- \[9\] Novikov, A., Vũ, N., Eisenberger, M., Dupont, E., Huang, P.S., Wagner, A.Z., Shirobokov, S., Kozlovskii, B., Ruiz, F.J.R., Mehrabian, A., Kumar, M.P., See, A., Chaudhuri, S., Holland, G., Davies, A., Nowozin, S., Kohli, P., Balog, M.: AlphaEvolve: A coding agent for scientific and algorithmic discovery (2025), https://arxiv.org/abs/2506.13131
- \[10\] Schick, T., Dwivedi-Yu, J., Dessì, R., Raileanu, R., Lomeli, M., Hambro, E., Zettlemoyer, L., Cancedda, N., Scialom, T.: Toolformer: Language models can teach themselves to use tools (2023), https://arxiv.org/abs/2302.04761
- \[11\] The Mathlib Community: Mathlib: A formal library of mathematics (2020), https://github.com/leanprover-community/mathlib4
- \[12\] Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E.H., Le, Q.V., Zhou, D.: Chain-of-thought prompting elicits reasoning in large language models (2022), https://arxiv.org/abs/2201.11903
- \[13\] OpenAI: Learning to Reason with LLMs (2024), https://openai.com/index/learning-to-reason-with-llms/
- \[14\] Ma, X., Li, X., Zhang, Z., Sun, M.: Reasoning Cache: Enhancing Long-Context Reasoning with Prompt Compression (2025), https://arxiv.org/abs/2506.17445