Numina-Lean-Agent: Un Sistema de Razonamiento Agéntico Abierto y General para Matemáticas Formales
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
January 20, 2026
Autores: 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
Resumen
Los sistemas agentes se han convertido recientemente en el paradigma dominante para la demostración formal de teoremas, logrando un rendimiento sólido mediante la coordinación de múltiples modelos y herramientas. Sin embargo, los enfoques existentes a menudo dependen de pipelines específicos para cada tarea y de demostradores formales entrenados, lo que limita su flexibilidad y reproducibilidad. En este artículo, proponemos el paradigma que utiliza directamente un agente de codificación general como razonador de matemáticas formales. Este paradigma está motivado por: (1) Un agente de codificación general proporciona una interfaz natural para diversas tareas de razonamiento más allá de la demostración, (2) El rendimiento puede mejorarse simplemente reemplazando el modelo base subyacente, sin necesidad de entrenamiento, y (3) MCP permite la extensión flexible y la llamada autónoma de herramientas especializadas, evitando diseños complejos. Basándonos en este paradigma, presentamos Numina-Lean-Agent, que combina Claude Code con Numina-Lean-MCP para permitir la interacción autónoma con Lean, la recuperación de teoremas relevantes, y herramientas de demostración informal y razonamiento auxiliar. Utilizando Claude Opus 4.5 como modelo base, Numina-Lean-Agent resuelve todos los problemas del Putnam 2025 (12 / 12), igualando al mejor sistema de código cerrado. Más allá de la evaluación comparativa, demostramos además su generalidad interactuando con matemáticos para formalizar con éxito el teorema de Brascamp-Lieb. Publicamos Numina-Lean-Agent y todas las soluciones en 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.