---
title: "Goedel-Prover — paper by Lin et al. (2025) — summary and ideas"
description: "Training language models to write machine-checkable proofs is hard because very little… 7.6 points. 50 references, cited by 82 papers here."
authors: ["Yong Lin", "Shange Tang", "Bohan Lyu", "Jiayun Wu", "Hongzhou Lin", "Kaiyu Yang", "Jia Li", "Mengzhou Xia", "Danqi Chen", "Sanjeev Arora", "Chi Jin"]
year: 2025
venue: "arXiv:2502.07640"
source: "https://arxiv.org/abs/2502.07640"
doi: "10.48550/arxiv.2502.07640"
arxiv: "2502.07640"
licence: "CC0 1.0 (arXiv)"
licence_url: "https://creativecommons.org/publicdomain/zero/1.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/2/) / Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

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

**Authors:** [Yong Lin](https://md.research.elamur.ai/free/en/authors/yong-lin/), [Shange Tang](https://md.research.elamur.ai/free/en/authors/shange-tang/), [Bohan Lyu](https://md.research.elamur.ai/free/en/authors/bohan-lyu/), [Jiayun Wu](https://md.research.elamur.ai/free/en/authors/jiayun-wu/), Hongzhou Lin, [Kaiyu Yang](https://md.research.elamur.ai/free/en/authors/kaiyu-yang/), [Jia Li](https://md.research.elamur.ai/free/en/authors/jia-li/), [Mengzhou Xia](https://md.research.elamur.ai/free/en/authors/mengzhou-xia/), [Danqi Chen](https://md.research.elamur.ai/free/en/authors/danqi-chen/), [Sanjeev Arora](https://md.research.elamur.ai/free/en/authors/sanjeev-arora/) and Chi Jin · **Year:** 2025 · **Venue:** arXiv:2502.07640 · **Licence:** [CC0 1.0 (arXiv)](https://creativecommons.org/publicdomain/zero/1.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2502.07640) · [PDF](https://arxiv.org/pdf/2502.07640v3) · [DOI 10.48550/arxiv.2502.07640](https://doi.org/10.48550/arxiv.2502.07640) · [arXiv 2502.07640](https://arxiv.org/abs/2502.07640) · [OpenAlex](https://openalex.org/W4407425807)

**Citations:** 2 citations (OpenAlex, 2026-10-14) · [82](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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 University](https://md.research.elamur.ai/free/en/universities/tsinghua-university/) — University, Beijing, China · 415 works · 94,028 citations
- [Princeton University](https://md.research.elamur.ai/free/en/universities/princeton-university/) — University, Princeton, United States · 113 works · 48,612 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/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.

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

- [← previous PaperBench: Evaluating AI's Ability to Replicate AI Research](https://md.research.elamur.ai/free/en/papers/starace-2025-paperbench-evaluating-ai-s/)
- [next → Light-R1: Curriculum SFT, DPO and RL for Long COT from Scratch and Beyond](https://md.research.elamur.ai/free/en/papers/wen-2025-light-r1-curriculum-sft-dpo/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/2/)

## 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/](https://artofproblemsolving.com/wiki/). Accessed: 2025-01-24. [↗](https://artofproblemsolving.com/wiki/)
2. Thomas Anthony, Zheng Tian, and David Barber. [Thinking fast and slow with deep learning and tree search](https://md.research.elamur.ai/free/en/papers/anthony-2017-thinking-fast-slow-deep-learning/). In Neural Information Processing Systems (NeurIPS), 2017.
3. Anthropic. Claude 3.5 sonnet, 2024. claude-3-5-sonnet. [find](https://scholar.google.com/scholar?q=Anthropic%2E+Claude+3%2E5+sonnet%2C+2024%2E+claude%2D3%2D5%2Dsonnet%2E)
4. URL — [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/) [https://www.anthropic.com/news/Zhangir](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. [↗](https://www.anthropic.com/news/Zhangir)
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](https://scholar.google.com/scholar?q=Haniel+Barbosa%2C+Clark+Barrett%2C+Martin+Brain%2C+Gereon+Kremer%2C+Hanna+Lachnitt%2C+Makai+Mann%2C+Abdalrhman+Mohamed%2C+Mudathir+Mohamed%2C+Aina+Niemetz%2C+Andres+No%CC%88tzli%2C+et+al%2E+cvc5%3A+A+versatile+and+industrial%2Dstre)
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](https://scholar.google.com/scholar?q=Bruno+Barras%2C+Samuel+Boutin%2C+Cristina+Cornes%2C+Judicae%CC%88l+Courant%2C+Jean%2DChristophe+Filliatre%2C+Eduardo+Gimenez%2C+Hugo+Herbelin%2C+Gerard+Huet%2C+Cesar+Munoz%2C+Chetan+Murthy%2C+et+al%2E+The+Coq+proof+assistant+refe)
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](https://scholar.google.com/scholar?q=Lichang+Chen%2C+Chen+Zhu%2C+Davit+Soselia%2C+Jiuhai+Chen%2C+Tianyi+Zhou%2C+Tom+Goldstein%2C+Heng+Huang%2C+Mohammad+Shoeybi%2C+and+Bryan+Catanzaro%2E+Odin%3A+Disentangled+reward+mitigates+hacking+in+rlhf%2E+arXiv+preprint+a)
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](https://md.research.elamur.ai/free/en/papers/cobbe-2021-training-verifiers-solve-math-word/). 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](https://scholar.google.com/scholar?q=Leonardo+De+Moura+and+Nikolaj+Bj%C3%B8rner%2E+Z3%3A+An+efficient+smt+solver%2E+In+International+conference+on+Tools+and+Algorithms+for+the+Construction+and+Analysis+of+Systems%2C+pp%2E+337%E2%80%93340%2E+Springer%2C+2008%2E)
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](https://scholar.google.com/scholar?q=Leonardo+De+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+Van+Doorn%2C+and+Jakob+von+Raumer%2E+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction%2DCADE%2D25%3A+25th+International+Conference+on+Au)
11. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. [Baldur: Whole-proof generation and repair with large language models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/). 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](https://scholar.google.com/scholar?q=Fabian+Gloeckle%2C+Jannis+Limperg%2C+Gabriel+Synnaeve%2C+and+Amaury+Hayat%2E+Abel%3A+Sample+efficient+online+reinforcement+learning+for+neural+theorem+proving%2E+In+The+4th+Workshop+on+Mathematical+Reasoning+and+)
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](https://md.research.elamur.ai/free/en/papers/deepseek-ai-2025-deepseek-r1-incentivizing-reasoning-capability/). 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](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/). 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](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/)
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](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). 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](https://scholar.google.com/scholar?q=Cezary+Kaliszyk%2C+Josef+Urban%2C+Henryk+Michalewski%2C+and+Miroslav+Ols%CC%8Ca%CC%81k%2E+Reinforcement+learning+of+theorem+proving%2E+In+Neural+Information+Processing+Systems+%28NeurIPS%29%2C+volume+31%2C+2018%2E)
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](https://scholar.google.com/scholar?q=Laura+Kova%CC%81cs+and+Andrei+Voronkov%2E+First%2Dorder+theorem+proving+and+vampire%2E+In+International+Conference+on+Computer+Aided+Verification%2C+pp%2E+1%E2%80%9335%2E+Springer%2C+2013%2E)
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](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). 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](https://scholar.google.com/scholar?q=Jia+Li%2C+Edward+Beeching%2C+Lewis+Tunstall%2C+Ben+Lipkin%2C+Roman+Soletskyi%2C+Shengyi+Huang%2C+Kashif+Rasul%2C+Longhui+Yu%2C+Albert+Q+Jiang%2C+Ziju+Shen%2C+et+al%2E+Numinamath%3A+The+largest+public+dataset+in+ai4maths+with)
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](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/).
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](https://scholar.google.com/scholar?q=Haohan+Lin%2C+Zhiqing+Sun%2C+Yiming+Yang%2C+and+Sean+Welleck%2E+Lean%2DSTaR%3A+Learning+to+interleave+thinking+and+proving%2E+arXiv+preprint+arXiv%3A2407%2E10040%2C+2024%2E)
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](https://scholar.google.com/scholar?q=Aixin+Liu%2C+Bei+Feng%2C+Bing+Xue%2C+Bingxuan+Wang%2C+Bochao+Wu%2C+Chengda+Lu%2C+Chenggang+Zhao%2C+Chengqi+Deng%2C+Chenyu+Zhang%2C+Chong+Ruan%2C+et+al%2E+Deepseek%2Dv3+technical+report%2E+arXiv+preprint+arXiv%3A2412%2E19437%2C+2024%2E)
24. MAA. American invitational mathematics examination - aime. In American Invitational Mathematics Examination - AIME 2024, February 2024. URL: [https://maa.org/](https://maa.org/) math-competitions/american-invitational-mathematics-examination-aime. mathlib4. mathlib4: The math library of lean 4, 2023. leanprover-communi… [↗](https://maa.org/)
25. URL [https://github.com/Aaron](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. [↗](https://github.com/Aaron)
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](https://scholar.google.com/scholar?q=Maciej+Miku%C5%82a%2C+Szymon+Tworkowski%2C+Szymon+Antoniak%2C+Bartosz+Piotrowski%2C+Albert+Q+Jiang%2C+Jin+Peng+Zhou%2C+Christian+Szegedy%2C+%C5%81ukasz+Kucin%CC%81ski%2C+Piotr+Mi%C5%82os%CC%81%2C+and+Yuhuai+Wu%2E+Magnushammer%3A+A+transformer%2Dbase)
27. Arindam Mitra, Hamed Khanpour, Corby Rosset, and Ahmed Awadallah. [Orca-math: Unlocking the potential of slms in grade school math](https://md.research.elamur.ai/free/en/papers/mitra-2024-orca-math-unlocking-potential-slms/). 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)](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
29. Lawrence C Paulson. Isabelle: A generic theorem prover. 1994. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulson%2E+Isabelle%3A+A+generic+theorem+prover%2E+1994%2E)
30. Stanislas Polu and Ilya Sutskever. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). 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](https://md.research.elamur.ai/free/en/papers/polu-2022-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](https://md.research.elamur.ai/free/en/papers/polu-2022-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](https://md.research.elamur.ai/free/en/papers/rafailov-2023-direct-preference-optimization-language-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](https://scholar.google.com/scholar?q=Alan+JA+Robinson+and+Andrei+Voronkov%2E+Handbook+of+automated+reasoning%2C+volume+1%2E+2001%2E)
35. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In International Conference on Automated Deduction (CADE), 2019. [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2C+Simon+Cruanes%2C+and+Petar+Vukmirovic%CC%81%2E+Faster%2C+higher%2C+stronger%3A+E+2%2E3%2E+In+International+Conference+on+Automated+Deduction+%28CADE%29%2C+2019%2E)
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](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/). 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](https://scholar.google.com/scholar?q=Amitayush+Thakur%2C+Yeming+Wen%2C+and+Swarat+Chaudhuri%2E+A+language%2Dagent+approach+to+formal+theorem%2Dproving%2E+arXiv+preprint+arXiv%3A2310%2E04353%2C+2023%2E)
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](https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/). 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](https://scholar.google.com/scholar?q=Lewis+Tunstall%2C+Leandro+Von+Werra%2C+and+Thomas+Wolf%2E+Natural+language+processing+with+transformers%2E+%E2%80%9D+O%E2%80%99Reilly+Media%2C+Inc%2E%E2%80%9D%2C+2022%2E)
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](https://scholar.google.com/scholar?q=Josef+Urban%2C+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2C+and+Petr+S%CC%8Cte%CC%8Cpa%CC%81nek%2E+MaLeCoP+machine+learning+connection+prover%2E+In+International+Conference+on+Automated+Reasoning+with+Analytic+Tableaux+and+Related+Methods%2C+2011%2E)
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](https://scholar.google.com/scholar?q=Ruida+Wang%2C+Jipeng+Zhang%2C+Yizhen+Jia%2C+Rui+Pan%2C+Shizhe+Diao%2C+Renjie+Pi%2C+and+Tong+Zhang%2E+Theoremllama%3A+Transforming+general%2Dpurpose+llms+into+lean4+experts%2E+arXiv+preprint+arXiv%3A2407%2E03203%2C+2024%2E)
42. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-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](https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/).
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](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/). 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](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/).
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](https://scholar.google.com/scholar?q=An+Yang%2C+Baosong+Yang%2C+Beichen+Zhang%2C+Binyuan+Hui%2C+Bo+Zheng%2C+Bowen+Yu%2C+Chengyuan+Li%2C+Dayiheng+Liu%2C+Fei+Huang%2C+Haoran+Wei%2C+et+al%2E+Qwen2%2E+5+technical+report%2E+arXiv+preprint+arXiv%3A2412%2E15115%2C+2024a%2E)
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](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). 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](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/). 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](https://md.research.elamur.ai/free/en/papers/ying-2024-internlm-math-open-math-large/). 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](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv preprint arXiv:2109.00110, 2021.

*Updated 2 November 2026*