Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing approaches often rely on task-specific pipelines and trained formal provers, limiting their flexibility and reproducibility. In this paper, we propose the paradigm that directly uses a general coding agent as a formal math reasoner. This paradigm is motivated by (1) A general coding agent provides a natural interface for diverse reasoning tasks beyond proving, (2) Performance can be improved by simply replacing the underlying base model, without training, and (3) MCP enables flexible extension and autonomous calling of specialized tools, avoiding complex design. Based on this paradigm, we introduce Numina-Lean-Agent, which combines Claude Code with Numina-Lean-MCP to enable autonomous interaction with Lean, retrieval of relevant theorems, informal proving and auxiliary reasoning tools. Using Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all problems in Putnam 2025 (12 / 12), matching the best closed-source system. Beyond benchmark evaluation, we further demonstrate its generality by interacting with mathematicians to successfully formalize the Brascamp-Lieb theorem. We release Numina-Lean-Agent and all solutions at https://github.com/project-numina/numina-lean-agent.

翻译：智能体系统近来已成为形式定理证明的主导范式，通过协调多个模型与工具实现了强大的性能。然而，现有方法通常依赖于任务特定的流程和经过训练的形式证明器，限制了其灵活性与可复现性。本文提出一种直接使用通用编码智能体作为形式数学推理器的新范式。该范式的动机在于：（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 及所有解答。