传统形式化定理证明系统因高度定制而受限，扩展性与复现性不佳。一项新研究提出用通用代码Agent统一数学推理，无需额外训练即可实现高级别自动证明，为AI解决复杂数学问题提供了更开放、通用且易于工程实现的新思路。
智能速览
通用代码Agent可直接作为数学推理核心，无需专门训练。
系统性能随底层大模型升级而自然提升，避免了高成本训练。
通过MCP插件体系，实现多种工具的即插即用与自主调用。
结合LeanDex语义检索，有效降低了AI在证明过程中的幻觉。
子Agent与蓝图机制有效支撑长程证明，缓解上下文退化问题。
精华内容
这项名为Numina-Lean-Agent的新范式，究竟是如何通过通用代码Agent和巧妙的工具编排，打破传统证明系统的壁垒，实现Putnam级别的推理能力的？
核心范式转变
该研究的核心在于颠覆传统思路，不再为数学证明设计专用模型，而是直接采用如Claude Code这类通用代码Agent作为推理引擎。这种设计统一处理了证明、检索、调试与工程化任务，极大提升了系统的开放性、通用性与工程可复现性。
系统最大的优势之一是无需额外训练。其能力主要由底层大模型决定，这意味着更换更强的模型即可直接提升证明水平，有效避免了传统方法中高昂的强化学习或监督训练成本。
插件化工具体系
为实现高效协同，研究团队构建了基于Model Context Protocol (MCP)的插件化工具体系。这使得Lean形式化系统、语义检索、非形式证明生成乃至外部讨论模型都能够即插即用，并被Agent自主调用。
其中，Lean-LSP-MCP组件构建了一个真实的编译环境，让Agent可以查询Lean的当前目标和诊断信息，并行尝试多种策略，形成“尝试–反馈–优化”的自动闭环。而LeanDex语义检索工具则支持跨mathlib等库的自然语言检索，确保引用的定理真实存在且语境匹配，显著降低了AI的“幻觉”现象。
证明生成与校验
在非形式化证明的生成上，该系统采用了迭代精修机制。具体而言，通过Generator–Verifier双模型循环校验的Informal Prover，对生成的证明进行反复打磨和验证。
这种循环校验的方式，相比一次性的独立采样，能够显著提升证明的成功率和质量，确保最终输出的非形式化证明在逻辑上更加严谨和可靠。
长程推理支撑
面对复杂的长程证明任务，系统设计了专门的支撑机制。通过引入子Agent，可以将一个复杂的证明难题拆解为多个子问题，分别进行处理和攻克。
同时，利用Blueprint显式规划证明的DAG（有向无环图），为Agent提供清晰的证明路线图。这种机制有效缓解了长上下文带来的信息退化问题，确保AI在处理长篇、复杂的数学定理时仍能保持思路清晰和逻辑连贯。
Numina-Lean-Agent通过通用代码Agent的范式创新，显著提升了形式化数学推理的通用性与工程可行性。这项技术不仅为AI解决复杂数学问题铺平了道路，也预示着未来AI与专业领域工具深度融合的广阔前景，或许下一个数学难题将由AI来攻克？
