Numina-Lean-Agent : Un système de raisonnement agentique ouvert et général pour les mathématiques formelles
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
Les systèmes agentiques sont récemment devenus le paradigme dominant pour la démonstration formelle de théorèmes, atteignant des performances remarquables en coordonnant plusieurs modèles et outils. Cependant, les approches existantes reposent souvent sur des pipelines spécifiques aux tâches et sur des démonstrateurs formels entraînés, limitant ainsi leur flexibilité et leur reproductibilité. Dans cet article, nous proposons un paradigme qui utilise directement un agent de codage général comme raisonneur mathématique formel. Ce paradigme est motivé par : (1) un agent de codage général fournit une interface naturelle pour des tâches de raisonnement diverses au-delà de la démonstration, (2) les performances peuvent être améliorées en remplaçant simplement le modèle de base sous-jacent, sans entraînement, et (3) MCP permet une extension flexible et un appel autonome d'outils spécialisés, évitant une conception complexe. Sur la base de ce paradigme, nous présentons Numina-Lean-Agent, qui combine Claude Code avec Numina-Lean-MCP pour permettre une interaction autonome avec Lean, la récupération de théorèmes pertinents, ainsi que des outils de démonstration informelle et de raisonnement auxiliaire. Utilisant Claude Opus 4.5 comme modèle de base, Numina-Lean-Agent résout tous les problèmes du Putnam 2025 (12 / 12), égalant ainsi le meilleur système propriétaire. Au-delà de l'évaluation sur benchmark, nous démontrons également sa généralité en collaborant avec des mathématiciens pour formaliser avec succès le théorème de Brascamp-Lieb. Nous publions Numina-Lean-Agent et toutes les solutions sur 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.