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를 결합한 Numina-Lean-Agent를 소개합니다. 이는 Lean과의 자율적 상호작용, 관련 정리 검색, 비형식적 증명 및 보조 추론 도구 활용을 가능하게 합니다. 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.