Elamur Research⌕
☰
home / papers / 2025 / Autoformalization in the Era of Large Language Models: A Survey

Autoformalization in the Era of Large Language Models: A Survey

Paper · 2025 · Ke Weng, Lun Du, Sirui Li et al.

Summary

This survey examines how large language models are changing autoformalization, the task of converting informal mathematical statements and proofs into machine-checkable code for proof assistants such as Lean, Coq and Isabelle. Formalizing mathematics by hand takes a great deal of time even for experts, so automating the translation could greatly speed up verified mathematics. The authors organize the field along three lines. First, they follow the full pipeline: data preprocessing, model design (rule-based approaches versus neural and LLM-based ones), post-processing and evaluation. Second, they group mathematical problems by domain, difficulty and level of abstraction. Third, they discuss autoformalization as a way to verify LLM outputs beyond pure mathematics, for example in code generation and system specification. The survey also catalogs open-source provers and datasets. Its main contribution is this structured map of the field. The authors identify the shortage of aligned informal–formal data as the key bottleneck and argue for hybrid systems that combine LLMs with symbolic tools.

Key points

  • Motivating milestones: AlphaProof reached silver-medal level on IMO problems, and GPT-o3 reportedly solved 25.2% of FrontierMath, compared with about 2% for earlier models.
  • Catalogued open models include DeepSeek-Prover-V1/V2, Kimina-Prover, Goedel-Prover, LLEMMA, Lean Workbook, LeanDojo, Herald, BFS-Prover and InternLM2.5-StepProver. MiniF2F is the most common evaluation benchmark.
  • Benchmark sizes:
    • MiniF2F: 488 problems
    • ProofNet: 374 problems
    • PutnamBench: 657 problems
    • ProverBench: 325 problems
    • CombiBench: 100 problems
    • Formal Math: 5,560 statements
    • Herald: about 580k statements plus 44k NL–FL proofs
    • DeepTheorem: 121K IMO-level theorems
  • Open challenges:
    • Parallel corpora remain small; LeanWorkbook is only about 4.8MB.
    • Full retraining for each new domain is too costly.
    • Interactive, modular pipelines are still needed.

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

🎓Northeastern UniversityBoston · United States70 works · 7,342 citations🏢Ant GroupHangzhou · China53 works · 1,274 citations🎓Aalborg UniversityAalborg · Denmark14 works · 754 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 4,145 worksReasoning · 1,948 works

Cite

Cite as Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu and Tiancheng Zhang. 2025. Autoformalization in the Era of Large Language Models: A Survey. arXiv:2505.23486.

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

@misc{weng2025autoformalization,
  title = {{Autoformalization in the Era of Large Language Models: A Survey}},
  author = {Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu and Tiancheng Zhang},
  year = {2025},
  doi = {10.48550/arxiv.2505.23486},
  eprint = {2505.23486},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2505.23486}
}

References

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

  1. Pranjal Aggarwal, Bryan Parno, and Sean Welleck. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176, 2024.
  2. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models, 2022.
  3. Team AlphaProof and Team AlphaGeometry. Ai achieves silver-medal standard solving international 178 mathematical olympiad problems. DeepMind blog, 179:45, 2024. find
  4. Antropic. model yet. 2024. Claude 3 haiku: Our fastest find
  5. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics, 2023.
  6. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics, 2024.
  7. Maria-Florina Balcan, Avrim Blum, Zhiyuan Li, and Dravyansh Sharma. On learning verifiers for chain-of-thought reasoning, 2025. find
  8. Lasse Blaauwbroek, David M Cerna, Thibault Gauthier, Jan Jakubŭv, Cezary Kaliszyk, Martin Suda, and Josef Urban. Learning guided automated reasoning: a brief survey. Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday, pages 54–83,… find
  9. Willy Chan, Michael Souliman, Jakob Nordhagen, Brando Miranda, Elyas Obbad, and Kai Fronsdal Sanmi Koyejo. Lean-ing on quality: How high-quality data beats diverse multilingual data in autoformalization, 2025. find
  10. Garett Cunningham, Razvan C. Bunescu, and David Juedes. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. CoRR, abs/2301.02195, 2023.
  11. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378–388, Cham, 2015. Springer International Publishing. find
  12. Peng Di, Jianguo Li, Hang Yu, Wei Jiang, Wenting Cai, Yang Cao, Chaoyu Chen, Dajun Chen, Hongwei Chen, Liang Chen, et al. Codefuse-13b: A pre-trained multi-lingual code large language model. In Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice… find
  13. Yann Fleureau, Edward Beeching Jia Li, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, and Kashif Rasul. How numinamath won the 1st aimo progress prize. 2024. find
  14. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset, 2025.
  15. Georges Gonthier. Formal proof—the four-color theorem. 2008. find
  16. Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef… — A formal proof of the Kepler conjecture
  17. Ahmed Abdeen Hamed, Alessandro Crimi, Magdalena M Misiak, and Byung Suk Lee. From knowledge generation to knowledge verification: Examining the biomedical generative capabilities of chatgpt. arXiv preprint arXiv:2502.14714, 2025. — [arXiv:2502.14714](https://arxiv.org/abs/2502.14714) find
  18. Lucas Torroba Hennigen, Shannon Shen, Aniruddha Nrusimha, Bernhard Gapp, David Sontag, and Yoon Kim. Towards verifiable text generation with symbolic references. arXiv preprint arXiv:2311.09188, 2023. find
  19. Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rapport Technique, 178:113, 1997. find
  20. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization, 2023.
  21. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, ICLR 2023…
  22. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformalization. In A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang, editors, Advances in Neural Information Processing Systems, volume 37, pages 83600–83626. Curran Associates, Inc.,… find
  23. Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948, 2023. — [arXiv:2311.07948](https://arxiv.org/abs/2311.07948) find
  24. Herb Krasner. The cost of poor software quality in the us: A 2022 report. Proc.Consortium Inf. Softw. QualityTM (CISQTM), 2022. find
  25. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency, 2024.
  26. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024.
  27. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving, 2025.
  28. Zeqin Liao, Yuhong Nan, Zixu Gao, Hen-glong Liang, Sicheng Hao, Peifan Reng, and Zibin Zheng. Augmenting smart contract decompiler output through fine-grained dependency analysis and llm-facilitated semantic recovery. arXiv preprint arXiv:2501.08670, 2025. — [arXiv:2501.08670](https://arxiv.org/abs/2501.08670) find
  29. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: A frontier model for open-source automated theorem proving, 2025.
  30. Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, Zhengfeng Yang, Jujian Zhang, Lihong Zhi, Jia Li, and Zhengying Liu. Combibench: Benchmarking llm capability for combinatorial mathematics, 2025.
  31. Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: Towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025. find
  32. Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data, 2025.
  33. Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. Formalalign: Automated alignment evaluation for autoformalization, 2024.
  34. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. Process-driven autoformalization in lean 4, 2024.
  35. Ferrari Pier Luigi. Abstraction in mathematics. 2003. find
  36. Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. Specgen: Automated generation of formal program specifications via large language models. corr abs/2401.08807 (2024), 2024. — [arXiv:2401.08807](https://arxiv.org/abs/2401.08807) find
  37. Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar. Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008, Proceedings, volume 5170. Springer Science & Business Media, 2008. find
  38. 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.
  39. Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing euclidean geometry, 2024.
  40. OpenAI. Gpt-4 technical report, 2024.
  41. Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization, 2024.
  42. Shashank Pathak. Gflean: An autoformalisation framework for lean via gf, 2024.
  43. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. find
  44. Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving autoformalization using type checking, 2025. find
  45. Mohammad Raza and Natasa Milic-Frayling. Instantiation-based formalization of logical reasoning tasks using language models and logical solvers, 2025. find
  46. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcemen… — DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
  47. Hyun Ryu, Gyeongman Kim, Hyemin S Lee, and Eunho Yang. Divide and translate: Compositional first-order logic translation and verification for complex logical reasoning. arXiv preprint arXiv:2410.08047, 2024. — [arXiv:2410.08047](https://arxiv.org/abs/2410.08047) find
  48. Vinu Sankar Sadasivan, Aounon Kumar, Sriram Balasubramanian, Wenxiao Wang, and Soheil Feizi. Can ai-generated text be reliably detected? arXiv preprint arXiv:2303.11156, 2023.
  49. Ensheng Shi, Fengji Zhang, Yanlin Wang, Bei Chen, Lun Du, Hongyu Zhang, Shi Han, Dongmei Zhang, and Hongbin Sun. Sotana: The open-source software development assistant. arXiv preprint arXiv:2308.13416, 2023. find
  50. Yuda Song, Hanlin Zhang, Carson Eisenach, Sham Kakade, Dean Foster, and Udaya Ghai. Mind the gap: Examining the self-improvement capabilities of large language models, 2025. find
  51. Mauricio Soroco, Jialin Song, Mengzhou Xia, Kye Emond, Weiran Sun, and Wuyang Chen. Pde-controller: Llms for autoformalization and reasoning of pdes, 2025. find
  52. Matthieu Sozeau, Guillaume Melquiond, and Pierre Roux. The coq proof assistant. find
  53. David Tall. Advanced mathematical thinking. 1991. find
  54. Terence Tao. Machine-assisted proof. Notices of the American Mathematical Society, to appear, 2024. find
  55. Gemini Team, Rohan Anil, Sebastian Borgeaud, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M. Dai, Anja Hauth, and Katie Millican. Gemini: A family of highly capable multimodal models, 2024.
  56. Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Tim-othée Lacroix, Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, Aurelien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. Llama: Open and efficient foundation language models, 2023.
  57. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, L… — Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
  58. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022.
  59. 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, 2024. find
  60. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean-github: Compiling github lean repositories for a versatile lean prover, 2024.
  61. Huajian Xin, Daya Guo, Zhihong Shao, Z.Z. Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Advancing theorem proving in LLMs through large-scale synthetic data. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. find
  62. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-… — DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  63. Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, and Wenda Li. Ape-bench i: Towards file-level automated proof engineering of formal math libraries, 2025. find
  64. 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, 2025.
  65. Beibei Xiong, Hangyu Lv, Haojia Shan, Jianlin Wang, Zhengfeng Yang, and Lihong Zhi. A combinatorial identities benchmark for theorem proving via automated theorem generation, 2025. find
  66. Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin, and Zhenguo Li. Mathesis: Towards form… — Mathesis: Towards Formal Theorem Proving from Natural Languages
  67. 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.
  68. 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. Formalmath: Benchmarking formal mathematical reasoning of large language models, 2025.
  69. Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover: Posttraining scaling in formal reasoning, 2025.
  70. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics, 2022.
  71. Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving, 2024.
  72. Da Zheng, Lun Du, Junwei Su, Yuchen Tian, Yuqi Zhu, Jintian Zhang, Lanning Wei, Ningyu Zhang, and Huajun Chen. Knowledge augmented complex problem solving with large language models: A survey. arXiv preprint arXiv:2505.03418, 2025. — [arXiv:2505.03418](https://arxiv.org/abs/2505.03418)
  73. Kuo Zhou and Lu Zhang. Step-wise formal verification for llm-based mathematical problem solving, 2025. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/weng-2025-autoformalization-era-large-language-models/