mlsanityData to 7 Oct 2026

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

arXiv 2504.21801 ↗First posted 30 Apr 2025cs.CL cs.AIcited by 270

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing.

Key facts. Cited by 270 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 20 of its 38 references that are in the map. First posted on arXiv 30 Apr 2025.

Builds on

20 of 38 references.

Closest ancestors · 8

Same direction, newest first

  1. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning15 Apr
  2. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoning8 Apr
  3. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan
  4. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving30 Dec
  5. 2024Formal Mathematical Reasoning: A New Frontier in AI20 Dec
  6. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically4 Nov
  7. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models5 Feb
  8. 2020Generative Language Modeling for Automated Theorem Proving7 Sep

Other references · 12

  1. 2017Proximal Policy Optimization Algorithmscited by 14,441
  2. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,146
  3. 2024OpenAI o1 System Cardcited by 1,220
  4. 2024DeepSeek-V3 Technical Reportcited by 724
  5. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  6. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  7. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  8. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  9. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  10. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  11. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  12. 2024SubgoalXL: Subgoal-based Expert Learning for Theorem Provingcited by 11

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 107; 2026: 163.

270 papers.

Sort:

By area:

  1. 2025Absolute Zero: Reinforced Self-play Reasoning with Zero Datacited by 323
  2. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 195
  3. 2025A Survey of Reinforcement Learning for Large Reasoning Modelscited by 175
  4. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  5. 2025WebShaper: Agentically Data Synthesizing via Information-Seeking Formalizationcited by 118
  6. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  7. 2025DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoningcited by 84
  8. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  9. 2025Breaking the Exploration Bottleneck: Rubric-Scaffolded Reinforcement Learning for General LLM Reasoningcited by 56
  10. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  11. 2025LEXam: Benchmarking Legal Reasoning on 340 Law Examscited by 52
  12. 2025DeepAnalyze: Agentic Large Language Models for Autonomous Data Sciencecited by 49
38 more
  1. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  2. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  3. 2025Solver-Informed RL: Grounding Large Language Models for Authentic Optimization Modelingcited by 44
  4. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
  5. 2026Code as Agent Harnesscited by 40
  6. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  7. 2025VERINA: Benchmarking Verifiable Code Generationcited by 30
  8. 2025Scaling Reasoning, Losing Control: Evaluating Instruction Following in Large Reasoning Modelscited by 28
  9. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  10. 2025Dynamic Mixture of Curriculum LoRA Experts for Continual Multimodal Instruction Tuningcited by 27
  11. 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 27
  12. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  13. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  14. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  15. 2026Trust Region On-Policy Distillationcited by 26
  16. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learningcited by 23
  17. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
  18. 2025Get Experience from Practice: LLM Agents with Record & Replaycited by 22
  19. 2025HardTests: Synthesizing High-Quality Test Cases for LLM Codingcited by 22
  20. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  21. 2025Introducing LongCat-Flash-Thinking: A Technical Reportcited by 21
  22. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  23. 2025A Technical Survey of Reinforcement Learning Techniques for Large Language Modelscited by 19
  24. 2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 19
  25. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  26. 2025Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Modelscited by 18
  27. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  28. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  29. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
  30. 2025DisCO: Reinforcing Large Reasoning Models with Discriminative Constrained Optimizationcited by 16
  31. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 16
  32. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 15
  33. 2025Find Your Optimal Teacher: Personalized Data Synthesis via Router-Guided Multi-Teacher Distillationcited by 15
  34. 2025Sailing by the Stars: A Survey on Reward Models and Learning Strategies for Learning from Rewardscited by 14
  35. 2025L-MTP: Leap Multi-Token Prediction Beyond Adjacent Context for Large Language Modelscited by 14
  36. 2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 14
  37. 2025MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?cited by 13
  38. 2026ToolPRMBench: Evaluating and Advancing Process Reward Models for Tool-using Agentscited by 13

50 most cited of 270 All 270 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  2. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
  3. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
  4. 2025Theorem Prover as a Judge for Synthetic Data Generation
  5. 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
  6. 2025DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoning
  7. 2021Proof Artifact Co-training for Theorem Proving with Language Models
  8. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction