---
title: "Lean Workbook — paper by Ying et al. (2024)"
description: "Large language models do well on informal math but poorly on formal theorem proving in Lean. 34 references, cited by 74 papers here."
authors: ["Huaiyuan Ying", "Zijian Wu", "Yihan Geng", "Zheng Yuan", "Dahua Lin", "Kai Chen"]
year: 2024
venue: "arXiv:2406.03847"
source: "https://arxiv.org/abs/2406.03847"
doi: "10.48550/arxiv.2406.03847"
arxiv: "2406.03847"
licence: "CC BY-NC-ND 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by-nc-nd/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/)

[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/6/) / Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

# Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

**Authors:** [Huaiyuan Ying](https://md.research.elamur.ai/free/en/authors/huaiyuan-ying/), [Zijian Wu](https://md.research.elamur.ai/free/en/authors/zijian-wu/), [Yihan Geng](https://md.research.elamur.ai/free/en/authors/yihan-geng/), [Zheng Yuan](https://md.research.elamur.ai/free/en/authors/zheng-yuan/), [Dahua Lin](https://md.research.elamur.ai/free/en/authors/dahua-lin/) and [Kai Chen](https://md.research.elamur.ai/free/en/authors/kai-chen/) · **Year:** 2024 · **Venue:** [arXiv:2406.03847](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/) ([NeurIPS 2024](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/2024/)) · **Licence:** [CC BY-NC-ND 4.0 (arXiv)](https://creativecommons.org/licenses/by-nc-nd/4.0/)

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

**Citations:** 6 citations (OpenAlex, 2026-10-14) · [74](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Large language models do well on informal math but poorly on formal theorem proving in Lean. A main reason is the lack of formal training data: MiniF2F is small, and Mathlib mostly covers foundational theorems rather than competition problems. The authors built an active-learning autoformalization pipeline that translates natural-language problems into Lean 4 statements and back. They first trained a translator on paired data from MiniF2F and ProofNet. They then applied it to problems collected from the Art of Problem Solving forum, which an auxiliary LLM had extracted and cleaned. Each candidate statement had to compile in Lean, survive back-translation with an NLI consistency check, and pass human inspection. Experts corrected recurring error patterns and added the fixes as training data for the next round. The resulting resource, Lean Workbook, holds about 57K formal–informal problem pairs, and a manual sample check put its accuracy at 93.5%. Adding it to training improves prover accuracy on MiniF2F. It gives the community open, contest-level data for autoformalization and automated proving.

## Key points
- **Models:** the translator starts from InternLM-Math-Plus-20B, and Qwen-1.5-14B-Chat extracts problems and filters out ill-defined ones.
- **Filtering signal:** compile pass counts rose from 136,670 (first-round model) to 205,079 (final-round model). NLI pass counts rose from 37,122 to 57,231.
- **Downstream gain:** fine-tuning an InternLM2-Math-Plus prover with Lean Workbook lifted MiniF2F-test accuracy from 37.3% to 46.7%, and MiniF2F-valid from 44.3% to 50.4%.
- **Proofs and IMO problems:** about 5K of the problems include formal proofs found by search. The pipeline also produced 21 IMO problems not yet formalized in Compfiles: 14 algebra, 5 number theory and 2 combinatorics.
- **Release:** code is in InternLM-Math and the data is on Hugging Face (InternLM/Lean-Workbook), plus a larger Lean Workbook Plus variant. The authors note that this variant makes more mistakes on number-theory problems.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

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

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

## Cite

Cite as: Huaiyuan Ying, Zijian Wu, Yihan Geng, Zheng Yuan, Dahua Lin and Kai Chen. 2024. Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. arXiv:2406.03847.

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

```bibtex
@misc{ying2024lean,
  title = {{Lean Workbook: A large-scale Lean problem set formalized from natural language math problems}},
  author = {Huaiyuan Ying, Zijian Wu, Yihan Geng, Zheng Yuan, Dahua Lin and Kai Chen},
  year = {2024},
  doi = {10.48550/arxiv.2406.03847},
  eprint = {2406.03847},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2406.03847}
}
```

- [← previous AppWorld: A Controllable World of Apps and People for Benchmarking Interactive Coding Agents](https://md.research.elamur.ai/free/en/papers/trivedi-2024-appworld-controllable-world-apps-people/)
- [next → Leave No Context Behind: Efficient Infinite Context Transformers with Infini-attention](https://md.research.elamur.ai/free/en/papers/munkhdalai-2024-leave-no-context-behind-efficient/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/6/)

## References

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

1. 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.
2. 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, 2023.
3. 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/), 2023.
4. Jinze Bai, Shuai Bai, Yunfei Chu, Zeyu Cui, Kai Dang, Xiaodong Deng, Yang Fan, Wenbin Ge, Yu Han, Fei Huang, Binyuan Hui, Luo Ji, Mei Li, Junyang Lin, Runji Lin, Dayiheng Liu, Gao Liu, Chengqiang Lu, Keming Lu, Jianxin Ma, Rui Men, Xingzhang Ren, Xuancheng Ren, Chuanqi Tan, Sinan Tan, Jianhong Tu, P… — [Qwen Technical Report](https://md.research.elamur.ai/free/en/papers/bai-2023-qwen-technical-report/)
5. 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.
6. Google. [Gemini: A family of highly capable multimodal models](https://md.research.elamur.ai/free/en/papers/gemini-team-2023-gemini-family-highly-capable-multimodal/), 2023.
7. 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.
8. 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.
9. 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. In The Twelfth International Conference on Learning Representations, 2024. [find](https://scholar.google.com/scholar?q=Yinya+Huang%2C+Xiaohan+Lin%2C+Zhengying+Liu%2C+Qingxing+Cao%2C+Huajian+Xin%2C+Haiming+Wang%2C+Zhenguo+Li%2C+Linqi+Song%2C+and+Xiaodan+Liang%2E+MUSTARD%3A+Mastering+uniform+synthesis+of+theorem+and+proof+data%2E+In+The+Twel)
10. InternLM. Internlm: A multilingual language model with progressively enhanced capabilities. [https://github.com/InternLM/InternLM](https://github.com/InternLM/InternLM), 2023. [↗](https://github.com/InternLM/InternLM)
11. Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023. [find](https://scholar.google.com/scholar?q=Albert+Q+Jiang%2C+Wenda+Li%2C+and+Mateja+Jamnik%2E+Multilingual+mathematical+autoformalization%2E+arXiv+preprint+arXiv%3A2311%2E03755%2C+2023%2E)
12. 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.
13. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. [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, 2022.
14. 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.
15. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. [Solving quantitative reasoning problems with language models](https://md.research.elamur.ai/free/en/papers/lewkowycz-2022-solving-quantitative-reasoning-problems-language/). In NeurIPS, 2022.
16. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. [Fimo: A challenge formal dataset for automated theorem proving](https://md.research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/). arXiv preprint arXiv:2309.04295, 2023.
17. 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, POPL ’20. ACM, January 2020.
18. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28, pages 625–635, Cham, 2021. [Springer International Publishing](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/).
19. Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing Euclidean geometry. In International Conference on Machine Learning (ICML), 2024. [find](https://scholar.google.com/scholar?q=Logan+Murphy%2C+Kaiyu+Yang%2C+Jialiang+Sun%2C+Zhaoyu+Li%2C+Anima+Anandkumar%2C+and+Xujie+Si%2E+Autoformalizing+Euclidean+geometry%2E+In+International+Conference+on+Machine+Learning+%28ICML%29%2C+2024%2E)
20. OpenAI. [Gpt-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/), 2023.
21. Lawrence C. Paulson. Isabelle: The next 700 theorem provers, 2000. [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson%2E+Isabelle%3A+The+next+700+theorem+provers%2C+2000%2E)
22. 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/), 2022.
23. 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.
24. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. [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/), 2024.
25. Ross Taylor, Marcin Kardas, Guillem Cucurull, Thomas Scialom, Anthony Hartshorn, Elvis Saravia, Andrew Poulton, Viktor Kerkez, and Robert Stojnic. [Galactica: A large language model for science](https://md.research.elamur.ai/free/en/papers/taylor-2022-galactica-large-language-model-science/). 2023.
26. The Coq Development Team. The Coq reference manual – release 8.18.0. [https://coq.inria.fr/doc/V8.18.0/refman](https://coq.inria.fr/doc/V8.18.0/refman), 2023. [↗](https://coq.inria.fr/doc/V8.18.0/refman)
27. 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/), 2023.
28. 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.
29. Sean Welleck and Rahul Saha. Llmstep: Llm proofstep suggestions in lean. arXiv preprint arXiv:2310.18457, 2023. [find](https://scholar.google.com/scholar?q=Sean+Welleck+and+Rahul+Saha%2E+Llmstep%3A+Llm+proofstep+suggestions+in+lean%2E+arXiv+preprint+arXiv%3A2310%2E18457%2C+2023%2E)
30. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. 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/), 2022.
31. 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, 2024.
32. 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.
33. 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/)
34. 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*