Elamur Research⌕
☰
home / 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

Paper · 2026 · Junqi Liu, Zihao Zhou, Zekai Zhu et al.

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 EdinburghEdinburgh · United Kingdom396 works · 82,279 citations🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 citations🎓Imperial College LondonLondon · United Kingdom56 works · 13,671 citations🎓Tongji UniversityShanghai · China35 works · 3,012 citations🎓University of LiverpoolLiverpool · United Kingdom19 works · 840 citations🎓Xi’an Jiaotong-Liverpool UniversitySuzhou · China12 works · 334 citations🔬Academy of Mathematics and Systems ScienceBeijing · China2 works · 35 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.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. DOI 10.48550/arxiv.2601.14027 · arXiv 2601.14027

@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}
}

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
  2. Anthropic. Claude opus 4.5 system card. Technical report, November 2025. URL https://www.anthropic.com/ claude-opus-4-5-system-card. ↗
  3. Axiom Math Team. From seeing why to checking everything. https://axiommath.ai/territory/ from-seeing-why-to-checking-everything, 2025. Axiom Math blog post. ↗
  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
  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. 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. ↗
  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
  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
  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. Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
  10. Paulson, L. C. Isabelle: A generic theorem prover. Springer, 1994. find
  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. 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. 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
  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, 2024. URL https://a…

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/liu-2026-numina-lean-agent-open-general/