Numina-Lean-Agent: Открытая и универсальная система агентного логического вывода для формальной математики
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
January 20, 2026
Авторы: 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
Аннотация
В последнее время агентные системы стали доминирующей парадигмой для формального доказательства теорем, демонстрируя высокую производительность за счет координации нескольких моделей и инструментов. Однако существующие подходы часто опираются на специализированные конвейеры и обученные формальные проверы, что ограничивает их гибкость и воспроизводимость. В данной статье мы предлагаем парадигму, которая напрямую использует универсального кодирующего агента в качестве формального математического решателя. Эта парадигма мотивирована следующими факторами: (1) универсальный кодирующий агент предоставляет естественный интерфейс для разнообразных задач логического вывода, выходящих за рамки доказательства теорем, (2) производительность может быть улучшена простой заменой базовой модели без дополнительного обучения и (3) MCP позволяет гибко расширять и автономно вызывать специализированные инструменты, избегая сложного проектирования. На основе этой парадигмы мы представляем Numina-Lean-Agent, который объединяет Claude Code с Numina-Lean-MCP для обеспечения автономного взаимодействия с Lean, поиска релевантных теорем, неформального доказательства и вспомогательных инструментов логического вывода. Используя Claude Opus 4.5 в качестве базовой модели, Numina-Lean-Agent решает все задачи Putnam 2025 (12 / 12), соответствуя лучшей проприетарной системе. Помимо бенчмарк-оценки, мы дополнительно демонстрируем универсальность системы, взаимодействуя с математиками для успешной формализации теоремы Браскама-Либа. Мы публикуем Numina-Lean-Agent и все решения по адресу 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.