Elamur Research⌕
☰
home / papers / 2025 / Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

Paper · 2025 · Kaito Baba, Chaoran Liu, Shuhei Kurita et al.

Summary

Writing proofs that a formal system such as Lean will accept takes a lot of manual work. LLMs do well on informal mathematics, but they rarely produce Lean code that passes verification. The authors present Prover Agent, a pipeline with three parts: a general LLM that reasons in natural language, a specialized model that writes formal proofs, and the Lean checker. Lean's error messages go back to the prover, which revises its proof over repeated rounds.

When a direct proof attempt fails, the agent proposes auxiliary lemmas. These can be subgoals of a planned proof, but also special cases, consequences of the hypotheses, or conjectures. Each lemma is proved separately, and the verified results are then used to build a proof of the original statement. Unlike decomposition methods that need a full proof sketch from the start, this lets a strategy emerge bottom-up.

Using only small language models, the system reaches 88.1% on MiniF2F and solves 25 PutnamBench problems with lower sample and token budgets than prior systems. This is a new best among SLM-based methods and suggests that good orchestration can partly substitute for model scale.

Key points

  • Prover Agent achieves 88.1% success on MiniF2F, and on PutnamBench it proves 25 problems. Both results are state-of-the-art among SLM-based approaches, achieved with fewer samples and tokens.
  • The motivation is the gap between informal and formal ability. For example, o3-mini produces a complete, correct Lean proof for competition problems in only 6.0% of single attempts.
  • Lean feedback drives refinement up to a fixed attempt limit (N_refine). Lemmas that remain too hard can be split recursively into smaller lemmas, up to a depth limit D, and unprovable lemmas are simply discarded.
  • In a case study, a generated special-case lemma (n = 3) led the model quickly to an induction-based proof. Without lemmas, the model wandered without a clear plan and failed.
  • The code is released at github.com/kAIto47802/Prover-Agent. The authors suggest the method could extend to other formal domains, such as software verification.

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

 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 Kaito Baba, Chaoran Liu, Shuhei Kurita and Akiyoshi Sannai. 2025. Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs. arXiv:2506.19923.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2506.19923 · arXiv 2506.19923

@misc{baba2025prover,
  title = {{Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs}},
  author = {Kaito Baba, Chaoran Liu, Shuhei Kurita and Akiyoshi Sannai},
  year = {2025},
  doi = {10.48550/arxiv.2506.19923},
  eprint = {2506.19923},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2506.19923}
}

References

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

  1. Anthony, T., Tian, Z., and Barber, D. Thinking fast and slow with deep learning and tree search. In Advances in Neural Information Processing Systems, volume 30, 2017.
  2. Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  3. Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. Measuring mathematical problem solving with the MATH dataset. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2), 2021.
  4. Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.-C., Giménez, E., Herbelin, H., et al. The Coq proof assistant reference manual. INRIA, version, 6(11):17–21, 1999. find
  5. Huang, J., Chen, X., Mishra, S., Zheng, H. S., Yu, A. W., Song, X., and Zhou, D. Large language models cannot self-correct reasoning yet. In The Twelfth International Conference on Learning Representations, 2024.
  6. Cao, C., Song, L., Li, Z., Le, X., Zhang, X., Xue, H., and Yang, F. Reviving DSP for advanced theorem prov-Huang, L., Yu, W., Ma, W., Zhong, W., Feng, Z., Wang, H., Chen, Q., Peng, W., Feng, X., Qin, B., and Liu, T. A survey on hallucination in large language models: Principles, taxonomy, challenges… — A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions
  7. Li, Y., Du, D., Song, L., Li, C., Wang, W., Yang, T., and Mi, H. HunyuanProver: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2025.
  8. Irving, G., Szegedy, C., Alemi, A. A., Een, N., Chollet, F., and Urban, J. DeepMath - deep sequence models for premise selection. In Advances in Neural Information Processing Systems, volume 29, 2016.
  9. Lin, H., Sun, Z., Welleck, S., and Yang, Y. Lean-STaR: Learning to interleave thinking and proving. In The Thirteenth International Conference on Learning Representations, 2025a.
  10. Ji, X., Liu, Y., Wang, Q., Zhang, J., Yue, Y., Shi, R., Sun, C., Zhang, F., Zhou, G., and Gai, K. Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. arXiv preprint arXiv:2507.08649, 2025. — [arXiv:2507.08649](https://arxiv.org/abs/2507.08649) find
  11. Lin, Y., Tang, S., Lyu, B., Wu, J., Lin, H., Yang, K., Li, J., Xia, M., Chen, D., Arora, S., and Jin, C. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025b.
  12. Lin, Y., Tang, S., Lyu, B., Yang, Z., Chung, J.-H., Zhao, H., Jiang, L., Geng, Y., Ge, J., Sun, J., Wu, J., Gesi, J., Lu, X., Acuna, D., Yang, K., Lin, H., Choi, Y., Chen, D., Arora, S., and Jin, C. Goedel-Prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.…
  13. Ji, Z., Lee, N., Frieske, R., Yu, T., Su, D., Xu, Y., Ishii, E., Bang, Y. J., Madotto, A., and Fung, P. Survey of hallucination in natural language generation. ACM Computing Surveys, 55(12), 2023. ISSN 0360-0300. doi: 10.1145/3571730.
  14. Jiang, A. Q., Li, W., Han, J. M., and Wu, Y. LISA: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, 2021. find
  15. Lu, P., Qiu, L., Yu, W., Welleck, S., and Chang, K.-W. A survey of deep learning for mathematical reasoning. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 14605–14631. Association for Computational Linguistics, 2023. doi: 10.1… find
  16. Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023. mathlib Community, T. The lean mathemati…
  17. Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, volume 31, 2018.
  18. Kwon, W., Li, Z., Zhuang, S., Sheng, Y., Zheng, L., Yu, C. H., Gonzalez, J., Zhang, H., and Stoica, I. Efficient memory management for large language model serving with pagedattention. In Proceedings of the 29th Symposium on Operating Systems Principles, pp. 611–626. Association for Computing Machin…
  19. Megill, N. D. and Wheeler, D. A. Metamath: A Computer Language for Pure Mathematics, 2019. URL http://us.metamath.org/downloads/ metamath.pdf. ↗
  20. Moura, L. d. and Ullrich, S. The lean 4 theorem prover and programming language. In Automated Deduction—CADE 28: 28th International Conference on Automated Deduction, Virtual Event, LNCS 12699, pp. 625–635. Springer-Verlag, 2021. doi: 10.1007/978-3-030-79876-5 37.
  21. 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. In Advances in Neural Information Processing Systems, volume 35, pp. 26337–26349, 2022.
  22. Newell, A. and Simon, H. The logic theory machine–a complex information processing system. IRE Transactions on Information Theory, 2(3):61–79, 1956. doi: 10.1109/TIT.1956.1056797.
  23. Lewkowycz, A., Andreassen, A., Dohan, D., Dyer, E., Michalewski, H., Ramasesh, V., Slone, A., Anil, C., Schlag, I., Gutman-Solo, T., Wu, Y., Neyshabur, B., Gur-Ari, G., and Misra, V. Solving quantitative reasoning problems with language models. In Advances in Neural Information Processing Systems, v…
  24. OpenAI. OpenAI o1 system card. arXiv:2412.16720, 2024. arXiv preprint OpenAI. OpenAI o3-mini, 2025. URL https://openai.com/index/openai-o3-mini/. ↗
  25. Paulson, L. C. Isabelle a Generic Theorem Prover. Springer Verlag, 1994. on Neural Information Processing Systems Datasets and Benchmarks Track, 2024b. find
  26. Polu, S. and Sutskever, I. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  27. 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.
  28. Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, 2023.
  29. Wang, H., Yuan, Y., Liu, Z., Shen, J., Yin, Y., Xiong, J., Xie, E., Shi, H., Li, Y., Li, L., Yin, J., Li, Z., and Liang, X. DT-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Annual Meeting of the Association for Computati…
  30. Rafailov, R., Sharma, A., Mitchell, E., Manning, C. D., Ermon, S., and Finn, C. Direct preference optimization: Your language model is secretly a reward model. In Advances in Neural Information Processing Systems, volume 36, pp. 53728–53741, 2023.
  31. Wang, H., Xin, H., Liu, Z., Li, W., Huang, Y., Lu, J., Yang, Z., Tang, J., Yin, J., Li, Z., and Liang, X. Proving theorems recursively. In Advances in Neural Information Processing Systems, volume 37, pp. 86720–86748, 2024a.
  32. Ren, Z. Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., Wu, Z. F., Gou, Z., Ma, S., Tang, H., Liu, Y., Gao, W., Guo, D., and Ruan, C. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv pre…
  33. 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
  34. Shen, Z., Huang, N., Yang, F., Wang, Y., Gao, G., Xu, T., Jiang, J., He, W., Yang, P., Sun, M., Ju, H., Wu, P., Dai, B., and Dong, B. REAL-Prover: Retrieval augmented Lean prover for mathematical reasoning. arXiv preprint arXiv:2505.20613, 2025.
  35. Song, Y., Zhang, H., Eisenach, C., Kakade, S. M., Foster, D., and Ghai, U. Mind the gap: Examining the self-improvement capabilities of large language models. In The Thirteenth International Conference on Learning Representations, 2025. find
  36. Wang, R., Zhang, J., Jia, Y., Pan, R., Diao, S., Pi, R., and Zhang, T. TheoremLlama: Transforming general-purpose LLMs into lean4 experts. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp. 11953–11974. Association for Computational Linguistics, 2024b. doi…
  37. Stechly, K., Valmeekam, K., and Kambhampati, S. On the self-verification limitations of large language models on reasoning and planning tasks. In The Thirteenth International Conference on Learning Representations, 2025.
  38. Wei, J., Wang, X., Schuurmans, D., Bosma, M., ichter, b., Xia, F., Chi, E., Le, Q. V., and Zhou, D. Chain-of-thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems, volume 35, pp. 24824–24837, 2022.
  39. Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling, 2024.
  40. Tsoukalas, G., Lee, J., Jennings, J., Xin, J., Ding, M., Jennings, M., Thakur, A., and Chaudhuri, S. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. In Advances in Neural Information Processing Systems, volume 37, pp. 11545–11569, 2024a.
  41. Wolf, T., Debut, L., Sanh, V., Chaumond, J., Delangue, C., Moi, A., Cistac, P., Rault, T., Louf, R., Funtowicz, M., Davison, J., Shleifer, S., von Platen, P., Ma, C., Jernite, Y., Plu, J., Xu, C., Le Scao, T., Gugger, S., Drame, M., Lhoest, Q., and Rush, A. Transformers: State-of-the-art natural lan… — Transformers: State-of-the-Art Natural Language Processing
  42. Tsoukalas, G., Lee, J., Jennings, J., Xin, J., Ding, M., Jennings, M., Thakur, A., and Chaudhuri, S. PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. In The Thirty-eight Conference Wu, M., Norrish, M., Walder, C., and Dezfouli, A. Tacticzero: Learning to prove t… — TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
  43. Yang, K., Poesia, G., He, J., Li, W., Lauter, K. E., Chaudhuri, S., and Song, D. Position: Formal mathematical reasoning—a new frontier in AI. In Forty-second International Conference on Machine Learning Position Paper Track, 2025b. — Formal Mathematical Reasoning: A New Frontier in AI
  44. Wu, Z., Huang, S., Zhou, Z., Ying, H., Wang, J., Lin, D., and Chen, K. InternLM2.5-StepProver: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024a.
  45. Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., and Chen, K. Lean workbook: A large-scale lean problem set formalized from natural language math problems. In Advances in Neural Information Processing Systems, volume 37, pp. 105848–105863, 2024.
  46. Wu, Z., Wang, J., Lin, D., and Chen, K. LEAN-GitHub: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227, 2024b.
  47. Yousefzadeh, R. and Cao, X. A lean dataset for international math olympiad: Small steps towards writing math proofs for hard problems. Transactions on Machine Learning Research, 2025. ISSN 2835-8856.
  48. 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. International Confe…
  49. Zeng, Z., Cheng, Q., Yin, Z., Zhou, Y., and Qiu, X. Revisiting the test-time scaling of o1-like models: Do they truly possess test-time scaling capabilities? arXiv preprint arXiv:2502.12215, 2025.
  50. Zhang, J., Wang, Q., Ji, X., Liu, Y., Yue, Y., Zhang, F., Zhang, D., Zhou, G., and Gai, K. Leanabell-Prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025.
  51. Xin, R., Xi, C., Yang, J., Chen, F., Wu, H., Xiao, X., Sun, Y., Zheng, S., and Shen, K. BFS-Prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025b.
  52. Zheng, K., Han, J. M., and Polu, S. miniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022.
  53. Xu, Z., Jain, S., and Kankanhalli, M. Hallucination is inevitable: An innate limitation of large language models. arXiv preprint arXiv:2401.11817, 2025.
  54. Zhou, A., Yan, K., Shlapentokh-Rothman, M., Wang, H., and Wang, Y.-X. Language agent tree search unifies reasoning, acting, and planning in language models. In Proceedings of the 41st International Conference on Machine Learning, volume 235, pp. 62138–62160. PMLR, 2024. find
  55. Yang, A., Zhang, B., Hui, B., Gao, B., Yu, B., Li, C., Liu, D., Tu, J., Zhou, J., Lin, J., Lu, K., Xue, M., Lin, R., Liu, T., Ren, X., and Zhang, Z. Qwen2.5-Math technical report: Toward mathematical expert model via self-improvement. arXiv preprint arXiv:2409.12122, 2024.
  56. Zhou, Y., Zhao, J., Zhang, Y., Wang, B., Wang, S., Chen, L., Wang, J., Chen, H., Jie, A., Zhang, X., Wang, H., Trung, L., Ye, R., Hoang, P. N., Zhang, H., Sun, P., and Li, H. Solving formal math problems by decomposition and iterative reflection. arXiv preprint arXiv:2507.15225, 2025.
  57. Yang, A., Li, A., Yang, B., Zhang, B., Hui, B., Zheng, B., Yu, B., Gao, C., Huang, C., Lv, C., Zheng, C., Liu, D., Zhou, F., Huang, F., Hu, F., Ge, H., Wei, H., Lin, H., Tang, J., Yang, J., Tu, J., Zhang, J., Yang, J., Yang, J., Zhou, J., Zhou, J., Lin, J., Dang, K., Bao, K., Yang, K., Yu, L., Deng,… — Qwen3 Technical Report
  58. Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. LeanDojo: Theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems, volume 36, pp. 21573–21612, 2023.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/baba-2025-prover-agent-agent-based-framework/