Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
Numina-Lean-Agent：开源通用智能体推理系统，用于形式数学证明
https://www.researchgate.net/publication/399956619_Numina-Lean-Agent_An_Open_and_General_Agentic_Reasoning_System_for_Formal_Mathematics
摘要
智能体系统近期已成为形式化定理证明的主流范式，通过协调多个模型与工具取得了卓越性能。然而，现有方法通常依赖于任务特定的流水线和经过训练的形式化证明器，限制了其灵活性与可复现性。本文提出一种新范式：直接使用通用代码智能体作为形式化数学推理器。该范式基于三点动机：(1) 通用代码智能体为证明以外的多样化推理任务提供了自然接口；(2) 仅需更换底层基础模型（无需训练）即可提升性能；(3) 通过 MCP（Model-Calling Protocol）可灵活扩展并自主调用专用工具，避免复杂设计。基于此范式，我们提出了 Numina-Lean-Agent，它结合 Claude Code 与 Numina-Lean-MCP，实现与 Lean 的自主交互、相关定理检索，以及非形式化证明和辅助推理工具的调用。以 Claude Opus 4.5 为基础模型，Numina-Lean-Agent 成功解决了 Putnam 2025 全部 12 道题目，性能媲美当前最优的闭源系统。除基准测试外，我们还展示了其通用性：通过与数学家协作，成功形式化了 Brascamp–Lieb 定理。我们在 https://github.com/project-numina/numina-lean-agent 开源发布 Numina-Lean-Agent 及所有解决方案。
- 引言
形式化定理证明旨在在严格定义的逻辑系统（如 Lean (2015) 和 Isabelle (Paulson, 1994)）中构建机器可验证的数学定理证明。与非形式化数学推理不同，形式化验证系统提供了自动且可靠地验证证明正确性的工具，从而为构建可靠推理奠定基础。早期神经定理证明研究聚焦于开发单模型形式化证明器。早期证明器结合策略预测与显式搜索方法（如蒙特卡洛树搜索）来探索证明空间（Lample 等, 2022；Hubert 等, 2025）。为缓解基于搜索方法的效率瓶颈，后续工作探索了整篇证明生成，以直接产出完整证明（Xin 等, 2024）。此后，其他研究引入非形式化推理以指导策略生成与证明构造（Wang 等, 2025；Ren 等, 2025）。尽管取得显著进展，在形式化系统中有效捕捉长程、结构化推理仍是核心挑战。
近期，若干系统超越了单模型形式化证明器，引入智能体工作流，使证明器能与形式化定理证明环境及其他模型交互。例如，HILBERT（Varambally 等, 2025）提出一个智能体框架，将非形式化推理器与形式化证明器结合以引导证明构造。同时，Seed-Prover 1.5（Chen 等, 2025）通过大规模智能体强化学习训练形式化证明器，强调与 Lean 编译器及相关工具的反复交互。此外，Axiom Math 团队开发的 AxiomProver（Axiom Math Team, 2025）采用自主多智能体集成架构，在 Putnam-2025 上取得满分成绩。这些系统凸显了智能体证明系统的日益有效性。然而，尽管性能强大，现有智能体证明系统仍存在若干局限：(1) 依赖于显式设计的任务特定推理流水线，且常与大量训练的形式化证明器耦合，限制了其向新工具或领域的扩展能力；(2) 大多数系统为闭源，且实现细节有限，使社区难以复现和拓展其工作。
本文提出一种基于通用代码智能体构建形式化数学推理器的新范式，其动机有三：(1) 代码智能体为证明之外的多样化证明工程任务提供了原生接口；(2) 可灵活替换底层基础模型以增强推理能力，无需任何训练；(3) 集成 MCP 支持即插即用式扩展专用推理工具，模型可根据具体查询自主调用它们。遵循此范式，我们提出 Numina-Lean-Agent，由 Claude Code 与 Numina-Lean-MCP 组成，提供多样化的推理工具。具体而言，Numina-Lean-MCP 集成了多个核心组件：包括 Lean-LSP-MCP（Dressler, 2025）用于与 Lean 定理证明器进行智能体交互；为提供相关背景知识，我们开发了 LeanDex，用于从 mathlib 等 Lean 库中语义检索相关定理与定义；采用 Informal Prover（Huang & Yang, 2025）生成详细的非形式化证明方案；并引入 Discussion Partner 工具，可查询外部语言模型以辅助推理与规划。这些组件共同使 Numina-Lean-Agent 成为一个通用而强大的形式化数学推理系统。
以 Claude Opus 4.5（Anthropic, 2025）为基础模型，Numina-Lean-Agent 成功解决了 Putnam 2025 全部 12 道题目，达到当前最先进水平，结果与闭源系统 AxiomProver 持平，并比 Harmonic 的 Aristotle（Achim 等, 2025）多解决两题。我们在第 3 节报告了所有解决方案及其计算成本与证明长度。值得注意的是，在某些题目（如 Problem-B1）上，Numina-Lean-Agent 生成的证明显著比 AxiomProver 和 Seed-Prover 1.5 更简洁。除标准自动证明外，Numina-Lean-Agent 还可作为通用数学推理系统，支持数学家进行交互式的“直觉式证明”（vibe proving）。我们通过与人类专家合作形式化 Brascamp-Lieb 定理来演示这一范式，交互过程的细节见第 4 节。
- Numina-Lean-Agent
2.1 概述
如图1所示，Numina-Lean-Agent 是一个基于 Claude Code 与 Numina-Lean-MCP 构建的智能体形式化定理证明框架。作为自主智能体，它能够动态选择并调用 Numina-Lean-MCP 中的适当推理工具，以应对多样化查询并完成复杂的形式化推理任务。
2.2 Numina-Lean-MCP
Lean-LSP-MCP：Lean-LSP-MCP（Dressler, 2025）是一个专为 Lean 定理证明器设计的模型上下文协议（MCP）服务器。它通过语言服务器协议（LSP）在大语言模型与 Lean 内核之间架起桥梁，赋予模型深入理解、分析和操作 Lean 项目的能力。其工具集分为三个维度，显著增强模型的证明能力：
- 语义感知与交互：此维度提供一系列工具，使智能体能模拟熟练 Lean 用户的行为。从用于把握全局结构的
lean file outline，到用于精确查询目标的lean goal，再到用于获取权威验证结果的lean diagnostic messages，这些工具使模型摆脱对证明状态的猜测，实现基于真实编译环境的精准决策。 - 代码执行与策略探索：支持通过
lean run code即时编译孤立代码片段，并利用lean multi attempt在单个证明节点上并行执行和评估多种策略。该机制建立了“尝试–反馈–优化”的闭环，为自动定理证明提供稳健支持。 - 定理检索与知识增强：集成多层级搜索工具，有效缓解幻觉问题。
lean local search聚焦于本地 Lean 项目与标准库（stdlib）内定义的挖掘；lean loogle则支持通过自然语言或结构化查询在庞大的 Mathlib 仓库中进行搜索。这种双重检索机制确保模型所引用的每一条定理均真实存在且语境恰当。
LeanDex：我们提出一款新的 Lean 定理搜索工具，支持在 Lean v4.26.0 环境下进行定理检索。与现有工具相比，loogle对搜索查询格式要求严格，而本地搜索主要局限于项目内部。LeanDex 是一款面向智能体的语义搜索工具，可跨多个包（包括 mathlib 和 FLT）检索数学定理与定义。给定自然语言查询后，LeanDex 会调用智能体解释并推理查询意图，识别最相关的 Lean 对象。该工具基于 LeanExplore 构建，在底层语义搜索框架基础上增强了推理与检索能力，显著提升了灵活性与覆盖范围。
非形式化证明器（Informal Prover）：我们实现了一个轻量级的 Gemini IMO 智能体系统（Huang & Yang, 2025）作为非形式化证明器，用于生成详细的非形式化解题方案。该系统包含两个模型：生成器（Generator）与验证器（Verifier）。生成器负责生成非形式化解法，验证器则评估其正确性。二者通过迭代精炼循环协作：当验证器发现生成证明中的错误时，会向生成器提供反馈；在下一轮迭代中，生成器结合前一版解法与验证器反馈进行修正。此过程持续进行，直至验证器接受解法为正确，或达到预设最大迭代次数（我们设定为20次）。
为提升验证可靠性，验证器对每个候选解独立评估三次。仅当三次验证均判定正确时，该解才被接受。在我们的实现中，生成器与验证器均使用 Gemini-3-Pro-Preview。
讨论伙伴（Discussion Partner）：在科学研究中，讨论被广泛认为是一种高效的认知工具。通过交换不同观点与推理路径，研究者常能突破思维盲点、激发新灵感，从而推动问题解决。受此启发，我们设计并实现了“讨论伙伴”工具，旨在辅助自动化形式化过程。
具体而言，该工具赋予 Claude Code 在 Lean 形式化过程中“寻求协助”的能力：当遇到障碍——如证明瓶颈、策略选择困境或中间引理模糊性——主模型可主动发起与其他大语言模型的讨论。这些协作模型从不同推理视角分析当前状态，提供候选思路或替代证明路径，给予富有洞察力的反馈。借助这一多模型协同机制，系统能更有效地探索证明空间，显著提升形式化过程的鲁棒性与成功率。
- 评估
3.1 性能
我们在 Putnam 2025 基准上对 Numina-Lean-Agent 进行了评估，并将其性能与其他现有证明器进行了比较。值得注意的是，我们使用了 Seed-Prover 1.5 提供的形式化题目陈述。此外，我们智能体执行的所有操作均为严格串行，未采用任何形式的并行化。所有 API 调用均禁用了互联网搜索功能，以防止智能体通过在线检索获取答案。
在此设置下，Numina-Lean-Agent 取得了当前最先进（state-of-the-art）的性能，成功解决了 Putnam 2025 全部 12 道题目。默认情况下，每道题分配约 50 美元的计算预算。由于问题 A5 的难度显著更高且证明搜索轨迹更长，其被分配了更大的预算，约为 1000 美元；问题 B6 的预算也相应提高至约 300 美元。这些数值旨在反映相对计算开销，而非精确的财务核算。
我们针对非形式化证明器（informal_prover）工具的两种设计范式，在 Putnam 2025 B4 题目上进行了对比实验。第一种方法采用迭代精炼策略：先生成初始解，再进行验证，根据反馈进行修正，并重复此循环共 n 轮（Huang & Yang, 2025）。第二种方法采用独立采样策略：独立生成 n 个解，并分别对每个解进行验证。为确保公平比较，两种方法的总调用次数保持一致。
实验结果表明，在相同的搜索配置下，迭代精炼策略显著优于独立采样策略。具体而言，独立采样在 10 轮内未能完成 B4 的形式化证明，而迭代精炼仅用 5 轮便成功完成了证明，清晰地展示了基于反馈的迭代修正机制在提升证明效率方面的优势。
此外，我们还提出了一种新的子智能体（subagent-based）方法来解决 A5 问题，其详细方法将在第 3.2 节中讨论。
如表3所示，我们在 Putnam 2025 上对比了 Numina-Lean-Agent 与其他代表性证明器在各题目上的求解时间。尽管 Numina-Lean-Agent 未采用任何并行执行机制，但它在部分题目上展现出显著的效率优势，在多个实例上的求解时间短于其他方法。
在表4中，我们进一步比较了不同证明器生成的证明长度。为确保公平比较，我们从最终的 Lean 代码中移除了所有注释和空行，并统计剩余的行数。结果表明，与 AxiomProver 和 Seed-Prover 1.5 相比，Numina-Lean-Agent 在大量题目上生成了更短的证明；尤其在 A3、B1 和 B5 题目上，这一优势尤为显著。我们注意到，基于步骤（step-based）的证明器在生成极短证明方面具有固有优势，因此 Numina-Lean-Agent 生成的证明通常比 Aristotle 的更长。然而，在相似设置下与其他智能体证明器相比，Numina-Lean-Agent 在大多数题目上始终能产出更简洁的形式化证明，展现出其在生成紧凑高效形式化证明方面的有效性。
3.2 Putnam-2025-A5
对于问题 A5，我们采用了一种新颖的子智能体（subagent）机制，将证明分解为若干子目标并独立求解，有效缓解了上下文过长的问题。我们的经验观察表明，当上下文过长时，模型遵循指令的能力显著下降，难以聚焦于单一证明目标，从而阻碍关键子目标的解决。通过引入子智能体并对证明任务进行模块化，我们能够大幅缓解这些问题，提升整体证明效率。
A5 的核心在于证明：在所有满足某特定性质的排列中，交错排列（alternating permutations）的数量最多。在若干前期实验中，模型反复卡在这个关键引理上。我们推测这一困难源于上下文过长，因此采用了子智能体策略，将该引理从整体证明中隔离出来单独处理。具体而言，子智能体首先调用 GPT-5.2 生成一个非形式化的提示（hint），然后在该提示的指导下完成相应的形式化工作。此过程可迭代进行，直至该引理被成功形式化。
- 使用 Numina-Lean-Agent 形式化 Brascamp–Lieb 定理
4.1 蓝图生成
在 Lean 中形式化一个复杂定理是一项具有密集依赖关系的长程任务。当直接要求 Claude Code 证明最终陈述时，它常常采用次优的形式化方案，并陷入局部死胡同。因此，我们引入“蓝图”（blueprint）作为显式的规划层，将全局目标分解为一系列可验证的子目标。
蓝图是一种类似设计文档的产物，包含：(i) 所需的定义与记号；(ii) 一组经过精心筛选、粒度适中的中间引理；(iii) 最终定理，其证明主要由这些引理组合而成。依赖关系被显式记录（例如通过\uses{...}），形成一个有向无环图（DAG），用于确定证明顺序并在搜索过程中减少歧义。
重要的是，蓝图生成是递归的，并且紧密耦合于形式化循环，而非一次性预处理步骤。当智能体尝试在 Lean 中证明引理时，编译反馈和证明状态检查可能揭示某个非形式化步骤存在错误、描述不足，或划分粒度不当。此时，智能体会回溯并精炼蓝图（例如加强假设、重述命题以匹配 Lean 接口，或插入缺失的中间引理），然后基于更新后的计划继续形式化。为提升鲁棒性，当当前蓝图反复导致瓶颈时，智能体还可调用外部讨论模型（如 Gemini）提出替代的分解方案或修复建议。
总体而言，蓝图扮演了高层数学规划的角色：由更强的数学推理器将困难命题分解为一系列小而可验证的步骤，而 Claude Code 则专注于将这些步骤转化为机器可验证的 Lean 证明。关键在于，验证不仅是终点——Lean 的反馈（如类型类搜索失败、缺失引理、接口不匹配等）提供了具体信号，用于修正蓝图，从而形成一个闭环的“规划–形式化–精炼”工作流，稳定地支持长程形式化。
4.2 人机协作
我们为 Numina-Lean-Agent 设计了一种人机协作交互框架，使人类专家能够通过撰写提示和修改蓝图与智能体协同工作。本文其中一位作者是数学家，我们基于他于 2025 年 11 月发表的预印本《Effective Brascamp–Lieb Inequalities》（2025）开展了一项协作案例研究。附录 A.1 展示了该论文主定理的形式化陈述。在此实验中，一位数学家、一位 Lean 形式化专家与 Numina-Lean-Agent 共同合作，完成了该论文结果的形式化。
在不到两周的间歇性协作中，两位人类专家与智能体共同完成了超过 8,000 行 Lean 代码的形式化。在此过程中，智能体自主引入了约 70 个新定义、引理和定理，展现出其主动扩展形式化库并参与大规模、持续性形式化工作的能力。目前，人类专家正在对完整 Lean 代码进行简化，我们在附录 A.1 中仅呈现主定理的形式化陈述。
在形式化更复杂的论证时，智能体有时会进一步分解证明，引入比原始蓝图中更细粒度的中间引理。这种行为似乎是一种针对形式化验证需求的自适应证明分解策略。
此外，与其它专用证明模型相比，我们的智能体不仅限于定理证明，还展现出强大的通用推理能力。对于一个正确性事先未知的形式化命题，传统方法通常只能并行尝试证明原命题及其否定。相比之下，在 Brascamp–Lieb 不等式的形式化过程中，我们观察到智能体能在证明过程中主动推理该命题本身的正确性。当检测到命题有误时，它能自主修正该命题。这种在形式化过程中动态检查并修改问题表述的能力，是以往证明器所不具备的。我们在附录 A.2 中提供了此类行为的具体示例。
4.3 局限性
有时，我们的系统生成的 Lean 代码过于冗长或结构欠佳。实践中，我们主要让智能体处理两类不同难度的sorry：
sorry仅涉及已良好结构化证明中的局部推理时，智能体通常能以高质量代码填补空缺；- 但当
sorry对应整个引理的完整证明时，尽管智能体通常能达成目标，但生成的代码往往冗长，不如预期简洁。
这凸显了系统的一个局限：虽然能处理复杂证明目标，但在更大或更复杂任务中，生成形式化代码的可读性与结构性可能下降。
此外，系统偶尔在类型层面问题上遇到困难，这会显著拖慢证明进程。例如，有一次智能体完全失败——并非因为核心数学论证困难，而是由于从Real到NNReal的类型转换问题。这类类型约束在非形式化数学中很少显式说明，因此智能体难以自行重建所需结构。在调整证明流程、提前处理类型转换以使形式化路径更“类型友好”后，智能体成功完成了剩余证明。此案例突显了非形式化与形式化证明之间的固有鸿沟，也强调了类型层面要求对自动化推理系统构成的挑战。
最后，尽管当前智能体在自动定理证明中展现出强大的问题解决能力，但其在功能正确性与形式优雅性之间仍存在明显差距。虽然智能体生成的证明通常能通过 Lean 编译器检查，但经验丰富的 Mathlib 贡献者常认为这些证明过于结果导向，依赖冗长且低级的策略脚本。与人类编写的 Mathlib 代码相比，这些证明缺乏结构化抽象和对高层模式的惯用表达，在简洁性、可读性以及符合 Mathlib 社区规范方面仍有很大提升空间。
原文：https://www.researchgate.net/publication/399956619_Numina-Lean-Agent_An_Open_and_General_Agentic_Reasoning_System_for_Formal_Mathematics
热门跟贴