Numina-Lean-Agent：面向形式数学的开放通用Agentic推理系统

Agentic 系统近来已成为形式定理证明的主导范式，通过协调多个模型与工具取得强劲表现。然而，现有方法常依赖任务特定管线与经过训练的形式证明器，限制了灵活性与可复现性。本文提出直接把通用编码智能体用作形式数学推理器的范式。该范式的动机在于：(1) 通用编码智能体为证明之外的多样推理任务提供自然接口；(2) 仅替换底层基座模型即可提升性能，无需训练；(3) MCP 支持灵活扩展与自主调用专门工具，避免复杂设计。基于该范式，我们推出 Numina-Lean-Agent，它把 Claude Code 与 Numina-Lean-MCP 结合，实现与 Lean 的自主交互、相关定理检索、非形式证明及辅助推理工具。以 Claude Opus 4.5 为基座模型，Numina-Lean-Agent 解出 Putnam 2025 全部问题（12/12），与最佳闭源系统持平。除基准评估外，我们进一步通过与数学家互动成功形式化 Brascamp-Lieb 定理，展示其通用性。我们在 https://github.com/project-numina/numina-lean-agent 发布 Numina-Lean-Agent 与全部解答。