Numina-Lean-Agent：面向形式数学的开放通用智能体推理系统 Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
基于Claude Code和MCP协议的智能体系统，在Putnam 2025上实现12/12满分
前置知识
形式化定理证明（Formal Theorem Proving）
形式化定理证明是使用严格定义的逻辑系统（如Lean、Isabelle）构建机器可验证证明的方法。与非形式化数学推理不同，形式化验证系统能够自动且可靠地验证证明的正确性。Lean是一种交互式定理证明器，使用依赖类型理论作为基础逻辑，用户通过编写tactic（策略）脚本来逐步构造证明。Lean 4版本引入了更好的元编程支持和性能优化，成为当前最活跃的形式化数学平台之一，其mathlib数学库包含超过100万行形式化代码。
本文的核心任务是在Lean中进行形式化证明，理解形式化证明的基本概念是理解论文贡献的前提
智能体系统（Agentic Systems）
智能体系统是指能够自主规划、决策和执行任务的AI系统。与传统的单次推理模型不同，智能体可以与环境交互、调用工具、根据反馈调整策略。在形式化证明场景中，智能体可以自主选择何时查询目标状态、何时搜索相关定理、何时生成代码、何时请求外部帮助。这种动态决策能力使得智能体能够处理更复杂的、需要长期规划的证明任务。
本文提出的Numina-Lean-Agent是一个智能体系统，理解智能体的工作原理对于理解论文的系统架构至关重要
MCP协议（Model Context Protocol）
MCP（Model Context Protocol）是一种让大语言模型与外部工具和服务交互的标准化协议。它提供了一种统一的方式来定义工具接口，使得模型可以动态地发现和调用各种专业工具，而无需在训练时硬编码这些能力。在本文中，MCP被用于将Lean证明器、定理检索系统、非形式化证明生成器等组件集成到一个统一的框架中，实现即插即用的工具扩展。
MCP是本文系统架构的核心，理解MCP的工作机制对于理解系统如何实现工具的灵活扩展至关重要
Lean-LSP-MCP
Lean-LSP-MCP是一个专门为Lean定理证明器设计的MCP服务器。它通过语言服务器协议（LSP）作为LLM与Lean内核之间的桥梁，使模型能够深入理解、分析和操作Lean项目。该工具提供三个维度的能力：语义感知与交互（如查询目标状态、获取诊断信息）、代码执行与策略探索（如编译代码片段、并行尝试多种策略）、定理检索与知识增强（如搜索本地项目和mathlib库）。
Lean-LSP-MCP是Numina-Lean-Agent与Lean交互的核心接口，理解其功能对于理解系统的具体工作流程至关重要
非形式化证明（Informal Proof）
非形式化证明是指用自然语言描述的数学证明，类似于教科书或论文中的证明风格。与形式化证明不同，非形式化证明不需要严格的逻辑系统验证，但更易于人类理解和交流。在本文中，系统使用一个非形式化证明生成器（基于Gemini模型）来生成详细的自然语言证明，作为形式化证明的引导和参考。
本文的一个关键创新是将非形式化推理与形式化证明相结合，理解非形式化证明的作用对于理解系统的工作流程至关重要
研究动机
现有的形式化定理证明系统面临几个关键限制。首先，大多数智能体证明系统依赖于专门为定理证明任务设计的推理流水线，这些流水线通常与经过大规模训练的形式化证明器紧密耦合。例如，Seed-Prover 1.5通过大规模智能体强化学习训练专门的形式化证明器，AxiomProver采用自主多智能体集成架构。这种任务特定的设计限制了系统向新工具或新领域扩展的灵活性。其次，大多数高性能系统都是闭源的，提供有限的实现细节，使得学术界难以复现和扩展这些工作。此外，现有系统在处理需要长期结构化推理的形式化任务时仍然面临挑战，特别是在证明空间探索效率和上下文长度限制方面。
本文的目标是本文的目标是提出一种基于通用编码智能体的形式化数学推理范式，具体目标包括：（1）利用通用编码智能体作为形式化数学推理器，提供一个能够处理多样化推理任务的自然接口；（2）实现基础模型的灵活替换，无需重新训练即可提升推理能力；（3）通过MCP协议实现专业推理工具的即插即用扩展，使模型能够根据具体查询自主调用合适的工具。最终目标是构建一个开放、通用、可扩展的形式化数学推理系统。
与已有工作不同的是，本文的独特切入角度在于提出了一个全新的范式：直接使用通用编码智能体作为形式化数学推理器，而不是训练专门的形式化证明器。这一范式的核心洞察是：通用编码智能体（如Claude Code）已经具备了强大的代码理解和生成能力，通过MCP协议可以灵活地扩展其能力边界。与现有方法相比，这种方法具有三个独特优势：（1）编码智能体提供了多样化的证明工程任务的自然接口；（2）可以通过简单替换底层基础模型来提升推理能力，无需任何训练；（3）MCP协议使得专业推理工具的集成变得简单灵活，避免了复杂的设计。
核心方法
Numina-Lean-Agent的整体架构如图1所示，它是一个基于Claude Code和Numina-Lean-MCP的形式化定理证明框架。系统的核心思想是将通用编码智能体（Claude Code）与专门为Lean设计的工具生态系统相结合，通过MCP协议实现动态的工具调用和交互。系统的工作流程可以概括为：用户提出数学问题→智能体分析问题并选择合适的工具→调用Lean-LSP-MCP与Lean交互、使用LeanDex检索相关定理、调用非形式化证明器生成参考证明、与讨论伙伴交流获取建议→根据反馈调整策略→最终生成形式化证明。这种架构使得系统能够根据具体问题动态选择和组合不同的推理工具，实现灵活高效的形式化证明。
本文的核心创新点在于提出了一种基于通用编码智能体的形式化数学推理范式，这与现有的任务特定方法有本质区别。现有方法（如Seed-Prover 1.5、AxiomProver）通常训练专门的形式化证明器，这些证明器与特定的推理流水线紧密耦合，难以扩展到新领域。而本文的方法直接利用Claude Code这样的通用编码智能体，通过MCP协议扩展其能力。这种方法的本质区别在于：它将形式化证明视为一种特殊的编码任务，利用编码智能体已有的代码理解、生成和调试能力，而不是从头训练专门的证明能力。这种范式转换带来了三个关键优势：（1）系统具有更强的通用性，能够处理多样化的数学推理任务；（2）可以通过替换基础模型（如从Claude 3.5升级到Claude Opus 4.5）来提升性能，无需重新训练；（3）通过MCP协议可以灵活地添加新工具，实现能力的即插即用扩展。
方法步骤详情
Numina-Lean-Agent的工作流程包括以下关键步骤：（1）问题接收与分析：智能体接收用户提出的数学问题（如Putnam竞赛题目），分析问题的性质和难度；（2）工具选择与调用：根据问题特点，智能体自主选择合适的工具组合。对于需要形式化证明的问题，首先调用Lean-LSP-MCP与Lean交互，查询当前目标状态；使用LeanDex检索相关的定理和定义，获取背景知识；（3）非形式化证明生成：调用非形式化证明器（基于Gemini IMO系统）生成详细的自然语言证明。该系统采用迭代优化策略，由生成器生成证明、验证器评估正确性，最多迭代20次，每次验证独立进行3次以确保可靠性；（4）讨论与协作：当遇到证明瓶颈时，智能体可以调用讨论伙伴工具，与其他LLM（如GPT-5.2）进行多模型协作，从不同推理角度分析问题，获取候选想法或替代证明路径；（5）证明构造与验证：基于收集到的信息，智能体生成Lean代码，通过Lean-LSP-MCP进行编译验证，根据反馈调整证明策略；（6）迭代优化：如果证明失败，智能体分析错误信息，调整策略，重复上述过程直到证明成功或达到预算限制。
技术新颖性
本文的技术新颖性体现在多个层面。首先，在范式层面，提出了基于通用编码智能体的形式化数学推理新范式，这与传统的训练专门证明器的方法有本质区别。其次，在系统架构层面，通过MCP协议实现了工具的即插即用扩展，使得系统能够灵活地集成各种专业推理工具，而无需复杂的系统设计。第三，在工具设计层面，提出了几个创新的工具组件：LeanDex提供了跨包的语义定理检索能力，支持mathlib和FLT等多个Lean库；非形式化证明器采用生成器-验证器迭代优化架构，通过独立验证3次确保可靠性；讨论伙伴工具实现了多模型协作推理，当主模型遇到瓶颈时可以寻求外部帮助。第四，在证明策略层面，提出了子智能体机制来处理特别困难的问题，如Putnam 2025的A5题。该机制将复杂证明分解为多个子目标，由独立的子智能体分别处理，有效缓解了上下文过长导致的推理能力下降问题。最后，在人机协作层面，提出了蓝图驱动的协作形式化方法，将人类专家的数学直觉与AI的执行能力相结合，成功形式化了Brascamp-Lieb定理这样复杂的数学结果。
实验结果
本文的核心发现在Putnam 2025基准测试上得到了充分验证。Numina-Lean-Agent使用Claude Opus 4.5作为基础模型，在Putnam 2025上实现了12/12的满分成绩，与闭源系统AxiomProver持平，超越了Harmonic的Aristotle系统（解决10/12题）和Seed-Prover 1.5（解决11/12题）。值得注意的是，系统在某些问题上（如B1题）生成了比AxiomProver和Seed-Prover 1.5更简洁的证明。在效率方面，尽管系统采用纯顺序执行（无并行化），但在多个问题上的求解时间仍优于竞争方法。在代码长度方面，Numina-Lean-Agent在多个问题上生成了更短的证明，特别是在A3、B1和B5题上优势明显。此外，系统还成功形式化了Brascamp-Lieb定理，在不到两周的人机协作中完成了超过8000行Lean代码的编写，自主引入了约70个新定义、引理和定理，展示了系统在大规模持续形式化任务中的能力。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| Putnam 2025 数学竞赛 | 解题数量（12题满分） | 12/12（100%） | AxiomProver 12/12, Seed-Prover 1.5 11/12, Aristotle 10/12 | 与AxiomProver持平，超越Seed-Prover 1.5 1题，超越Aristotle 2题 |
| Putnam 2025 求解时间 | 平均求解时间（分钟） | 多个问题求解时间更短（如A2: 30min, A6: 89min, B1: 55min） | Aristotle A2: 60min, A6: 60min; Seed-Prover 1.5 A6: 240min | 在部分问题上效率显著提升，如A6题比Seed-Prover 1.5快约2.7倍 |
| Putnam 2025 证明长度 | 代码行数（去除注释和空行） | 多个问题证明更简洁（如B1: 328行, A3: 422行, B5: 929行） | AxiomProver B1: 1179行, A3: 1089行; Seed-Prover 1.5 B1: 849行 | 在多个问题上生成更简洁的证明，如B1题比AxiomProver短约72% |
局限与改进
本文作者坦诚地指出了系统的几个局限性。首先，系统有时会生成过于冗长或结构不够良好的Lean代码。当需要填补的'sorry'涉及完整引理的证明时，生成的代码往往显得冗长，不如人工编写的Mathlib代码那样简洁和优雅。其次，系统在处理类型级别问题时偶尔会遇到困难，例如从Real到NNReal的类型转换问题。这类类型级别约束在非形式化数学中很少被明确说明，因此系统难以自主重构所需的结构。第三，与经验丰富的Mathlib贡献者编写的代码相比，生成的证明往往过于结果导向，依赖冗长的底层tactic脚本，缺乏结构化的抽象和惯用的高级模式使用。从独立观察来看，系统的性能高度依赖基础模型的能力，如果基础模型的推理能力不足，系统整体性能会受到显著影响。此外，系统的计算成本相对较高，某些困难问题（如A5题）的预算高达1000美元，这可能限制其在资源受限环境中的应用。
独立分析的弱点
本文存在几个值得深入分析的弱点。首先，系统对基础模型的依赖性过强，性能提升主要来自Claude Opus 4.5的强大推理能力，而非系统架构本身的创新。这意味着如果基础模型的能力达到瓶颈，系统的性能提升空间也会受限。改进方向包括开发更智能的工具选择策略和证明分解方法，减少对基础模型能力的依赖。其次，系统的计算成本较高，Putnam 2025基准测试中某些问题的预算高达1000美元，这限制了系统的实际应用范围。可以探索更高效的证明搜索策略，如基于蒙特卡洛树搜索的优先级调度，或开发轻量级的预筛选机制来减少不必要的尝试。第三，系统的证明质量（代码简洁性和可读性）仍有提升空间，生成的证明往往缺乏Mathlib社区代码的优雅结构。可以通过引入代码风格约束、参考优秀代码库的模式、或开发专门的证明优化模块来改进。第四，非形式化证明器的迭代策略（最多20次迭代）可能不够灵活，对于特别困难的问题可能需要更多的迭代次数，而对于简单问题则可能浪费资源。可以开发自适应的迭代策略，根据问题难度和证明进展动态调整迭代次数。
未来方向
基于本文的成果，未来研究可以从多个方向展开。首先，可以探索将本文的智能体范式扩展到其他形式化系统（如Isabelle、Coq），验证方法的通用性。其次，可以开发更高效的证明搜索算法，结合强化学习技术优化工具选择和证明策略。第三，可以进一步研究人机协作的形式化方法，开发更好的蓝图生成和优化算法，降低人类专家的参与成本。第四，可以探索多智能体协作的形式化证明，让多个专门的智能体分别处理不同类型的证明任务，提高整体效率。第五，可以研究证明的自动简化和优化，将冗长的证明自动重构为更简洁、更优雅的形式。最后，可以探索将形式化证明与非形式化推理更紧密地结合，开发能够自动在两种推理模式之间切换的混合系统。
复现评估
本文在可复现性方面做出了重要贡献。系统完全开源，所有代码和解决方案都在GitHub上公开（https://github.com/project-numina/numina-lean-agent）。这包括Numina-Lean-Agent的核心代码、MCP工具集成、以及Putnam 2025的所有解决方案。然而，完全复现该系统仍面临一些挑战：（1）需要访问Claude Opus 4.5等商业API，这会产生显著的计算成本；（2）系统依赖多个外部组件（Lean-LSP-MCP、LeanDex、Gemini IMO系统等），需要正确配置和集成；（3）某些组件（如GPT-5.2用于A5题的子智能体）可能不是公开可用的。从算力需求来看，系统采用纯顺序执行，但某些困难问题需要大量的API调用和长时间运行（如A5题耗时约2040分钟）。总体而言，本文为智能体形式化证明提供了重要的开源参考实现，但完全复现需要相当的技术能力和计算资源。
论文图表