Elamur Research⌕
☰
home / papers / 2025 / Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

Paper · 2025 · Yong Lin, Shange Tang, Bohan Lyu et al.

Summary

Training language models to write machine-checkable proofs is hard because very little mathematics exists in formal form. The authors address this by translating informal competition problems from the Numina collection into Lean 4 statements. They use two separately trained formalizers: one learned from Lean Workbook pairs, the other from pairs labelled by Claude-sonnet-3.5. LLM-based checks then confirm that each translation keeps the original meaning. The result is Goedel-Pset-v1, with 1.64M statements. Next, they run eight rounds of expert iteration. In each round, a prover fine-tuned from DeepSeek-Prover-V1.5-Base writes complete proofs without interacting with the compiler, Lean checks them, and the verified proofs become training data for the next round. The final Goedel-Prover-SFT is trained only with supervised fine-tuning. It reaches 57.6% Pass@32 on miniF2F, 7.6 points above DeepSeek-Prover-V1.5-RL, and ranks first on PutnamBench. All code, models and datasets are openly released. This gives a reproducible baseline for formal reasoning and shows how abundant informal text can be used to build scarce formal training data.

Key points

  • Resources: Goedel-Pset-v1 (1.64M Lean 4 statements), Goedel-Pset-v1-solved (proofs for over 800K of them), two Goedel-Formalizer-32B models, and new proofs for 29.7K Lean Workbook problems. Previous provers had solved about 15.7K.
  • On PutnamBench, Goedel-Prover-SFT solves 7 problems at Pass@512 and takes first place on the leaderboard. It beats DeepSeek-Prover-V1.5-RL on miniF2F at every sampling budget the authors tested.
  • Ablations: statements from both formalizers together give better results than either one alone (miniF2F 57.6% vs. 56.5% and 56.2%). Adding Mathlib4 to training helps on ProofNet but lowers miniF2F scores, which points to a distribution shift between concept-heavy and Olympiad-style data.
  • Adding DPO or GRPO on top of SFT raises miniF2F Pass@32 to about 60%. However, the gains mostly disappear at Pass@3200. These models also produce longer proofs and overuse the try tactic, a form of reward hacking.
  • A sketch-based alternative was tried: o1-preview writes a proof outline and DeepSeek-Prover-V1.5-RL proves the subgoals. It solved only 76 of 244 miniF2F validation problems, compared with 158 for the base prover alone.

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

🎓Tsinghua UniversityBeijing · China415 works · 94,028 citations🎓Princeton UniversityPrinceton · United States113 works · 48,612 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora and Chi Jin. 2025. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. arXiv:2502.07640.

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

@misc{lin2025goedel,
  title = {{Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving}},
  author = {Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora and Chi Jin},
  year = {2025},
  doi = {10.48550/arxiv.2502.07640},
  eprint = {2502.07640},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2502.07640}
}

References

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

  1. Art of problem solving wiki. https://artofproblemsolving.com/wiki/. Accessed: 2025-01-24. ↗
  2. Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. In Neural Information Processing Systems (NeurIPS), 2017.
  3. Anthropic. Claude 3.5 sonnet, 2024. claude-3-5-sonnet. find
  4. URL — ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics https://www.anthropic.com/news/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. ↗
  5. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength smt solver. In International Conference on Tools and Algorithms for the Construction and Analys… find
  6. 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. find
  7. Lichang Chen, Chen Zhu, Davit Soselia, Jiuhai Chen, Tianyi Zhou, Tom Goldstein, Heng Huang, Mohammad Shoeybi, and Bryan Catanzaro. Odin: Disentangled reward mitigates hacking in rlhf. arXiv preprint arXiv:2402.07319, 2024. find
  8. 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.
  9. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. Springer, 2008. find
  10. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378–388. find
  11. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023.
  12. Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. Google DeepMind. AI achieves silver-medal standard solving international mathemati… find
  13. 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.
  14. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021.
  15. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016. — DeepMath - Deep Sequence Models for Premise Selection
  16. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.
  17. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Neural Information Processing Systems (NeurIPS), volume 31, 2018. find
  18. Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In International Conference on Computer Aided Verification, pp. 1–35. Springer, 2013. find
  19. Guillaume Lample, Timothee Lacroix, Marie anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information…
  20. Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13, 2024a. find
  21. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hun-yuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024b.
  22. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-STaR: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024. find
  23. Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437, 2024. find
  24. MAA. American invitational mathematics examination - aime. In American Invitational Mathematics Examination - AIME 2024, February 2024. URL: https://maa.org/ math-competitions/american-invitational-mathematics-examination-aime. mathlib4. mathlib4: The math library of lean 4, 2023. leanprover-communi… ↗
  25. URL https://github.com/Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ondřej Čertı́k, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. Sympy: symbolic computing in python. PeerJ Computer Science, 3:e103, 2017. ↗
  26. Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. In International Conference on Learning Representations (ICLR), 202… find
  27. Arindam Mitra, Hamed Khanpour, Corby Rosset, and Ahmed Awadallah. Orca-math: Unlocking the potential of slms in grade school math. arXiv preprint arXiv:2402.14830, 2024.
  28. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction (CADE), 2021. — The Lean 4 Theorem Prover and Programming Language (System Description)
  29. Lawrence C Paulson. Isabelle: A generic theorem prover. 1994. find
  30. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  31. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  32. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In International Conference on Learning Representations (ICLR), 2023.
  33. Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. Direct preference optimization: Your language model is secretly a reward model. Advances in Neural Information Processing Systems, 36:53728–53741, 2023.
  34. Alan JA Robinson and Andrei Voronkov. Handbook of automated reasoning, volume 1. 2001. find
  35. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In International Conference on Automated Deduction (CADE), 2019. find
  36. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
  37. Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach to formal theorem-proving. arXiv preprint arXiv:2310.04353, 2023. find
  38. 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.
  39. Lewis Tunstall, Leandro Von Werra, and Thomas Wolf. Natural language processing with transformers. ” O’Reilly Media, Inc.”, 2022. find
  40. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek. MaLeCoP machine learning connection prover. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2011. find
  41. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024. find
  42. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. UR…
  43. 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.
  44. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  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, 2024b.
  46. An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, et al. Qwen2. 5 technical report. arXiv preprint arXiv:2412.15115, 2024a. find
  47. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024b.
  48. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024a.
  49. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. Internlm-math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024b.
  50. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/