【第567期】Numina-Lean-Agent：通用数学形式化推理系统

Seventy3：借助NotebookLM的能力进行论文解读，专注人工智能、大模型、机器人算法、crypto方向，让大家跟着AI一起进步。

如果你想要解读自己的论文，获得更多曝光度。请联系小助手微信：seventy3_podcast 加群。合作邮箱：zhiwudazhanjiangshi#gmail.com

今天的主题是：

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Summary

智能体系统（Agentic systems）近期已成为形式化定理证明的主流范式，通过协调多个模型和工具实现了强劲的性能。然而，现有方法往往依赖于针对特定任务的流水线和经过专门训练的形式化证明器，这限制了它们的灵活性和可复现性。

在本文中，我们提出了一种直接将通用代码智能体（General coding agent）作为形式化数学推理器的范式。该范式的出发点在于：(1) 通用代码智能体为证明之外的各种推理任务提供了天然的接口；(2) 无需训练，仅通过更换底层基座模型即可提升性能；(3) 模型上下文协议（MCP）能够灵活扩展并自主调用专用工具，从而避免了复杂的系统设计。

基于这一范式，我们推出了 Numina-Lean-Agent，它将 Claude Code 与 Numina-Lean-MCP 相结合，实现了与 Lean 的自主交互、相关定理检索、非形式化证明以及辅助推理工具的调用。在使用 Claude 4.5 Opus 作为基座模型时，Numina-Lean-Agent 解决了 Putnam 2025 的所有题目（12/12），达到了顶尖闭源系统的水平。

除了基准测试评估外，我们还通过与数学家交互并成功形式化了 Brascamp-Lieb 定理，进一步展示了该系统的通用性。我们已在上述网址发布了 Numina-Lean-Agent 及其全部解题方案。

原文链接：https://arxiv.org/abs/2601.14027