---
title: "Numina-Lean-Agent — paper by Liu et al. (2026)"
description: "The authors propose a different approach: use an off-the-shelf coding agent as the reasoner. 14 references, cited by 15 papers here."
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"]
year: 2026
venue: "arXiv:2601.14027"
source: "https://arxiv.org/abs/2601.14027"
doi: "10.48550/arxiv.2601.14027"
arxiv: "2601.14027"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/liu-2026-numina-lean-agent-open-general/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/liu-2026-numina-lean-agent-open-general/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2026](https://md.research.elamur.ai/free/en/papers/2026/) / Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

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

**Authors:** [Junqi Liu](https://md.research.elamur.ai/free/en/authors/junqi-liu/), [Zihao Zhou](https://md.research.elamur.ai/free/en/authors/zihao-zhou/), [Zekai Zhu](https://md.research.elamur.ai/free/en/authors/zekai-zhu/), [Marco Dos Santos](https://md.research.elamur.ai/free/en/authors/marco-dos-santos/), Weikun He, [Jiawei Liu](https://md.research.elamur.ai/free/en/authors/jiawei-liu/), [Ran Wang](https://md.research.elamur.ai/free/en/authors/ran-wang/), [Yunzhou Xie](https://md.research.elamur.ai/free/en/authors/yunzhou-xie/), Junqiao Zhao, [Qiufeng Wang](https://md.research.elamur.ai/free/en/authors/qiufeng-wang/), Lihong Zhi, [Jia Li](https://md.research.elamur.ai/free/en/authors/jia-li/) and [Wenda Li](https://md.research.elamur.ai/free/en/authors/wenda-li/) · **Year:** 2026 · **Venue:** arXiv:2601.14027 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2601.14027) · [PDF](https://arxiv.org/pdf/2601.14027) · [DOI 10.48550/arxiv.2601.14027](https://doi.org/10.48550/arxiv.2601.14027) · [arXiv 2601.14027](https://arxiv.org/abs/2601.14027) · [OpenAlex](https://openalex.org/W7125274582)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [15](https://md.research.elamur.ai/free/en/papers/liu-2026-numina-lean-agent-open-general/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Recent agentic systems for formal theorem proving perform well, but they often depend on custom pipelines and specially trained provers, and many are closed-source. The authors propose a different approach: use an off-the-shelf coding agent as the reasoner. Their system, Numina-Lean-Agent, pairs Claude Code with Numina-Lean-MCP, a set of tools exposed through the Model Context Protocol. These tools let the agent compile and inspect Lean code, search for relevant theorems, obtain informal proofs, and consult other LLMs. The agent decides on its own which tool to call. Because no model is trained, a stronger base model can simply be swapped in.

With Claude Opus 4.5 as the base model, the system solved every Putnam 2025 problem. This ties AxiomProver and beats Harmonic's Aristotle. It also helped a mathematician and a Lean expert formalize a recent result on Brascamp–Lieb inequalities, showing it is useful beyond benchmarks. The code and all solutions are publicly released, which supports reproducible research in formal mathematics.

## Key points
- **Toolkit.** Numina-Lean-MCP bundles four components:
  - Lean-LSP-MCP, for goal queries, diagnostics, running code and multi-attempt tactic trials;
  - LeanDex, a new agentic semantic search over mathlib and FLT for Lean v4.26.0, built on LeanExplore;
  - an Informal Prover, a generator–verifier loop on Gemini-3-Pro-Preview with up to 20 rounds, where a proof must pass three independent checks;
  - a Discussion Partner that queries external LLMs.
- **Putnam 2025 result: 12/12.** The evaluation used Seed-Prover 1.5's formal statements, strictly sequential execution and no web access. The budget was about $50 per problem, raised to roughly $1000 for A5.
- **Concise proofs.** For some problems, such as B1, the system's proofs were shorter than those of AxiomProver and Seed-Prover 1.5.
- **Brascamp–Lieb formalization.** In under two weeks, the team produced more than 8,000 lines of Lean. The agent contributed about 70 new definitions and lemmas, and it detected and fixed false statements on its own.
- **Limitations.**
  - Generated proofs tend to be verbose and not idiomatic Mathlib style.
  - The agent struggles with type-level issues; for example, a Real to NNReal conversion blocked one proof.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Edinburgh](https://md.research.elamur.ai/free/en/universities/university-of-edinburgh/) — University, Edinburgh, United Kingdom · 396 works · 82,279 citations
- [University of Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 287 works · 125,174 citations
- [Imperial College London](https://md.research.elamur.ai/free/en/universities/imperial-college-london/) — University, London, United Kingdom · 56 works · 13,671 citations
- [Tongji University](https://md.research.elamur.ai/free/en/universities/tongji-university/) — University, Shanghai, China · 35 works · 3,012 citations
- [University of Liverpool](https://md.research.elamur.ai/free/en/universities/university-of-liverpool/) — University, Liverpool, United Kingdom · 19 works · 840 citations
- [Xi’an Jiaotong-Liverpool University](https://md.research.elamur.ai/free/en/universities/xi-an-jiaotong-liverpool-university/) — University, Suzhou, China · 12 works · 334 citations
- [Academy of Mathematics and Systems Science](https://md.research.elamur.ai/free/en/labs/academy-of-mathematics-and-systems-science/) — Research institute, Beijing, China · 2 works · 35 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: 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 and Wenda Li. 2026. Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics. arXiv:2601.14027.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{liu2026numina,
  title = {{Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics}},
  author = {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 and Wenda Li},
  year = {2026},
  doi = {10.48550/arxiv.2601.14027},
  eprint = {2601.14027},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2601.14027}
}
```

- [← previous FoE: Forest of Errors Makes the First Solution the Best in Large Reasoning Models](https://md.research.elamur.ai/free/en/papers/jiang-2026-foe-forest-errors-makes-first/)
- [next → Qwen3-Coder-Next Technical Report](https://md.research.elamur.ai/free/en/papers/cao-2026-qwen3-coder-next-technical/)
- [↑ back to papers of 2026](https://md.research.elamur.ai/free/en/papers/2026/)

## References

14 references, 7 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Achim, T., Best, A., Bietti, A., Der, K., Fédérico, M., Gukov, S., Halpern-Leistner, D., Henningsgard, K., Kudryashov, Y., Meiburg, A., Michelsen, M., Patterson, R., Rodriguez, E., Scharff, L., Shanker, V., Sicca, V., Sowrirajan, H., Swope, A., Tamas, M., Tenev, V., Thomm, J., Williams, H., and Wu… — [Aristotle: IMO-level Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/)
2. Anthropic. Claude opus 4.5 system card. Technical report, November 2025. URL [https://www.anthropic.com/](https://www.anthropic.com/) claude-opus-4-5-system-card. [↗](https://www.anthropic.com/)
3. Axiom Math Team. From seeing why to checking everything. [https://axiommath.ai/territory/](https://axiommath.ai/territory/) from-seeing-why-to-checking-everything, 2025. Axiom Math blog post. [↗](https://axiommath.ai/territory/)
4. Bénard, T. and He, W. Effective brascamp-lieb inequalities. arXiv preprint arXiv:2511.11091, 2025. — [arXiv:2511.11091](https://arxiv.org/abs/2511.11091) [find](https://scholar.google.com/scholar?q=Be%CC%81nard%2C+T%2E+and+He%2C+W%2E+Effective+brascamp%2Dlieb+inequalities%2E+arXiv+preprint+arXiv%3A2511%2E11091%2C+2025%2E+%E2%80%94+%5BarXiv%3A2511%2E11091%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2511%2E11091%29)
5. Chen, J., Chen, W., Du, J., Hu, J., Jiang, Z., Jie, A., Jin, X., Jin, X., Li, C., Shi, W., et al. [Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-1-5/). arXiv preprint arXiv:2512.17260, 2025. de Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J.…
6. Dressler, O. Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover, 3 2025. URL [https://github.com/oOo0oOo/lean-lsp-mcp](https://github.com/oOo0oOo/lean-lsp-mcp). [↗](https://github.com/oOo0oOo/lean-lsp-mcp)
7. Huang, Y. and Yang, L. F. Winning gold at imo 2025 with a model-agnostic verification-and-refinement pipeline. arXiv preprint arXiv:2507.15855, 2025. — [arXiv:2507.15855](https://arxiv.org/abs/2507.15855) [find](https://scholar.google.com/scholar?q=Huang%2C+Y%2E+and+Yang%2C+L%2E+F%2E+Winning+gold+at+imo+2025+with+a+model%2Dagnostic+verification%2Dand%2Drefinement+pipeline%2E+arXiv+preprint+arXiv%3A2507%2E15855%2C+2025%2E+%E2%80%94+%5BarXiv%3A2507%2E15855%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2507%2E15)
8. Hubert, T., Mehta, R., Sartran, L., Horváth, M. Z., Žužić, G., Wieser, E., Huang, A., Schrittwieser, J., Schroecker, Y., Masoom, H., Bertolli, O., Zahavy, T., Mandhane, A., Yung, J., Beloshapka, I., Ibarz, B., Veeriah, V., Yu, L., Nash, O., Lezeau, P., Mercuri, S., Sönne, C., Mehta, B., Davies,… [find](https://scholar.google.com/scholar?q=Hubert%2C+T%2E%2C+Mehta%2C+R%2E%2C+Sartran%2C+L%2E%2C+Horva%CC%81th%2C+M%2E+Z%2E%2C+Z%CC%8Cuz%CC%8Cic%CC%81%2C+G%2E%2C+Wieser%2C+E%2E%2C+Huang%2C+A%2E%2C+Schrittwieser%2C+J%2E%2C+Schroecker%2C+Y%2E%2C+Masoom%2C+H%2E%2C+Bertolli%2C+O%2E%2C+Zahavy%2C+T%2E%2C+Mandhane%2C+A%2E%2C+Yung%2C+J%2E%2C+Beloshapka%2C+I)
9. Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
10. Paulson, L. C. Isabelle: A generic theorem prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=Paulson%2C+L%2E+C%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2C+1994%2E)
11. Ren, Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., et al. [Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/). arXiv preprint arXiv:2504.21801, 2025.
12. Varambally, S., Voice, T., Sun, Y., Chen, Z., Yu, R., and Ye, K. [Hilbert: Recursively building formal proofs with informal reasoning](https://md.research.elamur.ai/free/en/papers/varambally-2025-hilbert-recursively-building-formal-proofs/). arXiv preprint arXiv:2509.22819, 2025.
13. Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., Lu, J., de Saxcé, H., Bailey, B., Song, C., Xiao, C., Zhang, D., Zhang, E., Pu, F., Zhu, H., Liu, J., Bayer, J., Michel, J., Yu, L., Dreyfus-Schmidt, L., Tunstall, L., Pagani, L., Machado, M.,… — [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/)
14. Xin, H., Ren, Z. Z., Song, J., Shao, Z., Zhao, W., Wang, H., Liu, B., Zhang, L., Lu, X., Du, Q., Gao, W., Zhu, Q., Yang, D., Gou, Z., Wu, Z. F., Luo, F., and Ruan, C. [Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/), 2024. URL https://a…

*Updated 3 November 2026*