Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, Wenda Li
Proceedings of the 43rd International Conference on Machine Learning, PMLR 306:80284-80297, 2026.

Abstract

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v306-liu26gp, title = {Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics}, author = {Liu, Junqi and Zhou, Zihao and Zhu, Zekai and Dos Santos, Marco and He, Weikun and Liu, Jiawei and Xie, Yunzhou and Zhao, Junqiao and Wang, Qiufeng and Zhi, Lihong and Li, Jia and Li, Wenda}, booktitle = {Proceedings of the 43rd International Conference on Machine Learning}, pages = {80284--80297}, year = {2026}, editor = {Zhang, Tong and Dudik, Miroslav and Jaggi, Martin and Agarwal, Alekh and Li, Sharon and Schuurmans, Dale and Zhu, Jerry and Berkenkamp, Felix and Dong, Hanze and Bietti, Alberto}, volume = {306}, series = {Proceedings of Machine Learning Research}, month = {06--11 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v306/main/assets/liu26gp/liu26gp.pdf}, url = {https://proceedings.mlr.press/v306/liu26gp.html}, abstract = {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.} }
Endnote
%0 Conference Paper %T Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics %A Junqi Liu %A Zihao Zhou %A Zekai Zhu %A Marco Dos Santos %A Weikun He %A Jiawei Liu %A Yunzhou Xie %A Junqiao Zhao %A Qiufeng Wang %A Lihong Zhi %A Jia Li %A Wenda Li %B Proceedings of the 43rd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2026 %E Tong Zhang %E Miroslav Dudik %E Martin Jaggi %E Alekh Agarwal %E Sharon Li %E Dale Schuurmans %E Jerry Zhu %E Felix Berkenkamp %E Hanze Dong %E Alberto Bietti %F pmlr-v306-liu26gp %I PMLR %P 80284--80297 %U https://proceedings.mlr.press/v306/liu26gp.html %V 306 %X 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.
APA
Liu, J., Zhou, Z., Zhu, Z., Dos Santos, M., He, W., Liu, J., Xie, Y., Zhao, J., Wang, Q., Zhi, L., Li, J. & Li, W.. (2026). Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics. Proceedings of the 43rd International Conference on Machine Learning, in Proceedings of Machine Learning Research 306:80284-80297 Available from https://proceedings.mlr.press/v306/liu26gp.html.

Related Material