Numina-Lean-Agent: Een Open en Algemeen Agentisch Redeneersysteem voor Formele Wiskunde
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
January 20, 2026
Auteurs: 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
Samenvatting
Agentische systemen zijn recentelijk het dominante paradigma geworden voor formeel bewijzen, waarbij ze sterke prestaties bereiken door meerdere modellen en tools te coördineren. Bestaande benaderingen vertrouwen echter vaak op taakspecifieke pijplijnen en getrainde formele bewijssystemen, wat hun flexibiliteit en reproduceerbaarheid beperkt. In dit artikel stellen we het paradigma voor dat rechtstreeks een algemene codeer-agent gebruikt als formeel wiskundig redeneerder. Dit paradigma wordt gemotiveerd door: (1) een algemene codeer-agent biedt een natuurlijke interface voor diverse redeneertaken die verder gaan dan bewijzen, (2) de prestaties kunnen worden verbeterd door simpelweg het onderliggende basismodel te vervangen, zonder training, en (3) MCP maakt flexibele uitbreiding en autonoom aanroepen van gespecialiseerde tools mogelijk, wat complex ontwerp vermijdt. Gebaseerd op dit paradigma introduceren we Numina-Lean-Agent, dat Claude Code combineert met Numina-Lean-MCP om autonome interactie met Lean, retriev
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.