Numina-Lean-Agent: Ein offenes und allgemeines agentenbasiertes Reasoning-System für formale Mathematik
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
January 20, 2026
papers.authors: 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
papers.abstract
Agentische Systeme sind in jüngster Zeit zum dominanten Paradigma für formales Theorembeweisen geworden und erzielen starke Leistungen durch die Koordination mehrerer Modelle und Werkzeuge. Allerdings basieren bestehende Ansätze oft auf aufgabenspezifischen Pipelines und trainierten formalen Beweisern, was ihre Flexibilität und Reproduzierbarkeit einschränkt. In diesem Artikel schlagen wir das Paradigma vor, das direkt einen allgemeinen Coding-Agenten als formalen mathematischen Reasoner verwendet. Dieses Paradigma ist motiviert durch (1) Ein allgemeiner Coding-Agent bietet eine natürliche Schnittstelle für diverse Reasoning-Aufgaben über das Beweisen hinaus, (2) Die Leistung kann durch einfaches Ersetzen des zugrundeliegenden Basismodells ohne Training verbessert werden, und (3) MCP ermöglicht flexible Erweiterung und autonomen Aufruf spezialisierter Werkzeuge, wodurch komplexe Designs vermieden werden. Basierend auf diesem Paradigma stellen wir Numina-Lean-Agent vor, das Claude Code mit Numina-Lean-MCP kombiniert, um autonome Interaktion mit Lean, Abruf relevanter Theoreme, informelles Beweisen und auxiliary Reasoning-Werkzeuge zu ermöglichen. Mit Claude Opus 4.5 als Basismodell löst Numina-Lean-Agent alle Probleme im Putnam 2025 (12 / 12) und erreicht damit die Leistung des besten Closed-Source-Systems. Über die Benchmark-Bewertung hinaus demonstrieren wir weiterhin seine Allgemeingültigkeit, indem wir mit Mathematikern interagieren, um den Brascamp-Lieb-Satz erfolgreich zu formalisieren. Wir veröffentlichen Numina-Lean-Agent und alle Lösungen unter 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.