mlsanityData to 7 Oct 2026

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

arXiv 2306.15626 ↗First posted 27 Jun 2023cs.LG cs.AI cs.LOcited by 414

On the map: Retrieval-augmented generation → Agentic RAG, agents and memory

Abstract (arXiv)

Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): an LLM-based prover augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 98,734 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.

Key facts. Cited by 414 papers in the map (data through 7 Oct 2026). Placed in Agentic RAG, agents and memory, one of 15 directions in Retrieval-augmented generation. Builds on 76 of its 107 references that are in the map. First posted on arXiv 27 Jun 2023.

Builds on

76 of 107 references.

References · 76

  1. 2017Attention Is All You Needcited by 59,932
  2. 2023GPT-4 Technical Reportcited by 18,132
  3. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,491
  4. 2023LLaMA: Open and Efficient Foundation Language Modelscited by 13,958
  5. 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,160
  6. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  7. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  8. 2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,072
  9. 2020Dense Passage Retrieval for Open-Domain Question Answeringcited by 3,779
  10. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,155
  11. 2020REALM: Retrieval-Augmented Language Model Pre-Trainingcited by 2,126
  12. 2022Survey of Hallucination in Natural Language Generationcited by 2,056
38 more
  1. 2018Datasheets for Datasetscited by 1,371
  2. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  3. 2021Improving language models by retrieving from trillions of tokenscited by 1,278
  4. 2020Leveraging Passage Retrieval with Generative Models for Open Domain Question Answeringcited by 1,203
  5. 2022Atlas: Few-shot Learning with Retrieval Augmented Language Modelscited by 940
  6. 2022CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesiscited by 876
  7. 2023StarCoder: may the source be with you!cited by 790
  8. 2019Generalization through Memorization: Nearest Neighbor Language Modelscited by 788
  9. 2021ByT5: Towards a token-free future with pre-trained byte-to-byte modelscited by 504
  10. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  11. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  12. 2023RepoCoder: Repository-Level Code Completion Through Iterative Retrieval and Generationcited by 357
  13. 2023CodeGeeX: A Pre-Trained Model for Code Generation with Multilingual Benchmarking on HumanEval-Xcited by 294
  14. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  15. 2022Autoformalization with Large Language Modelscited by 252
  16. 2022Transformer Memory as a Differentiable Search Indexcited by 242
  17. 2022Memorizing Transformerscited by 219
  18. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  19. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  20. 2023MEGABYTE: Predicting Million-byte Sequences with Multiscale Transformerscited by 164
  21. 2021Optimizing Dense Retrieval Model Training with Hard Negativescited by 154
  22. 2022DocPrompting: Generating Code by Retrieving the Docscited by 151
  23. 2021Retrieval Augmented Code Generation and Summarizationcited by 148
  24. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  25. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  26. 2019The Lean mathematical librarycited by 127
  27. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  28. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  29. 2022ReACC: A Retrieval-Augmented Code Completion Frameworkcited by 117
  30. 2022Autoregressive Search Engines: Generating Substrings as Document Identifierscited by 112
  31. 2022Training Language Models with Memory Augmentationcited by 112
  32. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  33. 2022Repository-Level Prompt Generation for Large Language Models of Codecited by 106
  34. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  35. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  36. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  37. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  38. 2022CoCoMIC: Code Completion By Jointly Modeling In-file and Cross-file Contextcited by 64

50 most cited of 76 All 76 (JSON)

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 23; 2024: 108; 2025: 113; 2026: 170.

414 papers.

Sort:

By area:

  1. 2023The Rise and Potential of Large Language Model Based Agents: A Surveycited by 1,422
  2. 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 763
  3. 2023A Comprehensive Overview of Large Language Modelscited by 639
  4. 2023Llemma: An Open Language Model For Mathematicscited by 385
  5. 2024Retrieval-Augmented Generation for AI-Generated Content: A Surveycited by 352
  6. 2023MINT: Evaluating LLMs in Multi-turn Interaction with Tools and Language Feedbackcited by 293
  7. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  8. 2024ArCHer: Training Language Model Agents via Hierarchical Multi-Turn RLcited by 212
  9. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  10. 2024A Survey on Recent Advances in LLM-Based Multi-turn Dialogue Systemscited by 170
  11. 2024Recursive Introspection: Teaching Language Model Agents How to Self-Improvecited by 162
  12. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
38 more
  1. 2024BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrievalcited by 153
  2. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  3. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  4. 2024Exploring Large Language Model based Intelligent Agents: Definitions, Methods, and Prospectscited by 130
  5. 2025LLM Post-Training: A Deep Dive into Reasoning Large Language Modelscited by 129
  6. 2024ChartX & ChartVLM: A Versatile Benchmark and Foundation Model for Complicated Chart Reasoningcited by 127
  7. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  8. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  9. 2024LLM-SR: Scientific Equation Discovery via Programming with Large Language Modelscited by 117
  10. 2024KAN 2.0: Kolmogorov-Arnold Networks Meet Sciencecited by 116
  11. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  12. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  13. 2023Let's reward step by step: Step-Level reward model as the Navigators for Reasoningcited by 96
  14. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  15. 2023Cumulative Reasoning with Large Language Modelscited by 94
  16. 2024Chain of Ideas: Revolutionizing Research Via Novel Idea Development with LLM Agentscited by 94
  17. 2025Pass@K Policy Optimization: Solving Harder Reinforcement Learning Problemscited by 83
  18. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  19. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  20. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  21. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  22. 2024Reliable, Adaptable, and Attributable Language Models with Retrievalcited by 73
  23. 2024SynCode: LLM Generation with Grammar Augmentationcited by 66
  24. 2024StateFlow: Enhancing LLM Task-Solving through State-Driven Workflowscited by 65
  25. 2024Retrieval Augmented Generation (RAG) and Beyond: A Comprehensive Survey on How to Make your LLMs use External Data More Wiselycited by 65
  26. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  27. 2025Evaluating Step-by-step Reasoning Traces: A Surveycited by 62
  28. 2023Guiding Language Model Reasoning with Planning Tokenscited by 58
  29. 2024SelfDefend: LLMs Can Defend Themselves against Jailbreaking in a Practical Mannercited by 57
  30. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  31. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  32. 2025ACE: A Security Architecture for LLM-Integrated App Systemscited by 52
  33. 2025A Survey on Large Language Models for Mathematical Reasoningcited by 52
  34. 2024The Limits of Inference Scaling Through Resamplingcited by 51
  35. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  36. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  37. 2024LLaMoCo: Instruction Tuning of Large Language Models for Optimization Code Generationcited by 45
  38. 2024Process-Driven Autoformalization in Lean 4cited by 45

50 most cited of 414 All 414 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
  2. 2025LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
  3. 2025LemmaHead: RAG Assisted Proof Generation Using Large Language Models
  4. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
  5. 2025A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
  6. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  7. 2025Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
  8. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification