Elamur Research⌕
☰
home / papers / 2025 / FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

Paper · 2025 · Zhouliang Yu, Ruotian Peng, Keyi Ding et al.

Summary

Lean4 benchmarks for formal theorem proving, such as MiniF2F and ProofNet, are small and cover few areas of mathematics. Strong provers are also close to saturating them. FormalMATH addresses this with 5,560 verified Lean4 statements, from high-school Olympiad problems to undergraduate theorems. Topics include algebra, calculus, number theory, discrete and applied mathematics, and more. To avoid formalizing everything by hand, the authors built a human-in-the-loop pipeline. Several LLM autoformalizers propose candidates through best-of-N sampling. The Lean4 compiler then removes ill-formed outputs, multiple LLMs check that the meaning matches the original problem, and off-the-shelf provers try to prove the negation to catch false statements. Human experts review whatever survives. Tests of leading LLM-based provers show the benchmark is hard: the best system solves only about one problem in six. The analysis also uncovers uneven performance across domains, shortcut use of automation tactics, and lower success when natural-language solutions are added to the prompt. These findings give concrete directions for improving provers.

Key points

  • FormalMATH has 5,560 Lean4 statements, about 22.8× the size of MiniF2F (244 test problems). For comparison, ProofNet has 186.
  • Automatic filtering keeps 72.09% of the autoformalized statements before manual review, which reduces the cost of expert annotation.
  • Kimina-Prover scores best at 16.46% (pass@32) on FormalMATH-Full. BFS-Prover reaches 11.13% with best-first search under a 1×32×100 budget. Other evaluated provers include STP, Goedel-Prover, DeepSeek-V1.5 (SFT/RL) and InternLM-Prover.
  • Provers do relatively well on high-school algebra and applied mathematics but poorly on calculus and other areas. They often reduce multi-step arguments to a single tactic such as aesop or linarith.
  • Chain-of-thought prompting improves results, but adding human-written natural-language solutions lowers proof success.

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

🎓Chinese University of Hong KongHong Kong · China176 works · 17,536 citations🎓University of California, Los AngelesLos Angeles · United States110 works · 58,035 citations🎓Westlake UniversityHangzhou · China60 works · 8,829 citations🔬Max Planck SocietyMunich · Germany19 works · 42,336 citations🔬Max Planck Institute for Intelligent SystemsStuttgart · Germany11 works · 1,062 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 Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang and Weiyang Liu. 2025. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models. arXiv:2505.02735.

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

@misc{yu2025formalmath,
  title = {{FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models}},
  author = {Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang and Weiyang Liu},
  year = {2025},
  doi = {10.48550/arxiv.2505.02735},
  eprint = {2505.02735},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2505.02735}
}

References

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

  1. Team AlphaProof and Team AlphaGeometry. Ai achieves silver-medal standard solving international 178 mathematical olympiad problems. DeepMind blog, 2024. 4 find
  2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023. 1, 3, 4
  3. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. 1 find
  4. Jinze Bai, Shuai Bai, Yunfei Chu, Zeyu Cui, Kai Dang, Xiaodong Deng, Yang Fan, Wenbin Ge, Yu Han, Fei Huang, et al. Qwen technical report. arXiv preprint arXiv:2309.16609, 2023. 5
  5. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021. 3
  6. Rémi Coulom. Efficient selectivity and backup operators in Monte-Carlo tree search. In International conference on computers and games, pages 72–83. Springer, 2006. 4 find
  7. Konstantin Chernyshev, Vitaliy Polshkov, Ekaterina Artemova, Alex Myasnikov, Vlad Stepanov, Alexei Miasnikov, and Sergei Tilga. U-math: A university-level benchmark for evaluating mathematical skills in llms. arXiv preprint arXiv:2412.03205, 2024. 4, 21
  8. B.P. Demidovich. Problems in Mathematical Analysis. Edited by B. Demidovich. Translated From the Russian by G. Yankovsky. Russian Monographs and Texts on Advanced Mathematics and Physics. Mir Publishers, 1964. 4 find
  9. Kefan Dong and Tengyu Ma. Beyond limited data: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025. 4, 6, 7
  10. Jingxuan Fan, Sarah Martinson, Erik Y Wang, Kaylie Hausknecht, Jonah Brenner, Danxian Liu, Nianli Peng, Corey Wang, and Michael P Brenner. Hardmath: A benchmark dataset for challenging problems in applied mathematics. arXiv preprint arXiv:2410.09988, 2024. 4, 21 — [arXiv:2410.09988](https://arxiv.org/abs/2410.09988) find
  11. Bofei Gao, Feifan Song, Zhe Yang, Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, et al. Omni-math: A universal olympiad level mathematic benchmark for large language models. arXiv preprint arXiv:2410.07985, 2024. 4, 21
  12. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025. 4
  13. Masayoshi Hata. Problems and solutions in real analysis, volume 14. World Scientific Publishing Company, 2016. 21 find
  14. Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al. Openai o1 system card. arXiv preprint arXiv:2412.16720, 2024. 5
  15. Levente Kocsis and Csaba Szepesvári. Bandit based Monte-Carlo planning. In European conference on machine learning, pages 282–293. Springer, 2006. 4 find
  16. Leanprover Community. A read-eval-print-loop for Lean 4. leanprover-community/repl, 2023. 2, 4, 8 find
  17. K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, 2010. 1 find
  18. Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023. 2, 12 find
  19. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023. 3, 4
  20. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024. 4 https://github.com/ ↗
  21. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025. 3, 4, 6, 7
  22. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406.01940, 2024. 3
  23. Mathlib Community. The Lean mathematical library. In ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, 2020. 1, 4, 8
  24. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021. 2, 3
  25. Niklas Muennighoff, Zitong Yang, Weijia Shi, Xiang Lisa Li, Li Fei-Fei, Hannaneh Hajishirzi, Luke Zettlemoyer, Percy Liang, Emmanuel Candès, and Tatsunori Hashimoto. s1: Simple test-time scaling. arXiv preprint arXiv:2501.19393, 2025. 9, 10
  26. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. 3 find
  27. OpenAI. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023. 3, 5
  28. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311–318, 2002. 3
  29. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. 1, 4
  30. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025. 4
  31. Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 31(2):349–354, 2022. 1 find
  32. Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. Scaling llm test-time compute optimally can be more effective than scaling model parameters. arXiv preprint arXiv:2408.03314, 2024. 9
  33. Brian Smith. Constructive mathematics. The Bulletin of Symbolic Logic, 1(2):118–141, 1995. 13 find
  34. Terence Tao. The polynomial freiman-ruzsa conjecture. https://github.com/teorth/pf, 2023. 1 ↗
  35. Kimi Team, Angang Du, Bofei Gao, Bowei Xing, Changjiu Jiang, Cheng Chen, Cheng Li, Chenjun Xiao, Chenzhuang Du, Chonghua Liao, et al. Kimi k1. 5: Scaling reinforcement learning with llms. arXiv preprint arXiv:2501.12599, 2025. 4
  36. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. arXiv preprint arXiv:2407.11214, 2024. 3, 4
  37. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024. 4, 6, 7
  38. Wikipedia contributors. De morgan’s laws — Wikipedia, the free encyclopedia, [Year of specific version, e.g., 2025]. [Online; accessed 5-May-2025; version of (Date of specific version, e.g., 1-May-2025)]. 6 find
  39. Wikipedia contributors. Law of excluded middle — Wikipedia, the free encyclopedia, [Year of specific version, e.g., 2025]. [Online; accessed 5-May-2025; version of (Date of specific version, e.g., 28-April-2025)]. 6 find
  40. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In NeurIPS, 2022. 3, 5
  41. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025. 2, 3, 4, 6, 7
  42. Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203.11171, 2022. 2, 5
  43. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H Chi, Quoc V Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In NeurIPS, 2022. 2, 3
  44. Tim Z Xiao, Robert Bamler, Bernhard Schölkopf, and Weiyang Liu. Verbalized machine learning: Revisiting machine learning with language models. arXiv preprint arXiv:2406.04344, 2024. 9 — [arXiv:2406.04344](https://arxiv.org/abs/2406.04344) find
  45. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024. 1, 3, 4, 5, 6, 7
  46. Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025. 1, 2, 4, 6, 7
  47. Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. In ICLR, 2024. 3
  48. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024. 1, 3
  49. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In NeurIPS, 2023. 4
  50. Zhouliang Yu, Yuhuan Yuan, Tim Z Xiao, Fuxiang Frank Xia, Jie Fu, Ge Zhang, Ge Lin, and Weiyang Liu. Generating symbolic world models via test-time scaling of large language models. arXiv preprint arXiv:2502.04728, 2025. 9 — [arXiv:2502.04728](https://arxiv.org/abs/2502.04728) find
  51. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021. 1, 3, 4
  52. Yifan Zhang, Yifan Luo, and Yizhou Chen. Bluemo: A comprehensive collection of challenging mathematical olympiad problems from the little blue book series., 2024. 4, 21 find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/yu-2025-formalmath-benchmarking-formal-mathematical-reasoning/