Numina-Lean-Agent: 形式的数学のためのオープンで汎用的なエージェント推論システム

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

January 20, 2026

著者: Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, Wenda Li

cs.AI

要旨

エージェントシステムは近年、形式的定理証明における主流のパラダイムとなり、複数のモデルとツールを連携させることで高い性能を達成している。しかし、既存のアプローチはタスク固有のパイプラインや訓練された形式的証明器に依存することが多く、柔軟性と再現性が制限されている。本論文では、汎用のコーディングエージェントを形式的数学推論器として直接利用するパラダイムを提案する。このパラダイムは以下の観点に基づく。(1) 汎用コーディングエージェントは、証明を超えた多様な推論タスクに対する自然なインターフェースを提供する。(2) 訓練を必要とせず、基盤モデルを置き換えるだけで性能向上が可能である。(3) MCPが専門ツールの柔軟な拡張と自律的呼び出しを可能にし、複雑な設計を回避できる。このパラダイムに基づき、Claude CodeとNumina-Lean-MCPを組み合わせ、Leanとの自律的な対話、関連定理の検索、非形式的証明、補助的推論ツールを実現するNumina-Lean-Agentを導入する。基盤モデルにClaude Opus 4.5を使用したNumina-Lean-Agentは、Putnam 2025の問題全て（12問中12問）を解決し、最高性能のクローズドソースシステムに匹敵する結果を示した。ベンチマーク評価に加え、数学者との対話を通じてBrascamp-Lieb定理の形式化に成功した事例を示し、その汎用性をさらに実証する。Numina-Lean-Agent及び全ての解答をhttps://github.com/project-numina/numina-lean-agent で公開する。

English

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.