Numina-Lean-Agent: Um Sistema Aberto e Geral de Raciocínio Agente para Matemática Formal
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
Resumo
Os sistemas agentes tornaram-se recentemente o paradigma dominante para a demonstração formal de teoremas, alcançando desempenho notável ao coordenar múltiplos modelos e ferramentas. No entanto, as abordagens existentes frequentemente dependem de pipelines específicas para tarefas e provadores formais treinados, limitando sua flexibilidade e reprodutibilidade. Neste artigo, propomos o paradigma que utiliza diretamente um agente de codificação geral como um raciocinador matemático formal. Este paradigma é motivado por (1) Um agente de codificação geral fornece uma interface natural para diversas tarefas de raciocínio além da demonstração, (2) O desempenho pode ser melhorado simplesmente substituindo o modelo base subjacente, sem necessidade de treinamento, e (3) O MCP permite a extensão flexível e a chamada autônoma de ferramentas especializadas, evitando projetos complexos. Com base neste paradigma, introduzimos o Numina-Lean-Agent, que combina o Claude Code com o Numina-Lean-MCP para permitir interação autônoma com o Lean, recuperação de teoremas relevantes, demonstração informal e ferramentas auxiliares de raciocínio. Utilizando o Claude Opus 4.5 como modelo base, o Numina-Lean-Agent resolve todos os problemas do Putnam 2025 (12 / 12), igualando o melhor sistema de código fechado. Além da avaliação em benchmarks, demonstramos ainda sua generalidade ao interagir com matemáticos para formalizar com sucesso o teorema de Brascamp-Lieb. Disponibilizamos o Numina-Lean-Agent e todas as soluções em 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.