Numina-Lean-Agent: Un Sistema di Ragionamento Agente Aperto e Generale per la Matematica Formale
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
January 20, 2026
Autori: 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
Abstract
I sistemi agentici sono recentemente diventati il paradigma dominante per la dimostrazione formale di teoremi, raggiungendo prestazioni elevate attraverso il coordinamento di più modelli e strumenti. Tuttavia, gli approcci esistenti spesso si basano su pipeline specifiche per task e dimostratori formali addestrati, limitandone la flessibilità e la riproducibilità. In questo articolo, proponiamo il paradigma che utilizza direttamente un agente di codifica generale come ragionatore matematico formale. Questo paradigma è motivato da: (1) Un agente di codifica generale fornisce un'interfaccia naturale per task di ragionamento diversificati oltre la dimostrazione, (2) Le prestazioni possono essere migliorate semplicemente sostituendo il modello base sottostante, senza addestramento, e (3) MCP consente l'estensione flessibile e la chiamata autonoma di strumenti specializzati, evitando progettazioni complesse. Basandoci su questo paradigma, introduciamo Numina-Lean-Agent, che combina Claude Code con Numina-Lean-MCP per abilitare l'interazione autonoma con Lean, il recupero di teoremi rilevanti, strumenti di dimostrazione informale e ragionamento ausiliario. Utilizzando Claude Opus 4.5 come modello base, Numina-Lean-Agent risolve tutti i problemi del Putnam 2025 (12 / 12), eguagliando il miglior sistema closed-source. Oltre alla valutazione su benchmark, dimostriamo ulteriormente la sua generalità interagendo con matematici per formalizzare con successo il teorema di Brascamp-Lieb. Rilasciamo Numina-Lean-Agent e tutte le soluzioni su 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.