---
title: "TheoremLlama — paper by Wang et al. (2024)"
description: "The authors build an end-to-end pipeline in three stages: Data. 41 references, cited by 37 papers here."
authors: ["Ruida Wang", "Jipeng Zhang", "Yizhen Jia", "Rui Pan", "Shizhe Diao", "Renjie Pi", "Tong Zhang"]
year: 2024
venue: "arXiv:2407.03203"
source: "https://arxiv.org/abs/2407.03203"
doi: "10.48550/arxiv.2407.03203"
arxiv: "2407.03203"
licence: "CC BY 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/wang-2024-theoremllama-transforming-general-purpose-llms/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wang-2024-theoremllama-transforming-general-purpose-llms/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/8/) / TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

# TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

**Authors:** [Ruida Wang](https://md.research.elamur.ai/free/en/authors/ruida-wang/), [Jipeng Zhang](https://md.research.elamur.ai/free/en/authors/jipeng-zhang/), [Yizhen Jia](https://md.research.elamur.ai/free/en/authors/yizhen-jia/), [Rui Pan](https://md.research.elamur.ai/free/en/authors/rui-pan/), [Shizhe Diao](https://md.research.elamur.ai/free/en/authors/shizhe-diao/), [Renjie Pi](https://md.research.elamur.ai/free/en/authors/renjie-pi/) and [Tong Zhang](https://md.research.elamur.ai/free/en/authors/tong-zhang/) · **Year:** 2024 · **Venue:** [arXiv:2407.03203](https://md.research.elamur.ai/free/en/venues/emnlp/) ([EMNLP 2024](https://md.research.elamur.ai/free/en/venues/emnlp/2024/)) · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 14 citations (OpenAlex, 2026-10-14) · [37](https://md.research.elamur.ai/free/en/papers/wang-2024-theoremllama-transforming-general-purpose-llms/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
TheoremLlama tackles a core obstacle in automated formal proving. General-purpose LLMs write poor Lean4 proofs because there is almost no paired natural-language/formal (NL-FL) training data, and their pretraining mixes in outdated Lean3 code.

The authors build an end-to-end pipeline in three stages:
- **Data.** They take roughly 100k human-written theorems from Mathlib4 via LeanDojo. Gemini-1.5 writes informal statements and proofs for them, guided by examples retrieved with a fine-tuned ByT5 encoder. The informal reasoning is then inserted into the Lean4 code as comments, a step the paper calls "NL-FL bootstrapping." The result is the Open Bootstrapped Theorems (OBT) dataset.
- **Training.** Llama3-8B-Instruct is fine-tuned on OBT using block training and an easy-to-hard curriculum.
- **Inference.** Proofs verified as correct in earlier rounds are reused as in-context examples for later attempts.

The model proves 36.48% of MiniF2F-Valid and 33.61% of MiniF2F-Test, clearly ahead of GPT-4. Training needs only modest hardware, and the data, code and checkpoints are released. This makes it a practical recipe for adapting LLMs to low-resource, specialized domains.

## Key points
- **OBT dataset:** contains 106,852 NL-FL aligned, bootstrapped Lean4 theorems. The authors say no earlier open Lean4 aligned dataset had more than 1k records.
- **Example retrieval:** ByT5-Tacgen's encoder was fine-tuned on NL-annotated MiniF2F so that matching NL and Lean4 statements receive similar embeddings.
- **Results against GPT-4:** TheoremLlama reaches 36.48% (Valid) and 33.61% (Test) cumulative accuracy. GPT-4 scores 22.95% and 25.41%, though the paper assigns these two figures to Valid/Test inconsistently. TheoremLlama also beats Gemini-1.5.
- **Compute:** fine-tuning takes about 32 hours on a single 8×A6000 machine, far less than tree-search provers such as Polu et al.'s, which used 2,000 A100 GPU hours.
- **Limitations:** the system still struggles with IMO-level problems and uses no RL or Lean feedback loop. A further risk is that NL-guided provers may quietly fix flawed informal proofs, which could let those errors pass as correct.

*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

- [University of Illinois Urbana-Champaign](https://md.research.elamur.ai/free/en/universities/university-of-illinois-urbana-champaign/) — University, Urbana, United States · 228 works · 74,590 citations
- [Hong Kong University of Science and Technology](https://md.research.elamur.ai/free/en/universities/hong-kong-university-of-science-and-technology/) — University, Hong Kong, China · 183 works · 27,600 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧠 Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/) · 4,145 works

## Cite

Cite as: Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi and Tong Zhang. 2024. TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts. arXiv:2407.03203.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{wang2024theoremllama,
  title = {{TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts}},
  author = {Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi and Tong Zhang},
  year = {2024},
  doi = {10.48550/arxiv.2407.03203},
  eprint = {2407.03203},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2407.03203}
}
```

- [← previous RLEF: Grounding Code LLMs in Execution Feedback with Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/gehring-2024-rlef-grounding-code-llms-execution/)
- [next → VariErr NLI: Separating Annotation Error from Human Label Variation](https://md.research.elamur.ai/free/en/papers/genzel-2024-varierr-nli-separating-annotation-error/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/8/)

## References

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

1. Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. [Gpt-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv preprint arXiv:2303.08774.
2. AI@Meta. 2024. Llama 3 model card. [find](https://scholar.google.com/scholar?q=AI%40Meta%2E+2024%2E+Llama+3+model+card%2E)
3. Ateret Anaby-Tavor, Boaz Carmeli, Esther Goldbraich, Amir Kantor, George Kour, Segev Shlomov, Naama Tepper, and Naama Zwerdling. 2020. Do not have enough data? deep learning to the rescue! In Proceedings of the AAAI conference on artificial intelligence, volume 34, pages 7383–7390. [find](https://scholar.google.com/scholar?q=Ateret+Anaby%2DTavor%2C+Boaz+Carmeli%2C+Esther+Goldbraich%2C+Amir+Kantor%2C+George+Kour%2C+Segev+Shlomov%2C+Naama+Tepper%2C+and+Naama+Zwerdling%2E+2020%2E+Do+not+have+enough+data%3F+deep+learning+to+the+rescue%21+In+Proceedi)
4. Jeremy Avigad, Kevin Buzzard, Robert Y Lewis, and Patrick Massot. 2020. Mathematics in lean. [find](https://scholar.google.com/scholar?q=Jeremy+Avigad%2C+Kevin+Buzzard%2C+Robert+Y+Lewis%2C+and+Patrick+Massot%2E+2020%2E+Mathematics+in+lean%2E)
5. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. 2023a. [Proofnet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433.
6. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2023b. [Llemma: An open language model for mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/). arXiv preprint arXiv:2310.10631.
7. Abhimanyu Bambhaniya, Ritik Raj, Geonhwa Jeong, Souvik Kundu, Sudarshan Srinivasan, Midhilesh Elavazhagan, Madhu Kumar, and Tushar Krishna. 2024. Demystifying platform requirements for diverse llm inference use cases. arXiv preprint arXiv:2406.01698. — [arXiv:2406.01698](https://arxiv.org/abs/2406.01698) [find](https://scholar.google.com/scholar?q=Abhimanyu+Bambhaniya%2C+Ritik+Raj%2C+Geonhwa+Jeong%2C+Souvik+Kundu%2C+Sudarshan+Srinivasan%2C+Midhilesh+Elavazhagan%2C+Madhu+Kumar%2C+and+Tushar+Krishna%2E+2024%2E+Demystifying+platform+requirements+for+diverse+llm+inf)
8. Ting Chen, Simon Kornblith, Kevin Swersky, Mohammad Norouzi, and Geoffrey E Hinton. 2020. Big self-supervised models are strong semi-supervised learners. Advances in neural information processing systems, 33:22243–22255. [find](https://scholar.google.com/scholar?q=Ting+Chen%2C+Simon+Kornblith%2C+Kevin+Swersky%2C+Mohammad+Norouzi%2C+and+Geoffrey+E+Hinton%2E+2020%2E+Big+self%2Dsupervised+models+are+strong+semi%2Dsupervised+learners%2E+Advances+in+neural+information+processing+syst)
9. Projet Coq. 1996. The coq proof assistant-reference manual. INRIA Rocquencourt and ENS Lyon, version, 5. [find](https://scholar.google.com/scholar?q=Projet+Coq%2E+1996%2E+The+coq+proof+assistant%2Dreference+manual%2E+INRIA+Rocquencourt+and+ENS+Lyon%2C+version%2C+5%2E)
10. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. 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, pages 378–388. Springer. [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+2015%2E+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction%2DCADE%2D25%3A+25th+International+Conference)
11. Jiahui Gao, Renjie Pi, Yong Lin, Hang Xu, Jiacheng Ye, Zhiyong Wu, Weizhong Zhang, Xiaodan Liang, Zhenguo Li, and Lingpeng Kong. 2022. Self-guided noise-free data generation for efficient zero-shot learning. arXiv preprint arXiv:2205.12679. — [arXiv:2205.12679](https://arxiv.org/abs/2205.12679) [find](https://scholar.google.com/scholar?q=Jiahui+Gao%2C+Renjie+Pi%2C+Yong+Lin%2C+Hang+Xu%2C+Jiacheng+Ye%2C+Zhiyong+Wu%2C+Weizhong+Zhang%2C+Xiaodan+Liang%2C+Zhenguo+Li%2C+and+Lingpeng+Kong%2E+2022%2E+Self%2Dguided+noise%2Dfree+data+generation+for+efficient+zero%2Dshot+le)
12. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. 2021. Tactictoe: learning to prove with tactics. Journal of Automated Reasoning, 65(2):257–286. [find](https://scholar.google.com/scholar?q=Thibault+Gauthier%2C+Cezary+Kaliszyk%2C+Josef+Urban%2C+Ramana+Kumar%2C+and+Michael+Norrish%2E+2021%2E+Tactictoe%3A+learning+to+prove+with+tactics%2E+Journal+of+Automated+Reasoning%2C+65%282%29%3A257%E2%80%93286%2E)
13. John Harrison. 2009. Hol light: An overview. In International Conference on Theorem Proving in Higher Order Logics, pages 60–66. Springer. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+2009%2E+Hol+light%3A+An+overview%2E+In+International+Conference+on+Theorem+Proving+in+Higher+Order+Logics%2C+pages+60%E2%80%9366%2E+Springer%2E)
14. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. [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.
15. Gautier Izacard, Mathilde Caron, Lucas Hosseini, Sebastian Riedel, Piotr Bojanowski, Armand Joulin, and Edouard Grave. 2021. [Unsupervised dense information retrieval with contrastive learning](https://md.research.elamur.ai/free/en/papers/izacard-2021-unsupervised-dense-information-retrieval-contrastive/). arXiv preprint arXiv:2112.09118.
16. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. 2022a. [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.
17. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pages 378–392. [find](https://scholar.google.com/scholar?q=Albert+Qiaochu+Jiang%2C+Wenda+Li%2C+Jesse+Michael+Han%2C+and+Yuhuai+Wu%2E+2021%2E+Lisa%3A+Language+models+of+isabelle+proofs%2E+In+6th+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+pages+378%E2%80%93392%2E)
18. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. 2022b. [Thor: Wielding hammers to integrate language models and automated theorem provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). Advances in Neural Information Processing Systems, 35:8360–8373.
19. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). Advances in neural information processing systems, 35:26337–26349.
20. Norman Megill and David A Wheeler. 2019. [Metamath: a computer language for mathematical proofs](https://md.research.elamur.ai/free/en/papers/megill-2019-metamath-computer-language-mathematical-proofs/). Lulu. com.
21. Yu Meng, Jiaxin Huang, Yu Zhang, and Jiawei Han. 2022. [Generating training data with language models: Towards zero-shot language understanding](https://md.research.elamur.ai/free/en/papers/meng-2022-generating-training-data-language-models/). Advances in Neural Information Processing Systems, 35:462–477.
22. Leonardo de Moura and Sebastian Ullrich. 2021. [The lean 4 theorem prover and programming language](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/). In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer.
23. Allen Newell and Herbert Simon. 1956. [The logic theory machine–a complex information processing system](https://md.research.elamur.ai/free/en/papers/newell-1956-logic-theory-machine-complex-information/). IRE Transactions on information theory, 2(3):61–79.
24. Lawrence C Paulson. 1994. Isabelle: A generic theorem prover. Springer. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulson%2E+1994%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2E)
25. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. [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.
26. Stanislas Polu and Ilya Sutskever. 2020. [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.
27. Machel Reid, Nikolay Savinov, Denis Teplyashin, Dmitry Lepikhin, Timothy Lillicrap, Jean-baptiste Alayrac, Radu Soricut, Angeliki Lazaridou, Orhan Firat, Julian Schrittwieser, et al. 2024. [Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context](https://md.research.elamur.ai/free/en/papers/gemini-team-2024-gemini-1-5-unlocking-multimodal/). arXiv preprint arXiv:2403.…
28. Baptiste Roziere, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Romain Sauvestre, Tal Remez, et al. 2023. [Code llama: Open foundation models for code](https://md.research.elamur.ai/free/en/papers/roziere-2024-code-llama-open-foundation-models/). arXiv preprint arXiv:2308.12950.
29. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Yu Wu, and Daya Guo. 2024. [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.
30. Demin Song, Honglin Guo, Yunhua Zhou, Shuhao Xing, Yudong Wang, Zifan Song, Wenwei Zhang, Qipeng Guo, Hang Yan, Xipeng Qiu, et al. 2024. Code needs comments: Enhancing code llms with comment augmentation. arXiv preprint arXiv:2402.13013. [find](https://scholar.google.com/scholar?q=Demin+Song%2C+Honglin+Guo%2C+Yunhua+Zhou%2C+Shuhao+Xing%2C+Yudong+Wang%2C+Zifan+Song%2C+Wenwei+Zhang%2C+Qipeng+Guo%2C+Hang+Yan%2C+Xipeng+Qiu%2C+et+al%2E+2024%2E+Code+needs+comments%3A+Enhancing+code+llms+with+comment+augmentat)
31. Petru Soviany, Radu Tudor Ionescu, Paolo Rota, and Nicu Sebe. 2022. Curriculum learning: A survey. International Journal of Computer Vision, 130(6):1526– 1565. [find](https://scholar.google.com/scholar?q=Petru+Soviany%2C+Radu+Tudor+Ionescu%2C+Paolo+Rota%2C+and+Nicu+Sebe%2E+2022%2E+Curriculum+learning%3A+A+survey%2E+International+Journal+of+Computer+Vision%2C+130%286%29%3A1526%E2%80%93+1565%2E)
32. Terence Tao. 2023. A slightly longer lean 4 proof tour. [https://terrytao.wordpress.com/2023/12/](https://terrytao.wordpress.com/2023/12/) 05/a-slightly-longer-lean-4-proof-tour/. Accessed: 2024-06-15. [↗](https://terrytao.wordpress.com/2023/12/)
33. Terence Tao, Yael Dillies, and Bhavik Mehta. 2023. Formalizing the proof of pfr in lean4 using blueprint: a short tour. Accessed: 2024-06-15. [find](https://scholar.google.com/scholar?q=Terence+Tao%2C+Yael+Dillies%2C+and+Bhavik+Mehta%2E+2023%2E+Formalizing+the+proof+of+pfr+in+lean4+using+blueprint%3A+a+short+tour%2E+Accessed%3A+2024%2D06%2D15%2E)
34. Richard Taylor and Andrew Wiles. 1995. Ring-theoretic properties of certain hecke algebras. Annals of Mathematics, 141(3):553–572. [find](https://scholar.google.com/scholar?q=Richard+Taylor+and+Andrew+Wiles%2E+1995%2E+Ring%2Dtheoretic+properties+of+certain+hecke+algebras%2E+Annals+of+Mathematics%2C+141%283%29%3A553%E2%80%93572%2E)
35. Ruida Wang, Wangchunshu Zhou, and Mrinmaya Sachan. 2023. Let’s synthesize step by step: Iterative dataset synthesis with large language models by extrapolating errors from small models. arXiv preprint arXiv:2310.13671. [find](https://scholar.google.com/scholar?q=Ruida+Wang%2C+Wangchunshu+Zhou%2C+and+Mrinmaya+Sachan%2E+2023%2E+Let%E2%80%99s+synthesize+step+by+step%3A+Iterative+dataset+synthesis+with+large+language+models+by+extrapolating+errors+from+small+models%2E+arXiv+preprint)
36. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, et al. 2022. [Chain-of-thought prompting elicits reasoning in large language models](https://md.research.elamur.ai/free/en/papers/wei-2022-chain-thought-prompting-elicits-reasoning/). Advances in neural information processing systems, 35:24824–24837.
37. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in Neural Information Processing Systems, 35:32353–32368.
38. Kaiyu Yang and Jia Deng. 2019. [Learning to prove theorems via interacting with proof assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/). In International Conference on Machine Learning, pages 6984–6994. PMLR.
39. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2024. [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.
40. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. [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.
41. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. [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.

*Updated 3 November 2026*