---
title: "Lean-STaR: Learning to Interleave Thinking and Proving (2024)"
description: "Language-model provers for formal mathematics are usually trained only on proof code. 58 references, cited by 49 papers here."
authors: ["Haohan Lin", "Zhiqing Sun", "Sean Welleck", "Yiming Yang"]
year: 2024
venue: "arXiv:2407.10040"
source: "https://arxiv.org/abs/2407.10040"
doi: "10.48550/arxiv.2407.10040"
arxiv: "2407.10040"
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/lin-2024-lean-star-learning-interleave-thinking/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/)

[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/) / Lean-STaR: Learning to Interleave Thinking and Proving

# Lean-STaR: Learning to Interleave Thinking and Proving

**Authors:** Haohan Lin, [Zhiqing Sun](https://md.research.elamur.ai/free/en/authors/zhiqing-sun/), [Sean Welleck](https://md.research.elamur.ai/free/en/authors/sean-welleck/) and [Yiming Yang](https://md.research.elamur.ai/free/en/authors/yiming-yang/) · **Year:** 2024 · **Venue:** arXiv:2407.10040 · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 2 citations (OpenAlex, 2026-10-14) · [49](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Language-model provers for formal mathematics are usually trained only on proof code. That code leaves out the informal reasoning a person does before choosing each step. Lean-STaR addresses this by training a model to write a brief natural-language "thought" before predicting every Lean tactic.

Training has two stages. First, GPT-4 receives proof states paired with the ground-truth tactics from Mathlib. It writes retrospective rationales that justify each tactic, producing roughly 50k (state, thought, tactic) examples. Fine-tuning on these gives a thought-augmented tactic predictor called Lean-CoT. Second, following the Self-Taught Reasoner (STaR) approach, the model undergoes expert iteration. It samples thought-annotated proofs, Lean checks them, and only verified proofs are kept as new training data.

On miniF2F-test, the method beats direct tactic-prediction baselines. With InternLM2-7b-plus it reaches 45.4% pass@32. The work matters because it links informal reasoning with machine-checked proofs. It also yields what the authors call the first thought-augmented dataset for theorem proving.

## Key points
- About 50k thought-augmented examples were synthesized from Mathlib with GPT-4. Two rounds of expert iteration added roughly 50k more.
- The model factorizes tactic prediction into generating a thought given the state, then a tactic given both. Lean's verification signal supplies the reward.
- With InternLM2-7b as the base model, Lean-STaR solves 34.8% (pass@32) and 36.1% (pass@64) of miniF2F-test.
- With InternLM2-7b-plus, it scores 45.4% pass@32 against a prior 43.4%. The abstract reports 43.4% → 46.3% at Pass@64.
- Arithmetic slips in the thoughts can be harmless, because Lean tactics such as nlinarith do the actual calculation.

*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

- [Carnegie Mellon University](https://md.research.elamur.ai/free/en/universities/carnegie-mellon-university/) — University, Pittsburgh, United States · 633 works · 195,218 citations
- [Tsinghua University](https://md.research.elamur.ai/free/en/universities/tsinghua-university/) — University, Beijing, China · 439 works · 94,783 citations

📚 Shelves (3): [🖥️ 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 · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Haohan Lin, Zhiqing Sun, Sean Welleck and Yiming Yang. 2024. Lean-STaR: Learning to Interleave Thinking and Proving. arXiv:2407.10040.

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

```bibtex
@misc{lin2024lean,
  title = {{Lean-STaR: Learning to Interleave Thinking and Proving}},
  author = {Haohan Lin, Zhiqing Sun, Sean Welleck and Yiming Yang},
  year = {2024},
  doi = {10.48550/arxiv.2407.10040},
  eprint = {2407.10040},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2407.10040}
}
```

- [← previous From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models](https://md.research.elamur.ai/free/en/papers/welleck-2024-decoding-meta-generation-inference-time/)
- [next → LlaSMol: Advancing Large Language Models for Chemistry with a Large-Scale, Comprehensive, High-Quality Instruction Tuning Dataset](https://md.research.elamur.ai/free/en/papers/yu-2024-llasmol-advancing-large-language-models/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/8/)

## References

58 references, 41 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. [Gpt-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv preprint arXiv:2303.08774, 2023.
2. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. [Towards a mathematics formalisation assistant using large language models](https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/). arXiv preprint arXiv:2211.07524, 2022.
3. 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/). Advances in neural information processing systems, 30, 2017.
4. Jeremy Avigad. Mathematics and the formal turn, 2023. [find](https://scholar.google.com/scholar?q=Jeremy+Avigad%2E+Mathematics+and+the+formal+turn%2C+2023%2E)
5. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. [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, 2023a.
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](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/). arXiv preprint arXiv:2310.10631, 2023b.
7. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. [Hammering towards qed](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). Journal of Formalized Reasoning, 9(1):101–148, 2016.
8. Sascha Bohme and Tobias Nipkow. Sledgehammer: judgement day. In Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings 5, pp. 107–121. [find](https://scholar.google.com/scholar?q=Sascha+Bohme+and+Tobias+Nipkow%2E+Sledgehammer%3A+judgement+day%2E+In+Automated+Reasoning%3A+5th+International+Joint+Conference%2C+IJCAR+2010%2C+Edinburgh%2C+UK%2C+July+16%2D19%2C+2010%2E+Proceedings+5%2C+pp%2E+107%E2%80%93121%2E)
9. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. [Language models are few-shot learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/). Advances in neural information processing systems, 33:1877–1901, 2020.
10. Kevin Buzzard. Lean in 2024. [https://xenaproject.wordpress.com/2024/01/20/](https://xenaproject.wordpress.com/2024/01/20/) lean-in-2024/, 2024. [↗](https://xenaproject.wordpress.com/2024/01/20/)
11. Nathan C Carter and Kenneth G Monks. Lurch: a word processor that can grade students’ proofs. In CICM Workshops, 2013. [find](https://scholar.google.com/scholar?q=Nathan+C+Carter+and+Kenneth+G+Monks%2E+Lurch%3A+a+word+processor+that+can+grade+students%E2%80%99+proofs%2E+In+CICM+Workshops%2C+2013%2E)
12. Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks. arXiv preprint arXiv:2211.12588, 2022. [find](https://scholar.google.com/scholar?q=Wenhu+Chen%2C+Xueguang+Ma%2C+Xinyi+Wang%2C+and+William+W+Cohen%2E+Program+of+thoughts+prompting%3A+Disentangling+computation+from+reasoning+for+numerical+reasoning+tasks%2E+arXiv+preprint+arXiv%3A2211%2E12588%2C+2022%2E)
13. Projet Coq. The coq proof assistant-reference manual. INRIA Rocquencourt and ENS Lyon, version, 5, 1996. [find](https://scholar.google.com/scholar?q=Projet+Coq%2E+The+coq+proof+assistant%2Dreference+manual%2E+INRIA+Rocquencourt+and+ENS+Lyon%2C+version%2C+5%2C+1996%2E)
14. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. Journal of automated reasoning, 61:423–453, 2018. [find](https://scholar.google.com/scholar?q=Lukasz+Czajka+and+Cezary+Kaliszyk%2E+Hammer+for+coq%3A+Automation+for+dependent+type+theory%2E+Journal+of+automated+reasoning%2C+61%3A423%E2%80%93453%2C+2018%2E)
15. 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)
16. Emily First. Automating the Formal Verification of Software. PhD thesis, 2023. URL [https://scholarworks.umass.edu/dissertations_2/2812](https://scholarworks.umass.edu/dissertations_2/2812). [↗](https://scholarworks.umass.edu/dissertations_2/2812)
17. Emily First, Markus 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 Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, pp. 1229–1241, New York…
18. Fabian Gloeckle, Baptiste Roziere, Amaury Hayat, and Gabriel Synnaeve. Temperature-scaled large language models for lean proofstep prediction. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, 2023. [find](https://scholar.google.com/scholar?q=Fabian+Gloeckle%2C+Baptiste+Roziere%2C+Amaury+Hayat%2C+and+Gabriel+Synnaeve%2E+Temperature%2Dscaled+large+language+models+for+lean+proofstep+prediction%2E+In+The+3rd+Workshop+on+Mathematical+Reasoning+and+AI+at+N)
19. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. [Proof artifact co-training for theorem proving with language models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). arXiv preprint arXiv:2102.06203, 2021.
20. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. [Proof artifact co-training for theorem proving with language models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). In International Conference on Learning Representations, 2022. URL [https://openreview.net/forum?id=rpxJc9j04U](https://openreview.net/forum?id=rpxJc9j04U). [↗](https://openreview.net/forum?id=rpxJc9j04U)
21. 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.
22. Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. [Mustard: Mastering uniform synthesis of theorem and proof data](https://md.research.elamur.ai/free/en/papers/huang-2024-mustard-mastering-uniform-synthesis-theorem/). arXiv preprint arXiv:2402.08957, 2024.
23. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothee 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.
24. Dongyeop Kang, Andrew Head, Risham Sidhu, Kyle Lo, Daniel S Weld, and Marti A Hearst. Document-level definition detection in scholarly documents: Existing models, error analyses, and future directions. arXiv preprint arXiv:2010.05129, 2020. [find](https://scholar.google.com/scholar?q=Dongyeop+Kang%2C+Andrew+Head%2C+Risham+Sidhu%2C+Kyle+Lo%2C+Daniel+S+Weld%2C+and+Marti+A+Hearst%2E+Document%2Dlevel+definition+detection+in+scholarly+documents%3A+Existing+models%2C+error+analyses%2C+and+future+directions)
25. 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/). Advances in neural information processing systems, 35:26337–26349, 2022.
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](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/), 2024.
27. The mathlib Community. [The lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367–381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974. doi: 10.1145/ 3372885.3373824. URL https://d…
28. Allen Newell and Herbert Simon. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 2(3):61–79, 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/)
29. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. [find](https://scholar.google.com/scholar?q=Tobias+Nipkow%2C+Markus+Wenzel%2C+and+Lawrence+C+Paulson%2E+Isabelle%2FHOL%3A+a+proof+assistant+for+higher%2Dorder+logic%2E+Springer%2C+2002%2E)
30. Maxwell Nye, Anders Johan Andreassen, Guy Gur-Ari, Henryk Michalewski, Jacob Austin, David Bieber, David Dohan, Aitor Lewkowycz, Maarten Bosma, David Luan, et al. [Show your work: Scratchpads for intermediate computation with language models](https://md.research.elamur.ai/free/en/papers/al-2021-show-your-work-scratchpads-intermediate/). arXiv preprint arXiv:2112.00114, 2021.
31. National Academies of Sciences. Artificial intelligence to assist mathematical reasoning: Proceedings of a workshop, 2023. [find](https://scholar.google.com/scholar?q=National+Academies+of+Sciences%2E+Artificial+intelligence+to+assist+mathematical+reasoning%3A+Proceedings+of+a+workshop%2C+2023%2E)
32. OpenAI. OpenAI: GPT-4, 2023. URL [https://openai.com/research/gpt-4](https://openai.com/research/gpt-4). [↗](https://openai.com/research/gpt-4)
33. 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.
34. 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.
35. Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. [Mathematical reasoning via self-supervised skip-tree training](https://md.research.elamur.ai/free/en/papers/rabe-2020-mathematical-reasoning-self-supervised-skip/). arXiv preprint arXiv:2006.04757, 2020.
36. Avi Singh, John D Co-Reyes, Rishabh Agarwal, Ankesh Anand, Piyush Patil, Peter J Liu, James Harrison, Jaehoon Lee, Kelvin Xu, Aaron Parisi, et al. [Beyond human data: Scaling self-training for problem-solving with language models](https://md.research.elamur.ai/free/en/papers/singh-2023-human-data-scaling-self-training/). arXiv preprint arXiv:2312.06585, 2023.
37. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pp. 3–20. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2E+A+promising+path+towards+autoformalization+and+general+artificial+intelligence%2E+In+Intelligent+Computer+Mathematics%3A+13th+International+Conference%2C+CICM+2020%2C+Bertinoro%2C+Italy%2C+July)
38. Terence Tao. [https://mathstodon.xyz/@tao/111287749336059662](https://mathstodon.xyz/@tao/111287749336059662), 2023. [↗](https://mathstodon.xyz/@tao/111287749336059662)
39. Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach to formal theorem-proving. arXiv preprint arXiv:2310.[04353, 2023](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/).
40. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. [An in-context learning agent for formal theorem-proving](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/), 2024. URL https://arxiv.org/abs/ 2310.04353. [↗](https://arxiv.org/abs/)
41. Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. [Lego-prover: Neural theorem proving with growing libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/), 2023a.
42. Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. [Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function](https://md.research.elamur.ai/free/en/papers/wang-2023-dt-solver-automated-theorem-proving/). In Proceedings of the 61st Annual Meeting of the Association for Computational…
43. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. [Exploration of neural machine translation in autoformalization of mathematics in mizar](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/). In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 85–98, 2020.
44. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, et al. [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, 2022.
45. Sean Welleck and Rahul Saha. [Llmstep: Llm proofstep suggestions in lean](https://md.research.elamur.ai/free/en/papers/welleck-2023-llmstep-llm-proofstep-suggestions-lean/). arXiv preprint arXiv:2310.18457, 2023.
46. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. [Naturalproofs: Mathematical theorem proving in natural language](https://md.research.elamur.ai/free/en/papers/welleck-2021-naturalproofs-mathematical-theorem-proving-natural/). arXiv preprint arXiv:2104.01112, 2021.
47. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. [Naturalprover: Grounded mathematical proof generation with language models](https://md.research.elamur.ai/free/en/papers/welleck-2022-naturalprover-grounded-mathematical-proof-generation/). Advances in Neural Information Processing Systems, 35:4913–4927, 2022.
48. Yuhuai Wu, Markus N Rabe, Wenda Li, Jimmy Ba, Roger B Grosse, and Christian Szegedy. [Lime: Learning inductive bias for primitives of mathematical reasoning](https://md.research.elamur.ai/free/en/papers/wu-2021-lime-learning-inductive-bias-primitives/). In International Conference on Machine Learning, pp. 11251–11262. PMLR, 2021.
49. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles 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/). Advances in Neural Information Processing Systems, 35:32353–32368, 2022.
50. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. [Lego-prover: Neural theorem proving with growing libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). arXiv preprint arXiv:2310.00656, 2023.
51. 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](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). In Neural Information Processing Systems (NeurIPS), 2023.
52. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open m… — [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/)
53. Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. [Star: Bootstrapping reasoning with reasoning](https://md.research.elamur.ai/free/en/papers/zelikman-2022-star-bootstrapping-reasoning-reasoning/). Advances in Neural Information Processing Systems, 35:15476–15488, 2022.
54. Xueliang Zhao, Wenda Li, and Lingpeng Kong. [Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving](https://md.research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/), 2024. URL [https://openreview.net/forum?](https://openreview.net/forum?) id=xLoxMvO695. [↗](https://openreview.net/forum?)
55. 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.
56. Denny Zhou. Teach language models to reason. [https://dennyzhou.github.io/](https://dennyzhou.github.io/) LLMs-Reason-Taiwan-2023.pdf, 2023. Accessed: 2024-05-21. [↗](https://dennyzhou.github.io/)
57. Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization. arXiv preprint arXiv:2403.[18120, 2024a](https://md.research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/).
58. Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify – grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, 2024b. [URL https://openreview](https://md.research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/). net/forum?id=V5tdi1…

*Updated 3 November 2026*