---
title: "REAL-Prover — paper by Shen et al. (2025) — summary and ideas"
description: "LLM-based provers for Lean 4 handle olympiad-style problems well, but they rarely carry over to… 39 references, cited by 10 papers here."
authors: ["Ziju Shen", "Naohao Huang", "Fanyi Yang", "Yutong Wang", "Guoxiong Gao", "Tianyi Xu", "Jiedong Jiang", "Wanyi He", "Pu Yang", "Mengzhou Sun", "Haocheng Ju", "Peihao Wu", "Bryan Dai", "Bin Dong"]
year: 2025
venue: "arXiv:2505.20613"
source: "https://arxiv.org/abs/2505.20613"
doi: "10.48550/arxiv.2505.20613"
arxiv: "2505.20613"
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/shen-2025-real-prover-retrieval-augmented-lean/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/shen-2025-real-prover-retrieval-augmented-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/9/) / REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

# REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

**Authors:** Ziju Shen, Naohao Huang, Fanyi Yang, [Yutong Wang](https://md.research.elamur.ai/free/en/authors/yutong-wang/), [Guoxiong Gao](https://md.research.elamur.ai/free/en/authors/guoxiong-gao/), [Tianyi Xu](https://md.research.elamur.ai/free/en/authors/tianyi-xu/), [Jiedong Jiang](https://md.research.elamur.ai/free/en/authors/jiedong-jiang/), Wanyi He, Pu Yang, Mengzhou Sun, [Haocheng Ju](https://md.research.elamur.ai/free/en/authors/haocheng-ju/), Peihao Wu, [Bryan Dai](https://md.research.elamur.ai/free/en/authors/bryan-dai/) and [Bin Dong](https://md.research.elamur.ai/free/en/authors/bin-dong/) · **Year:** 2025 · **Venue:** arXiv:2505.20613 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 0 citations (OpenAlex, 2026-10-14) · 10 in our library, of the 149,439 papers whose bibliographies we read

## Summary
LLM-based provers for Lean 4 handle olympiad-style problems well, but they rarely carry over to university and graduate mathematics. At that level, proofs depend on finding the right lemmas among Mathlib's very large collection of results. REAL-Prover addresses this with a stepwise tree-search prover. At every proof state, the fine-tuned model REAL-Prover-v1 proposes tactics, and the LeanSearch-PS retriever adds semantically related Mathlib theorems to its prompt.

Training data come from HERALD-AF. This pipeline formalizes informal problems with Herald-translator and back-translates them via DeepSeek-V3. It keeps only statements that an LLM judges faithful to the original. Proofs for these statements are then synthesized through expert iteration in a new Lean 4 environment, Jixia-interactive.

Using supervised fine-tuning alone, the system reaches 23.7% Pass@64 on ProofNet, comparable to leading models. It scores 56.7% on FATE-M, a new graduate-level algebra benchmark, which is state of the art. The work shows that retrieval is an effective lever for advanced formal mathematics, and the components are released as open source.

## Key points
- Ablation: without retrieval (REAL-Prover-v1-NoRet), FATE-M accuracy drops from 56.7% to 44.7%, and ProofNet from 23.7% to 22.6%.
- On miniF2F, REAL-Prover scores 54.1% with a 64×64 budget, trailing RL-trained systems such as BFS-Prover (70.8%). The authors cite two reasons: olympiad problems rely less on Mathlib, and their model lacks RL.
- The authors release a dataset of 55k state–tactic pairs collected during expert iteration.
- FATE-M (Formal Algebra Theorem Evaluation–Medium) pairs informal and formal problems in graduate abstract algebra: groups, rings and fields.
- Planned extensions are RL fine-tuning (e.g., GRPO) and a natural-language chain-of-thought layer. Code: github.com/frenzymath/REAL-Prover.

*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

- [Peking University](https://md.research.elamur.ai/free/en/universities/peking-university/) — University, Beijing, China · 315 works · 43,267 citations
- [National University of Singapore](https://md.research.elamur.ai/free/en/universities/national-university-of-singapore/) — University, Singapore, Singapore · 207 works · 39,576 citations
- [Renmin University of China](https://md.research.elamur.ai/free/en/universities/renmin-university-of-china/) — University, Beijing, China · 139 works · 17,752 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 (2): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works · [🔍 Information retrieval & search](https://md.research.elamur.ai/free/en/topics/information-retrieval/) · 552 works

## Cite

Cite as: Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai and Bin Dong. 2025. REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning. arXiv:2505.20613.

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

```bibtex
@misc{shen2025real,
  title = {{REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning}},
  author = {Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai and Bin Dong},
  year = {2025},
  doi = {10.48550/arxiv.2505.20613},
  eprint = {2505.20613},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2505.20613}
}
```

- [← previous QwenLong-L1.5: Post-Training Recipe for Long-Context Reasoning and Memory Management](https://md.research.elamur.ai/free/en/papers/shen-2025-qwenlong-l1-5-post/)
- [next → RichRAG: Crafting Rich Responses for Multi-faceted Queries in Retrieval-Augmented Generation](https://md.research.elamur.ai/free/en/papers/wang-2025-richrag-crafting-rich-responses-multi/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/9/)

## References

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

1. Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Deepak Kapur, editor, Computer Mathematics, pages 333–333, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. [find](https://scholar.google.com/scholar?q=Georges+Gonthier%2E+The+four+colour+theorem%3A+Engineering+of+a+formal+proof%2E+In+Deepak+Kapur%2C+editor%2C+Computer+Mathematics%2C+pages+333%E2%80%93333%2C+Berlin%2C+Heidelberg%2C+2008%2E+Springer+Berlin+Heidelberg%2E)
2. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandr… [find](https://scholar.google.com/scholar?q=Georges+Gonthier%2C+Andrea+Asperti%2C+Jeremy+Avigad%2C+Yves+Bertot%2C+Cyril+Cohen%2C+Fran%C3%A7ois+Garillot%2C+St%C3%A9phane+Le+Roux%2C+Assia+Mahboubi%2C+Russell+O%E2%80%99Connor%2C+Sidi+Ould+Biha%2C+Ioana+Pasca%2C+Laurence+Rideau%2C+Alexey+S)
3. 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/).
4. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. [find](https://scholar.google.com/scholar?q=Yves+Bertot+and+Pierre+Cast%C3%A9ran%2E+Interactive+theorem+proving+and+program+development%3A+Coq%E2%80%99Art%3A+the+calculus+of+inductive+constructions%2E+Springer+Science+%26+Business+Media%2C+2013%2E)
5. 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.
6. Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. [A semantic search engine for mathlib4](https://md.research.elamur.ai/free/en/papers/gao-2024-semantic-search-engine-mathlib4/). In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Findings of the Association for Computational Linguistics: EMNLP 2024, pages 8001–8013, Miami, Florida, USA, November 2024. Associa…
7. 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.
8. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. [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/). In The Eleventh International Conference on Learning Representations, 2023.
9. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-based demonstration learning for formal theorem proving. In Forty-first International Conference on Machine Learning, 2024. [find](https://scholar.google.com/scholar?q=Xueliang+Zhao%2C+Wenda+Li%2C+and+Lingpeng+Kong%2E+Subgoal%2Dbased+demonstration+learning+for+formal+theorem+proving%2E+In+Forty%2Dfirst+International+Conference+on+Machine+Learning%2C+2024%2E)
10. Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, 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/). In The Twelfth International Conference on Learning Representations, 2024.
11. Huajian Xin, Daya Guo, Zhihong Shao, Z.Z. Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Advancing theorem proving in LLMs through large-scale synthetic data. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. [find](https://scholar.google.com/scholar?q=Huajian+Xin%2C+Daya+Guo%2C+Zhihong+Shao%2C+Z%2EZ%2E+Ren%2C+Qihao+Zhu%2C+Bo+Liu%2C+Chong+Ruan%2C+Wenda+Li%2C+and+Xiaodan+Liang%2E+Advancing+theorem+proving+in+LLMs+through+large%2Dscale+synthetic+data%2E+In+The+4th+Workshop+on+)
12. 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/).
13. Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learnin… — [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
14. Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025. [find](https://scholar.google.com/scholar?q=Ran+Xin%2C+Chenguang+Xi%2C+Jie+Yang%2C+Feng+Chen%2C+Hang+Wu%2C+Xia+Xiao%2C+Yifan+Sun%2C+Shen+Zheng%2C+and+Kai+Shen%2E+Bfs%2Dprover%3A+Scalable+best%2Dfirst+tree+search+for+llm%2Dbased+automatic+theorem+proving%2E+arXiv+preprint+)
15. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcemen… — [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)
16. Huajian Xin, Daya Guo, Zhihong Shao, Z.Z. Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Advancing theorem proving in LLMs through large-scale synthetic data. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. [find](https://scholar.google.com/scholar?q=Huajian+Xin%2C+Daya+Guo%2C+Zhihong+Shao%2C+Z%2EZ%2E+Ren%2C+Qihao+Zhu%2C+Bo+Liu%2C+Chong+Ruan%2C+Wenda+Li%2C+and+Xiaodan+Liang%2E+Advancing+theorem+proving+in+LLMs+through+large%2Dscale+synthetic+data%2E+In+The+4th+Workshop+on+)
17. Qihao Zhu Zhihong Shao, Peiyi Wang 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/). CoRR, abs/2402.03300, 2024.
18. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. [Goedel-prover: A frontier model for open-source automated theorem proving](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/). arXiv preprint arXiv:2502.07640, 2025.
19. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. [Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/). arXiv preprint arXiv:2412.20735, 2024.
20. Kaiyu Yang, Aidan M 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 Thirty-seventh Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023…
21. Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick SH Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. [Dense passage retrieval for open-domain question answering](https://md.research.elamur.ai/free/en/papers/karpukhin-2020-dense-passage-retrieval-open-domain/). In EMNLP (1), pages 6769–6781, 2020.
22. Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anandkumar. Leanagent: Lifelong learning for formal theorem proving. In The Thirteenth International Conference on Learning Representations, 2025. [find](https://scholar.google.com/scholar?q=Adarsh+Kumarappan%2C+Mo+Tiwari%2C+Peiyang+Song%2C+Robert+Joseph+George%2C+Chaowei+Xiao%2C+and+Anima+Anandkumar%2E+Leanagent%3A+Lifelong+learning+for+formal+theorem+proving%2E+In+The+Thirteenth+International+Conferenc)
23. 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/). CoRR, abs/2109.00110, 2021.
24. 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.
25. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations, 2025. [find](https://scholar.google.com/scholar?q=Guoxiong+Gao%2C+Yutong+Wang%2C+Jiedong+Jiang%2C+Qi+Gao%2C+Zihan+Qin%2C+Tianyi+Xu%2C+and+Bin+Dong%2E+Herald%3A+A+natural+language+annotated+lean+4+dataset%2E+In+The+Thirteenth+International+Conference+on+Learning+Repres)
26. DeepSeek-AI, Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, et al. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437, 2025. [find](https://scholar.google.com/scholar?q=DeepSeek%2DAI%2C+Aixin+Liu%2C+Bei+Feng%2C+Bing+Xue%2C+Bingxuan+Wang%2C+et+al%2E+Deepseek%2Dv3+technical+report%2E+arXiv+preprint+arXiv%3A2412%2E19437%2C+2025%2E)
27. frenzymath. jixia: A static analysis tool for lean 4. [https://github.com/frenzymath/jixia](https://github.com/frenzymath/jixia), 2024. [↗](https://github.com/frenzymath/jixia)
28. Rui Meng, Ye Liu, Shafiq Rayhan Joty, Caiming Xiong, Yingbo Zhou, and Semih Yavuz. SFR-Embedding-Mistral: Enhance text retrieval with transfer learning. Salesforce AI Research Blog, 2024. [find](https://scholar.google.com/scholar?q=Rui+Meng%2C+Ye+Liu%2C+Shafiq+Rayhan+Joty%2C+Caiming+Xiong%2C+Yingbo+Zhou%2C+and+Semih+Yavuz%2E+SFR%2DEmbedding%2DMistral%3A+Enhance+text+retrieval+with+transfer+learning%2E+Salesforce+AI+Research+Blog%2C+2024%2E)
29. Aaron van den Oord, Yazhe Li, and Oriol Vinyals. [Representation learning with contrastive predictive coding](https://md.research.elamur.ai/free/en/papers/oord-2018-representation-learning-contrastive-predictive-coding/). arXiv preprint arXiv:1807.03748, 2018.
30. An Yang, Baosong Yang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Zhou, Chengpeng Li, Chengyuan Li, Dayiheng Liu, Fei Huang, et al. Qwen2 technical report. arXiv preprint arXiv:2407.10671, 2024. [find](https://scholar.google.com/scholar?q=An+Yang%2C+Baosong+Yang%2C+Binyuan+Hui%2C+Bo+Zheng%2C+Bowen+Yu%2C+Chang+Zhou%2C+Chengpeng+Li%2C+Chengyuan+Li%2C+Dayiheng+Liu%2C+Fei+Huang%2C+et+al%2E+Qwen2+technical+report%2E+arXiv+preprint+arXiv%3A2407%2E10671%2C+2024%2E)
31. Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. Numinamath. Hugging Face repository, 2024. [find](https://scholar.google.com/scholar?q=Jia+LI%2C+Edward+Beeching%2C+Lewis+Tunstall%2C+Ben+Lipkin%2C+Roman+Soletskyi%2C+Shengyi+Costa+Huang%2C+Kashif+Rasul%2C+Longhui+Yu%2C+Albert+Jiang%2C+Ziju+Shen%2C+Zihan+Qin%2C+Bin+Dong%2C+Li+Zhou%2C+Yann+Fleureau%2C+Guillaume+Lam)
32. 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/). In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024.
33. Liang Wang, Nan Yang, Xiaolong Huang, Linjun Yang, Rangan Majumder, and Furu Wei. [Improving text embeddings with large language models](https://md.research.elamur.ai/free/en/papers/wang-2024-improving-text-embeddings-large-language/). In Lun-Wei Ku, Andre Martins, and Vivek Srikumar, editors, Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long P…
34. Luyu Gao, Xueguang Ma, Jimmy Lin, and Jamie Callan. Tevatron: An efficient and flexible toolkit for neural retrieval. In Proceedings of the 46th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’23, page 3120–3124, New York, NY, USA, 2023. Association fo… [find](https://scholar.google.com/scholar?q=Luyu+Gao%2C+Xueguang+Ma%2C+Jimmy+Lin%2C+and+Jamie+Callan%2E+Tevatron%3A+An+efficient+and+flexible+toolkit+for+neural+retrieval%2E+In+Proceedings+of+the+46th+International+ACM+SIGIR+Conference+on+Research+and+Deve)
35. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. TheoremLlama: Transforming general-purpose LLMs into lean4 experts. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Proceedings of the 2024 Conference on Empirical Methods in Natural Language Proces… [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+In+Yaser+Al%2DOnaizan%2C+Mohit+Bansal%2C+and+Yun%2DNu)
36. Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025. [find](https://scholar.google.com/scholar?q=Jingyuan+Zhang%2C+Qi+Wang%2C+Xingguang+Ji%2C+Yahui+Liu%2C+Yang+Yue%2C+Fuzheng+Zhang%2C+Di+Zhang%2C+Guorui+Zhou%2C+and+Kun+Gai%2E+Leanabell%2Dprover%3A+Posttraining+scaling+in+formal+reasoning%2E+arXiv+preprint+arXiv%3A2504%2E061)
37. Kefan Dong and Tengyu Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025. [find](https://scholar.google.com/scholar?q=Kefan+Dong+and+Tengyu+Ma%2E+Stp%3A+Self%2Dplay+llm+theorem+provers+with+iterative+conjecturing+and+proving%2E+arXiv+preprint+arXiv%3A2502%2E00212%2C+2025%2E)
38. 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)
39. 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, editors, Advances in Neural Informatio…

*Updated 2 November 2026*