mlsanityData to 7 Oct 2026

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

arXiv 2405.14333 ↗First posted 23 May 2024cs.AIcited by 225

On the map: Synthetic data and self-improvement for LLMs → Self-play RL for reasoning

Abstract (arXiv)

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.

Key facts. Cited by 225 papers in the map (data through 7 Oct 2026). Placed in Self-play RL for reasoning, one of 13 directions in Synthetic data and self-improvement for LLMs. Builds on 23 of its 35 references that are in the map. First posted on arXiv 23 May 2024.

Builds on

23 of 35 references.

References · 23

  1. 2017Attention Is All You Needcited by 59,932
  2. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2023Llemma: An Open Language Model For Mathematicscited by 385
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  8. 2022Autoformalization with Large Language Modelscited by 252
  9. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  10. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  11. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  12. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
11 more
  1. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  2. 2018Reinforcement Learning of Theorem Provingcited by 69
  3. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  4. 2017Deep Network Guided Proof Searchcited by 47
  5. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  6. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  7. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  8. 2023Multilingual Mathematical Autoformalizationcited by 38
  9. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  10. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  11. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 24; 2025: 107; 2026: 94.

225 papers.

Sort:

By area:

  1. 2025s1: Simple test-time scalingcited by 1,311
  2. 2025rStar-Math: Small LLMs Can Master Math Reasoning with Self-Evolved Deep Thinkingcited by 308
  3. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  4. 2024Step-DPO: Step-wise Preference Optimization for Long-chain Reasoning of LLMscited by 265
  5. 2025AReaL: A Large-Scale Asynchronous Reinforcement Learning System for Language Reasoningcited by 234
  6. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  7. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  8. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  9. 2025WebShaper: Agentically Data Synthesizing via Information-Seeking Formalizationcited by 118
  10. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  11. 2025A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systemscited by 108
  12. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
38 more
  1. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  2. 2024Interpretable Contrastive Monte Carlo Tree Search Reasoningcited by 62
  3. 2024A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challengescited by 55
  4. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  5. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  6. 2024The Limits of Inference Scaling Through Resamplingcited by 51
  7. 2025Agentic Reward Modeling: Integrating Human Preferences with Verifiable Correctness Signals for Reliable Reward Systemscited by 49
  8. 2024GraphArena: Evaluating and Exploring Large Language Models on Graph Computationcited by 48
  9. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  10. 2025Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlocited by 45
  11. 2024A Survey on Data Synthesis and Augmentation for Large Language Modelscited by 40
  12. 2025Harnessing the Reasoning Economy: A Survey of Efficient Reasoning for Large Language Modelscited by 35
  13. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  14. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  15. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  16. 2025Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoningcited by 33
  17. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 32
  18. 2025Two Heads are Better Than One: Test-time Scaling of Multi-agent Collaborative Reasoningcited by 29
  19. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 28
  20. 2025R2R: Efficiently Navigating Divergent Reasoning Paths with Small-Large Model Token Routingcited by 28
  21. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  22. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  23. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  24. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  25. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  26. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
  27. 2025To Backtrack or Not to Backtrack: When Sequential Search Limits Model Reasoningcited by 24
  28. 2025PDE-Controller: LLMs for Autoformalization and Reasoning of PDEscited by 23
  29. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  30. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learningcited by 23
  31. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  32. 2025O2-Searcher: A Searching-based Agent Model for Open-Domain Open-Ended Question Answeringcited by 22
  33. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  34. 2025Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Samplingcited by 20
  35. 2024TPO: Aligning Large Language Models with Multi-branch & Multi-step Preference Treescited by 19
  36. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  37. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 18
  38. 2025TinyV: Reducing False Negatives in Verification Improves RL for LLM Reasoningcited by 18

50 most cited of 225 All 225 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
  2. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
  3. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
  4. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  5. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  6. 2024Lean-STaR: Learning to Interleave Thinking and Proving
  7. 2025LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
  8. 2025DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning