---
title: "MA-LoT — paper by Wang et al. (2025) — summary and ideas"
description: "Annotated Lean Long CoT data is scarce, so the authors introduce LoT-Transfer Learning (LoT-TL). 42 references, cited by 18 papers here."
authors: ["Ruida Wang", "Rui Pan", "Yuxin Li", "Jipeng Zhang", "Yizhen Jia", "Shizhe Diao", "Renjie Pi", "Junjie Hu", "Tong Zhang"]
year: 2025
venue: "arXiv:2503.03205"
source: "https://arxiv.org/abs/2503.03205"
doi: "10.48550/arxiv.2503.03205"
arxiv: "2503.03205"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/)

[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/5/) / MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

# MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

**Authors:** [Ruida Wang](https://md.research.elamur.ai/free/en/authors/ruida-wang/), [Rui Pan](https://md.research.elamur.ai/free/en/authors/rui-pan/), [Yuxin Li](https://md.research.elamur.ai/free/en/authors/yuxin-li/), [Jipeng Zhang](https://md.research.elamur.ai/free/en/authors/jipeng-zhang/), Yizhen Jia, [Shizhe Diao](https://md.research.elamur.ai/free/en/authors/shizhe-diao/), [Renjie Pi](https://md.research.elamur.ai/free/en/authors/renjie-pi/), [Junjie Hu](https://md.research.elamur.ai/free/en/authors/junjie-hu/) and [Tong Zhang](https://md.research.elamur.ai/free/en/authors/tong-zhang/) · **Year:** 2025 · **Venue:** arXiv:2503.03205 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [18](https://md.research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper addresses automated theorem proving in Lean4. Current LLM approaches fall into two camps. Step-by-step tree search uses verifier feedback but is costly and lacks high-level planning. Whole-proof generation exploits natural-language reasoning but never sees intermediate verifier signals. MA-LoT bridges these with a model-collaboration framework. A prover drafts a full proof after natural-language planning inside a Long Chain-of-Thought. A corrector then reads the Lean4 verifier's error messages, reasons about them in Long CoT, and outputs a revised proof over several rounds. Both roles are played by one trained model, LoT-Solver. Annotated Lean Long CoT data is scarce, so the authors introduce LoT-Transfer Learning (LoT-TL). This pipeline combines general natural-language Long CoT data, Lean SFT data for code completion, and pairs of failed and fixed proofs. During training, a system-prompt switch turns Long CoT off, and at inference the switch turns it on, so formal reasoning in Long CoT emerges without dedicated labels. On MiniF2F-Test (Lean4), MA-LoT outperforms strong prover baselines. The authors argue that pairing formal verification with reflective reasoning could also benefit other specialized domains.

## Key points
- MA-LoT scores 61.07% on the Lean4 MiniF2F-Test, compared with Godel-Prover at 55.33%, InternLM-Step-Prover at 50.70%, and DeepSeek-V3 at 33.61%, under similar sampling budgets.
- LoT-TL draws on three data sources: general NL Long CoT, Lean SFT (code completion), and Lean correction pairs. It toggles Long CoT through the system prompt rather than relying on annotated formal reasoning traces.
- In ablations, disabling Long CoT in LoT-Solver lowers accuracy from 51.64% to 49.18%. Fine-tuning DeepSeek-Prover-v1.5-RL on the same SFT data without Long CoT yields 48.36%.
- A dedicated corrector is essential: without it, the prover tends to repeat its wrong proof instead of analyzing the error. The framework solved several IMO- and AIME-level MiniF2F problems.
- The work appeared at ICML 2025, and the code is released at github.com/RickySkywalker/LeanOfThought-Official.

*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 (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 252 works

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

## Cite

Cite as: Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu and Tong Zhang. 2025. MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving. arXiv:2503.03205.

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

```bibtex
@misc{wang2025ma,
  title = {{MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving}},
  author = {Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu and Tong Zhang},
  year = {2025},
  doi = {10.48550/arxiv.2503.03205},
  eprint = {2503.03205},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2503.03205}
}
```

- [← previous LLMs know their vulnerabilities: Uncover Safety Gaps through Natural Distribution Shifts](https://md.research.elamur.ai/free/en/papers/ren-2025-llms-know-their-vulnerabilities-uncover/)
- [next → Multilingual Retrieval-Augmented Generation for Knowledge-Intensive Task](https://md.research.elamur.ai/free/en/papers/ranaldi-2025-multilingual-retrieval-augmented-generation-knowledge/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/5/)

## References

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

1. Achiam, J., Adler, S., Agarwal, S., Ahmad, L., Akkaya, I., Aleman, F. L., Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., 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. Azerbayev, Z., Schoelkopf, H., Paster, K., Santos, M. D., McAleer, S., Jiang, A. Q., Deng, J., Biderman, S., and Welleck, S. [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, 2023.
3. De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. 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=De+Moura%2C+L%2E%2C+Kong%2C+S%2E%2C+Avigad%2C+J%2E%2C+Van+Doorn%2C+F%2E%2C+and+von+Raumer%2C+J%2E+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction%2DCADE%2D25%3A+25th+International+Conference+on+Automated+Deduction)
4. Dong, K. and Ma, T. Beyond limited data: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025. [find](https://scholar.google.com/scholar?q=Dong%2C+K%2E+and+Ma%2C+T%2E+Beyond+limited+data%3A+Self%2Dplay+llm+theorem+provers+with+iterative+conjecturing+and+proving%2E+arXiv+preprint+arXiv%3A2502%2E00212%2C+2025%2E)
5. First, E., Rabe, M. N., Ringer, T., and Brun, Y. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1229–1241, 2023. [find](https://scholar.google.com/scholar?q=First%2C+E%2E%2C+Rabe%2C+M%2E+N%2E%2C+Ringer%2C+T%2E%2C+and+Brun%2C+Y%2E+Baldur%3A+Whole%2Dproof+generation+and+repair+with+large+language+models%2E+In+Proceedings+of+the+31st+ACM+Joint+European+Software+Engineering+Conference+and)
6. Frieder, S., Bayer, J., Collins, K. M., Berner, J., Loader, J., Juhász, A., Ruehle, F., Welleck, S., Poesia, G., Griffiths, R.-R., et al. Data for mathematical copilots: Better ways of presenting proofs for machine learning. arXiv preprint arXiv:2412.15184, 2024. — [arXiv:2412.15184](https://arxiv.org/abs/2412.15184) [find](https://scholar.google.com/scholar?q=Frieder%2C+S%2E%2C+Bayer%2C+J%2E%2C+Collins%2C+K%2E+M%2E%2C+Berner%2C+J%2E%2C+Loader%2C+J%2E%2C+Juha%CC%81sz%2C+A%2E%2C+Ruehle%2C+F%2E%2C+Welleck%2C+S%2E%2C+Poesia%2C+G%2E%2C+Griffiths%2C+R%2E%2DR%2E%2C+et+al%2E+Data+for+mathematical+copilots%3A+Better+ways+of+presenting+pro)
7. Harrison, J. Hol light: An overview. In International Conference on Theorem Proving in Higher Order Logics, pp. 60–66. Springer, 2009. [find](https://scholar.google.com/scholar?q=Harrison%2C+J%2E+Hol+light%3A+An+overview%2E+In+International+Conference+on+Theorem+Proving+in+Higher+Order+Logics%2C+pp%2E+60%E2%80%9366%2E+Springer%2C+2009%2E)
8. Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. [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. Jiang, A. Q., Li, W., Han, J. M., and Wu, Y. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378–392, 2021. [find](https://scholar.google.com/scholar?q=Jiang%2C+A%2E+Q%2E%2C+Li%2C+W%2E%2C+Han%2C+J%2E+M%2E%2C+and+Wu%2C+Y%2E+Lisa%3A+Language+models+of+isabelle+proofs%2E+In+6th+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+pp%2E+378%E2%80%93392%2C+2021%2E)
10. Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. [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.
11. Kumarappan, A., Tiwari, M., Song, P., George, R. J., Xiao, C., and Anandkumar, A. Leanagent: Lifelong learning for formal theorem proving. arXiv preprint arXiv:2410.06209, 2024. [find](https://scholar.google.com/scholar?q=Kumarappan%2C+A%2E%2C+Tiwari%2C+M%2E%2C+Song%2C+P%2E%2C+George%2C+R%2E+J%2E%2C+Xiao%2C+C%2E%2C+and+Anandkumar%2C+A%2E+Leanagent%3A+Lifelong+learning+for+formal+theorem+proving%2E+arXiv+preprint+arXiv%3A2410%2E06209%2C+2024%2E)
12. Lin, H., Sun, Z., Yang, Y., and Welleck, S. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024. [find](https://scholar.google.com/scholar?q=Lin%2C+H%2E%2C+Sun%2C+Z%2E%2C+Yang%2C+Y%2E%2C+and+Welleck%2C+S%2E+Lean%2Dstar%3A+Learning+to+interleave+thinking+and+proving%2E+arXiv+preprint+arXiv%3A2407%2E10040%2C+2024%2E)
13. Reid, M., Savinov, N., Teplyashin, D., Lepikhin, D., Lillicrap, T., Alayrac, J.-b., Soricut, R., Lazaridou, A., Firat, O., Schrittwieser, J., et al. [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.05530, 2024.
14. Lin, Y., Tang, S., Lyu, B., Wu, J., Lin, H., Yang, K., Li, J., Xia, M., Chen, D., Arora, S., and Jin, C. Goedel-prover: A frontier model for open-source automated theorem proving, 2025. URL [https://arxiv.org/](https://arxiv.org/) abs/2502.07640. [↗](https://arxiv.org/)
15. Shao, Z., Wang, P., Zhu, Q., Xu, R., Song, J., Bi, X., Zhang, H., Zhang, M., Li, Y., Wu, Y., 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.
16. Liu, A., Feng, B., Xue, B., Wang, B., Wu, B., Lu, C., Zhao, C., Deng, C., Zhang, C., Ruan, C., et al. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437, 2024. [find](https://scholar.google.com/scholar?q=Liu%2C+A%2E%2C+Feng%2C+B%2E%2C+Xue%2C+B%2E%2C+Wang%2C+B%2E%2C+Wu%2C+B%2E%2C+Lu%2C+C%2E%2C+Zhao%2C+C%2E%2C+Deng%2C+C%2E%2C+Zhang%2C+C%2E%2C+Ruan%2C+C%2E%2C+et+al%2E+Deepseek%2Dv3+technical+report%2E+arXiv+preprint+arXiv%3A2412%2E19437%2C+2024%2E)
17. Wang, R., Jansen, P., Côté, M.-A., and Ammanabrolu, P. Scienceworld: Is your agent smarter than a 5th grader? arXiv preprint arXiv:2203.07540, 2022. [find](https://scholar.google.com/scholar?q=Wang%2C+R%2E%2C+Jansen%2C+P%2E%2C+Co%CC%82te%CC%81%2C+M%2E%2DA%2E%2C+and+Ammanabrolu%2C+P%2E+Scienceworld%3A+Is+your+agent+smarter+than+a+5th+grader%3F+arXiv+preprint+arXiv%3A2203%2E07540%2C+2022%2E)
18. Ma, C., Zhang, J., Zhu, Z., Yang, C., Yang, Y., Jin, Y., Lan, Z., Kong, L., and He, J. Agentboard: An analytical evaluation board of multi-turn llm agents. arXiv preprint arXiv:2401.13178, 2024. [find](https://scholar.google.com/scholar?q=Ma%2C+C%2E%2C+Zhang%2C+J%2E%2C+Zhu%2C+Z%2E%2C+Yang%2C+C%2E%2C+Yang%2C+Y%2E%2C+Jin%2C+Y%2E%2C+Lan%2C+Z%2E%2C+Kong%2C+L%2E%2C+and+He%2C+J%2E+Agentboard%3A+An+analytical+evaluation+board+of+multi%2Dturn+llm+agents%2E+arXiv+preprint+arXiv%3A2401%2E13178%2C+2024%2E)
19. Wang, R., Zhou, W., and Sachan, M. Let’s synthesize step by step: Iterative dataset synthesis with large language models by extrapolating errors from small models. arXiv preprint arXiv:2310.13671, 2023. [find](https://scholar.google.com/scholar?q=Wang%2C+R%2E%2C+Zhou%2C+W%2E%2C+and+Sachan%2C+M%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+arXiv%3A2310%2E13671%2C+202)
20. Moura, L. d. and Ullrich, S. The lean 4 theorem prover and programming language. In Automated Deduction– CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, [Proceedings 28, pp](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/). 625–635.
21. Wang, R., Zhang, J., Jia, Y., Pan, R., Diao, S., Pi, R., and Zhang, T. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024. [find](https://scholar.google.com/scholar?q=Wang%2C+R%2E%2C+Zhang%2C+J%2E%2C+Jia%2C+Y%2E%2C+Pan%2C+R%2E%2C+Diao%2C+S%2E%2C+Pi%2C+R%2E%2C+and+Zhang%2C+T%2E+Theoremllama%3A+Transforming+general%2Dpurpose+llms+into+lean4+experts%2E+arXiv+preprint+arXiv%3A2407%2E03203%2C+2024%2E)
22. Wei, J., Wang, X., Schuurmans, D., Bosma, M., Xia, F., Chi, E., Le, Q. V., Zhou, D., 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.
23. Newell, A. and Simon, H. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 2(3):61–79, 1956. [find](https://scholar.google.com/scholar?q=Newell%2C+A%2E+and+Simon%2C+H%2E+The+logic+theory+machine%E2%80%93a+complex+information+processing+system%2E+IRE+Transactions+on+information+theory%2C+2%283%29%3A61%E2%80%9379%2C+1956%2E)
24. Open-Source-O1. Open-o1, 2024. URL [https://github.com/Open-Source-O1/Open-O1](https://github.com/Open-Source-O1/Open-O1). Accessed: 2024-12-28. [↗](https://github.com/Open-Source-O1/Open-O1)
25. Wu, Z., Huang, S., Zhou, Z., Ying, H., Wang, J., Lin, D., and Chen, K. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024a. [find](https://scholar.google.com/scholar?q=Wu%2C+Z%2E%2C+Huang%2C+S%2E%2C+Zhou%2C+Z%2E%2C+Ying%2C+H%2E%2C+Wang%2C+J%2E%2C+Lin%2C+D%2E%2C+and+Chen%2C+K%2E+Internlm2%2E+5%2Dstepprover%3A+Advancing+automated+theorem+proving+via+expert+iteration+on+large%2Dscale+lean+problems%2E+arXiv+preprint+ar)
26. OpenAI. Learning to reason with llms. [https://openai.com/index/](https://openai.com/index/) learning-to-reason-with-llms/, September 13 2024. Accessed: 2024-11-24. [↗](https://openai.com/index/)
27. Wu, Z., Wang, J., Lin, D., and Chen, K. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227, 2024b. [find](https://scholar.google.com/scholar?q=Wu%2C+Z%2E%2C+Wang%2C+J%2E%2C+Lin%2C+D%2E%2C+and+Chen%2C+K%2E+Lean%2Dgithub%3A+Compiling+github+lean+repositories+for+a+versatile+lean+prover%2E+arXiv+preprint+arXiv%3A2407%2E17227%2C+2024b%2E)
28. Paulson, L. C. Isabelle: A generic theorem prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=Paulson%2C+L%2E+C%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2C+1994%2E)
29. Xie, T., Zhou, F., Cheng, Z., Shi, P., Weng, L., Liu, Y., Hua, T. J., Zhao, J., Liu, Q., Liu, C., et al. [Openagents: An open platform for language agents in the wild](https://md.research.elamur.ai/free/en/papers/xie-2023-openagents-open-platform-language-agents/). arXiv preprint arXiv:2310.10634, 2023.
30. Polu, S. and Sutskever, I. [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. Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., and Liang, X. [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.
32. Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. [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.
33. Pourchot, A. and Sigaud, O. Cem-rl: Combining evolutionary and gradient-based methods for policy search. arXiv preprint arXiv:1810.01222, 2018. — [arXiv:1810.01222](https://arxiv.org/abs/1810.01222) [find](https://scholar.google.com/scholar?q=Pourchot%2C+A%2E+and+Sigaud%2C+O%2E+Cem%2Drl%3A+Combining+evolutionary+and+gradient%2Dbased+methods+for+policy+search%2E+arXiv+preprint+arXiv%3A1810%2E01222%2C+2018%2E+%E2%80%94+%5BarXiv%3A1810%2E01222%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1810%2E01222%29)
34. Xin, H., Ren, Z., Song, J., Shao, Z., Zhao, W., Wang, H., Liu, B., Zhang, L., Lu, X., Du, Q., 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/).
35. Reed, S., Zolna, K., Parisotto, E., Colmenarejo, S. G., Novikov, A., Barth-Maron, G., Gimenez, M., Sulsky, Y., Kay, J., Springenberg, J. T., et al. A generalist agent. arXiv preprint arXiv:2205.06175, 2022. [find](https://scholar.google.com/scholar?q=Reed%2C+S%2E%2C+Zolna%2C+K%2E%2C+Parisotto%2C+E%2E%2C+Colmenarejo%2C+S%2E+G%2E%2C+Novikov%2C+A%2E%2C+Barth%2DMaron%2C+G%2E%2C+Gimenez%2C+M%2E%2C+Sulsky%2C+Y%2E%2C+Kay%2C+J%2E%2C+Springenberg%2C+J%2E+T%2E%2C+et+al%2E+A+generalist+agent%2E+arXiv+preprint+arXiv%3A2205%2E06175%2C)
36. Xu, Y., Su, H., Xing, C., Mi, B., Liu, Q., Shi, W., Hui, B., Zhou, F., Liu, Y., Xie, T., et al. Lemur: Harmonizing natural language and code for language agents. arXiv preprint arXiv:2310.06830, 2023. — [arXiv:2310.06830](https://arxiv.org/abs/2310.06830) [find](https://scholar.google.com/scholar?q=Xu%2C+Y%2E%2C+Su%2C+H%2E%2C+Xing%2C+C%2E%2C+Mi%2C+B%2E%2C+Liu%2C+Q%2E%2C+Shi%2C+W%2E%2C+Hui%2C+B%2E%2C+Zhou%2C+F%2E%2C+Liu%2C+Y%2E%2C+Xie%2C+T%2E%2C+et+al%2E+Lemur%3A+Harmonizing+natural+language+and+code+for+language+agents%2E+arXiv+preprint+arXiv%3A2310%2E06830%2C+2023%2E)
37. Yang, H., Yue, S., and He, Y. Auto-gpt for online decision making: Benchmarks and additional opinions. arXiv preprint arXiv:2306.02224, 2023. [find](https://scholar.google.com/scholar?q=Yang%2C+H%2E%2C+Yue%2C+S%2E%2C+and+He%2C+Y%2E+Auto%2Dgpt+for+online+decision+making%3A+Benchmarks+and+additional+opinions%2E+arXiv+preprint+arXiv%3A2306%2E02224%2C+2023%2E)
38. Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., and Song, D. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024a. [find](https://scholar.google.com/scholar?q=Yang%2C+K%2E%2C+Poesia%2C+G%2E%2C+He%2C+J%2E%2C+Li%2C+W%2E%2C+Lauter%2C+K%2E%2C+Chaudhuri%2C+S%2E%2C+and+Song%2C+D%2E+Formal+mathematical+reasoning%3A+A+new+frontier+in+ai%2E+arXiv+preprint+arXiv%3A2412%2E16075%2C+2024a%2E)
39. Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. [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.
40. Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., and Chen, K. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024. [find](https://scholar.google.com/scholar?q=Ying%2C+H%2E%2C+Wu%2C+Z%2E%2C+Geng%2C+Y%2E%2C+Wang%2C+J%2E%2C+Lin%2C+D%2E%2C+and+Chen%2C+K%2E+Lean+workbook%3A+A+large%2Dscale+lean+problem+set+formalized+from+natural+language+math+problems%2E+arXiv+preprint+arXiv%3A2406%2E03847%2C+2024%2E)
41. Zheng, C., Wang, H., Xie, E., Liu, Z., Sun, J., Xin, H., Shen, J., Li, Z., and Li, Y. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806, 2023. [find](https://scholar.google.com/scholar?q=Zheng%2C+C%2E%2C+Wang%2C+H%2E%2C+Xie%2C+E%2E%2C+Liu%2C+Z%2E%2C+Sun%2C+J%2E%2C+Xin%2C+H%2E%2C+Shen%2C+J%2E%2C+Li%2C+Z%2E%2C+and+Li%2C+Y%2E+Lyra%3A+Orchestrating+dual+correction+in+automated+theorem+proving%2E+arXiv+preprint+arXiv%3A2309%2E15806%2C+2023%2E)
42. Zheng, K., Han, J. M., and Polu, S. [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 30 October 2026*