---
title: "DeepSeek-Prover-V2 — Ren 2025"
description: "Lean 4 accepts only proofs where every step is fully rigorous and machine-checkable, while LLMs tend to reason loosely and informally."
authors: ["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", "Chong Ruan"]
year: 2025
venue: "arXiv:2504.21801"
source: "https://arxiv.org/abs/2504.21801"
doi: "10.48550/arxiv.2504.21801"
arxiv: "2504.21801"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)

[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/) / DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

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

**Authors:** [Z. Z. Ren](https://md.research.elamur.ai/free/en/authors/z-z-ren/), [Zhihong Shao](https://md.research.elamur.ai/free/en/authors/zhihong-shao/), [Junxiao Song](https://md.research.elamur.ai/free/en/authors/junxiao-song/), [Huajian Xin](https://md.research.elamur.ai/free/en/authors/huajian-xin/), [Haocheng Wang](https://md.research.elamur.ai/free/en/authors/haocheng-wang/), [Wanjia Zhao](https://md.research.elamur.ai/free/en/authors/wanjia-zhao/), [Liyue Zhang](https://md.research.elamur.ai/free/en/authors/liyue-zhang/), Zhe Fu, [Qihao Zhu](https://md.research.elamur.ai/free/en/authors/qihao-zhu/), [Dejian Yang](https://md.research.elamur.ai/free/en/authors/dejian-yang/), Z. F. Wu, [Zhibin Gou](https://md.research.elamur.ai/free/en/authors/zhibin-gou/) et al. (18 authors) · **Year:** 2025 · **Venue:** arXiv:2504.21801 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

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

**Citations:** 3 citations (OpenAlex, 2026-10-14) · 117 in our library, of the 140884 papers whose bibliographies we read

## Summary
Lean 4 accepts only proofs where every step is fully rigorous and machine-checkable, while LLMs tend to reason loosely and informally. This paper tries to connect the two. DeepSeek-AI builds training data with a recursive pipeline. First, DeepSeek-V3 works through a theorem in natural language. It then turns its plan into a Lean skeleton in which each intermediate `have` step is left as a `sorry` subgoal. A smaller 7B prover fills in each subgoal. The finished formal proof is then joined with DeepSeek-V3's reasoning trace to make cold-start examples. The decomposed subgoals are also turned into extra lemma statements, which form a curriculum of tasks that get harder over time. Reinforcement learning on top of this cold start produces the open-source DeepSeek-Prover-V2-671B and a 7B variant. The large model reaches a new state of the art on MiniF2F-test and also does well on college-level benchmarks. The authors release ProverBench as well. On recent AIME problems, the model's formal proofs come close to DeepSeek-V3's informal answer-finding, which suggests the gap between informal and formal reasoning is getting smaller.

## Key points
- **Results for DeepSeek-Prover-V2-671B:** on MiniF2F-test it scores 82.4% at Pass@32 and 88.9% at Pass@8192. It solves 37.1% of ProofNet-test at Pass@1024 and 47 of 658 PutnamBench problems.
- **Pipeline design:** DeepSeek-V3 does both the subgoal decomposition and the Lean formalization. The cheaper 7B model handles the proof search for each subgoal, which keeps compute costs down. Subgoals become lemmas in two ways: either they replace the original goal, or they also take earlier subgoals as premises. The second form is used for recursive solving, and both forms feed the curriculum.
- **ProverBench (325 problems):** 15 problems come from AIME 24 and 25, limited to number theory and algebra; geometry, combinatorics and counting problems were left out. The other 310 come from textbooks and tutorials and cover nine areas, such as calculus (90 problems), linear algebra (50) and abstract algebra (40).
- **AIME comparison:** given the correct answers, DeepSeek-Prover-V2-671B builds valid Lean proofs for 6 of the 15 problems. DeepSeek-V3-0324 solves 8 of 15 informally using Maj@16.
- **Release and baselines:** the models are on GitHub (deepseek-ai/DeepSeek-Prover-V2). They are compared against Kimina-Prover-Preview, BFS-Prover, STP and Goedel-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.*

Fields: [Mathematics & statistics](https://md.research.elamur.ai/free/en/shelves/mathematics/)

Topics: [Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/)

## Cite

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

```bibtex
@misc{ren2025deepseek,
  title = {{DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition}},
  author = {Ren, Z. Z. and Shao, Zhihong and Song, Junxiao and Xin, Huajian and Wang, Haocheng and Zhao, Wanjia and Zhang, Liyue and Fu, Zhe and Zhu, Qihao and Yang, Dejian and Wu, Z. F. and Gou, Zhibin and Ma, Shirong and Tang, Hongxuan and Liu, Yuxuan and Gao, Wenjun and Guo, Daya and Ruan, Chong},
  year = {2025},
  doi = {10.48550/arxiv.2504.21801},
  eprint = {2504.21801},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2504.21801}
}
```

- [← previous The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search](https://md.research.elamur.ai/free/en/papers/yamada-2025-ai-scientist-v2-workshop/)
- [next → L1: Controlling How Long A Reasoning Model Thinks With Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/aggarwal-2025-l1-controlling-long-reasoning-model/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/)

## References

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

1. Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023. [find](https://scholar.google.com/scholar?q=Z%2E+Azerbayev%2C+B%2E+Piotrowski%2C+H%2E+Schoelkopf%2C+E%2E+W%2E+Ayers%2C+D%2E+Radev%2C+and+J%2E+Avigad%2E+ProofNet%3A+Autoformalizing+and+formally+proving+undergraduate%2Dlevel+mathematics%2E+arXiv+preprint+arXiv%3A2302%2E12433%2C+2023%2E) [our card](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/)
2. B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliâtre, E. Giménez, H. Herbelin, et al. The Coq proof assistant reference manual. INRIA, version, 6(11):17–21, 1999. [find](https://scholar.google.com/scholar?q=B%2E+Barras%2C+S%2E+Boutin%2C+C%2E+Cornes%2C+J%2E+Courant%2C+Y%2E+Coscoy%2C+D%2E+Delahaye%2C+D%2E+de+Rauglaudre%2C+J%2E%2DC%2E+Filli%C3%A2tre%2C+E%2E+Gim%C3%A9nez%2C+H%2E+Herbelin%2C+et+al%2E+The+Coq+proof+assistant+reference+manual%2E+INRIA%2C+version%2C+6%2811%29%3A)
3. A. G. Barto and S. Mahadevan. Recent advances in hierarchical reinforcement learning. Discrete event dynamic systems, 13:341–379, 2003. [find](https://scholar.google.com/scholar?q=A%2E+G%2E+Barto+and+S%2E+Mahadevan%2E+Recent+advances+in+hierarchical+reinforcement+learning%2E+Discrete+event+dynamic+systems%2C+13%3A341%E2%80%93379%2C+2003%2E)
4. DeepMind. AI achieves silver-medal standard solving international mathematical olympiad problems. [https://deepmind.google/discover/blog/ai-solves-imo-problems-a](https://deepmind.google/discover/blog/ai-solves-imo-problems-a) t-silver-medal-level/ , 2024. [↗](https://deepmind.google/discover/blog/ai-solves-imo-problems-a)
5. DeepSeek-AI. Deepseek-v3 technical report, 2024. URL https://arxiv.org/abs/2412.194 37 . [↗](https://arxiv.org/abs/2412.194)
6. DeepSeek-AI. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning, 2025. URL https://arxiv.org/abs/2501.12948 . [↗](https://arxiv.org/abs/2501.12948) [our card](https://md.research.elamur.ai/free/en/papers/deepseek-2025-ai-deepseek-r1-incentivizing-reasoning-capability/)
7. K. Dong and T. 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=K%2E+Dong+and+T%2E+Ma%2E+STP%3A+Self%2Dplay+llm+theorem+provers+with+iterative+conjecturing+and+proving%2E+arXiv+preprint+arXiv%3A2502%2E00212%2C+2025%2E)
8. K. Dong, A. Mahankali, and T. Ma. Formal theorem proving by rewarding llms to decompose proofs hierarchically. arXiv preprint arXiv:2411.01829, 2024. — [arXiv:2411.01829](https://arxiv.org/abs/2411.01829) [find](https://scholar.google.com/scholar?q=K%2E+Dong%2C+A%2E+Mahankali%2C+and+T%2E+Ma%2E+Formal+theorem+proving+by+rewarding+llms+to+decompose+proofs+hierarchically%2E+arXiv+preprint+arXiv%3A2411%2E01829%2C+2024%2E+%E2%80%94+%5BarXiv%3A2411%2E01829%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2411%2E01)
9. M. Eppe, C. Gumbsch, M. Kerzel, P. D. Nguyen, M. V. Butz, and S. Wermter. Intelligent problem-solving as integrated hierarchical reinforcement learning. Nature Machine Intelligence, 4(1): 11–20, 2022. [find](https://scholar.google.com/scholar?q=M%2E+Eppe%2C+C%2E+Gumbsch%2C+M%2E+Kerzel%2C+P%2E+D%2E+Nguyen%2C+M%2E+V%2E+Butz%2C+and+S%2E+Wermter%2E+Intelligent+problem%2Dsolving+as+integrated+hierarchical+reinforcement+learning%2E+Nature+Machine+Intelligence%2C+4%281%29%3A+11%E2%80%9320%2C+2022%2E)
10. D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2), 2021. [find](https://scholar.google.com/scholar?q=D%2E+Hendrycks%2C+C%2E+Burns%2C+S%2E+Kadavath%2C+A%2E+Arora%2C+S%2E+Basart%2C+E%2E+Tang%2C+D%2E+Song%2C+and+J%2E+Steinhardt%2E+Measuring+mathematical+problem+solving+with+the+MATH+dataset%2E+In+Thirty%2Dfifth+Conference+on+Neural+Inform) [our card](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/)
11. A. Jaech, A. Kalai, A. Lerer, A. Richardson, A. El-Kishky, A. Low, A. Helyar, A. Madry, A. Beutel, A. Carney, et al. Openai o1 system card. arXiv preprint arXiv:2412.16720, 2024. [find](https://scholar.google.com/scholar?q=A%2E+Jaech%2C+A%2E+Kalai%2C+A%2E+Lerer%2C+A%2E+Richardson%2C+A%2E+El%2DKishky%2C+A%2E+Low%2C+A%2E+Helyar%2C+A%2E+Madry%2C+A%2E+Beutel%2C+A%2E+Carney%2C+et+al%2E+Openai+o1+system+card%2E+arXiv+preprint+arXiv%3A2412%2E16720%2C+2024%2E) [our card](https://md.research.elamur.ai/free/en/papers/openai-2024-openai-o1-system-card/)
12. A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023. [find](https://scholar.google.com/scholar?q=A%2E+Q%2E+Jiang%2C+S%2E+Welleck%2C+J%2E+P%2E+Zhou%2C+T%2E+Lacroix%2C+J%2E+Liu%2C+W%2E+Li%2C+M%2E+Jamnik%2C+G%2E+Lample%2C+and+Y%2E+Wu%2E+Draft%2C+sketch%2C+and+prove%3A+Guiding+formal+theorem+provers+with+informal+proofs%2E+In+The+Eleventh+Internat) [our card](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/)
13. G. Lample, M.-A. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, A. Rodriguez, and T. Lacroix. Hypertree proof search for neural theorem proving. In Proceedings of the 36th International Conference on Neural Information Processing Systems, pages 26337–26349, 2022. [find](https://scholar.google.com/scholar?q=G%2E+Lample%2C+M%2E%2DA%2E+Lachaux%2C+T%2E+Lavril%2C+X%2E+Martinet%2C+A%2E+Hayat%2C+G%2E+Ebner%2C+A%2E+Rodriguez%2C+and+T%2E+Lacroix%2E+Hypertree+proof+search+for+neural+theorem+proving%2E+In+Proceedings+of+the+36th+International+Conferen) [our card](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/)
14. Y. Li, D. Du, L. Song, C. Li, W. Wang, T. Yang, and H. Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024. [find](https://scholar.google.com/scholar?q=Y%2E+Li%2C+D%2E+Du%2C+L%2E+Song%2C+C%2E+Li%2C+W%2E+Wang%2C+T%2E+Yang%2C+and+H%2E+Mi%2E+Hunyuanprover%3A+A+scalable+data+synthesis+framework+and+guided+tree+search+for+automated+theorem+proving%2E+arXiv+preprint+arXiv%3A2412%2E20735%2C+202)
15. Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, et al. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025. [find](https://scholar.google.com/scholar?q=Y%2E+Lin%2C+S%2E+Tang%2C+B%2E+Lyu%2C+J%2E+Wu%2C+H%2E+Lin%2C+K%2E+Yang%2C+J%2E+Li%2C+M%2E+Xia%2C+D%2E+Chen%2C+S%2E+Arora%2C+et+al%2E+Goedel%2DProver%3A+A+frontier+model+for+open%2Dsource+automated+theorem+proving%2E+arXiv+preprint+arXiv%3A2502%2E07640%2C+20)
16. J. Liu, X. Lin, J. Bayer, Y. Dillies, W. Jiang, X. Liang, R. Soletskyi, H. Wang, Y. Xie, B. Xiong, et al. CombiBench: Benchmarking llm capability for combinatorial mathematics. arXiv preprint arXiv:2505.03171, 2025. [find](https://scholar.google.com/scholar?q=J%2E+Liu%2C+X%2E+Lin%2C+J%2E+Bayer%2C+Y%2E+Dillies%2C+W%2E+Jiang%2C+X%2E+Liang%2C+R%2E+Soletskyi%2C+H%2E+Wang%2C+Y%2E+Xie%2C+B%2E+Xiong%2C+et+al%2E+CombiBench%3A+Benchmarking+llm+capability+for+combinatorial+mathematics%2E+arXiv+preprint+arXiv%3A25)
17. L. d. Moura and S. Ullrich. 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, pages 625–635. [find](https://scholar.google.com/scholar?q=L%2E+d%2E+Moura+and+S%2E+Ullrich%2E+The+Lean+4+theorem+prover+and+programming+language%2E+In+Automated+Deduction%E2%80%93CADE+28%3A+28th+International+Conference+on+Automated+Deduction%2C+Virtual+Event%2C+July+12%E2%80%9315%2C+2021%2C+P) [our card](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
18. O. Nachum, S. S. Gu, H. Lee, and S. Levine. Data-efficient hierarchical reinforcement learning. Advances in neural information processing systems, 31, 2018. [find](https://scholar.google.com/scholar?q=O%2E+Nachum%2C+S%2E+S%2E+Gu%2C+H%2E+Lee%2C+and+S%2E+Levine%2E+Data%2Defficient+hierarchical+reinforcement+learning%2E+Advances+in+neural+information+processing+systems%2C+31%2C+2018%2E)
19. L. C. Paulson. Isabelle a Generic Theorem Prover. Springer Verlag, 1994. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson%2E+Isabelle+a+Generic+Theorem+Prover%2E+Springer+Verlag%2C+1994%2E)
20. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. [find](https://scholar.google.com/scholar?q=S%2E+Polu+and+I%2E+Sutskever%2E+Generative+language+modeling+for+automated+theorem+proving%2E+arXiv+preprint+arXiv%3A2009%2E03393%2C+2020%2E) [our card](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/)
21. J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347, 2017. [find](https://scholar.google.com/scholar?q=J%2E+Schulman%2C+F%2E+Wolski%2C+P%2E+Dhariwal%2C+A%2E+Radford%2C+and+O%2E+Klimov%2E+Proximal+policy+optimization+algorithms%2E+arXiv+preprint+arXiv%3A1707%2E06347%2C+2017%2E)
22. Z. Shao, P. Wang, Q. Zhu, R. Xu, J. Song, M. Zhang, Y. Li, Y. Wu, and D. Guo. DeepSeekMath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024. [find](https://scholar.google.com/scholar?q=Z%2E+Shao%2C+P%2E+Wang%2C+Q%2E+Zhu%2C+R%2E+Xu%2C+J%2E+Song%2C+M%2E+Zhang%2C+Y%2E+Li%2C+Y%2E+Wu%2C+and+D%2E+Guo%2E+DeepSeekMath%3A+Pushing+the+limits+of+mathematical+reasoning+in+open+language+models%2E+arXiv+preprint+arXiv%3A2402%2E03300%2C+2024%2E) [our card](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/)
23. G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. [find](https://scholar.google.com/scholar?q=G%2E+Tsoukalas%2C+J%2E+Lee%2C+J%2E+Jennings%2C+J%2E+Xin%2C+M%2E+Ding%2C+M%2E+Jennings%2C+A%2E+Thakur%2C+and+S%2E+Chaudhuri%2E+PutnamBench%3A+Evaluating+neural+theorem%2Dprovers+on+the+putnam+mathematical+competition%2E+In+The+Thirty%2Deight)
24. H. Wang, H. Xin, Z. Liu, W. Li, Y. Huang, J. Lu, Y. Zhicheng, J. Tang, J. Yin, Z. Li, et al. Proving theorems recursively. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024a. [find](https://scholar.google.com/scholar?q=H%2E+Wang%2C+H%2E+Xin%2C+Z%2E+Liu%2C+W%2E+Li%2C+Y%2E+Huang%2C+J%2E+Lu%2C+Y%2E+Zhicheng%2C+J%2E+Tang%2C+J%2E+Yin%2C+Z%2E+Li%2C+et+al%2E+Proving+theorems+recursively%2E+In+The+Thirty%2Deighth+Annual+Conference+on+Neural+Information+Processing+Syste)
25. H. Wang, H. Xin, C. Zheng, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin, et al. Lego-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024b. [find](https://scholar.google.com/scholar?q=H%2E+Wang%2C+H%2E+Xin%2C+C%2E+Zheng%2C+Z%2E+Liu%2C+Q%2E+Cao%2C+Y%2E+Huang%2C+J%2E+Xiong%2C+H%2E+Shi%2C+E%2E+Xie%2C+J%2E+Yin%2C+et+al%2E+Lego%2Dprover%3A+Neural+theorem+proving+with+growing+libraries%2E+In+The+Twelfth+International+Conference+on+Lea)
26. H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, et al. Kimina-Prover Preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025. [find](https://scholar.google.com/scholar?q=H%2E+Wang%2C+M%2E+Unsal%2C+X%2E+Lin%2C+M%2E+Baksys%2C+J%2E+Liu%2C+M%2E+D%2E+Santos%2C+F%2E+Sung%2C+M%2E+Vinyes%2C+Z%2E+Ying%2C+Z%2E+Zhu%2C+et+al%2E+Kimina%2DProver+Preview%3A+Towards+large+formal+reasoning+models+with+reinforcement+learning%2E+arXiv+)
27. Z. Wu, S. Huang, Z. Zhou, H. Ying, J. Wang, D. Lin, and K. Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024. [find](https://scholar.google.com/scholar?q=Z%2E+Wu%2C+S%2E+Huang%2C+Z%2E+Zhou%2C+H%2E+Ying%2C+J%2E+Wang%2C+D%2E+Lin%2C+and+K%2E+Chen%2E+Internlm2%2E+5%2Dstepprover%3A+Advancing+automated+theorem+proving+via+expert+iteration+on+large%2Dscale+lean+problems%2E+arXiv+preprint+arXiv%3A24)
28. H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. DeepSeek-Prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a. [find](https://scholar.google.com/scholar?q=H%2E+Xin%2C+D%2E+Guo%2C+Z%2E+Shao%2C+Z%2E+Ren%2C+Q%2E+Zhu%2C+B%2E+Liu%2C+C%2E+Ruan%2C+W%2E+Li%2C+and+X%2E+Liang%2E+DeepSeek%2DProver%3A+Advancing+theorem+proving+in+llms+through+large%2Dscale+synthetic+data%2E+arXiv+preprint+arXiv%3A2405%2E14333%2C+2) [our card](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/)
29. H. Xin, Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, et al. DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024b. [find](https://scholar.google.com/scholar?q=H%2E+Xin%2C+Z%2E+Ren%2C+J%2E+Song%2C+Z%2E+Shao%2C+W%2E+Zhao%2C+H%2E+Wang%2C+B%2E+Liu%2C+L%2E+Zhang%2C+X%2E+Lu%2C+Q%2E+Du%2C+et+al%2E+DeepSeek%2DProver%2DV1%2E5%3A+Harnessing+proof+assistant+feedback+for+reinforcement+learning+and+monte%2Dcarlo+tree+sea) [our card](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
30. R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. 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=R%2E+Xin%2C+C%2E+Xi%2C+J%2E+Yang%2C+F%2E+Chen%2C+H%2E+Wu%2C+X%2E+Xiao%2C+Y%2E+Sun%2C+S%2E+Zheng%2C+and+K%2E+Shen%2E+BFS%2DProver%3A+Scalable+best%2Dfirst+tree+search+for+llm%2Dbased+automatic+theorem+proving%2E+arXiv+preprint+arXiv%3A2502%2E03438%2C+20)
31. K. Yang, G. Poesia, J. He, W. Li, K. Lauter, S. Chaudhuri, and D. Song. Formal mathematical reasoning: A new frontier in AI. arXiv preprint arXiv:2412.16075, 2024. [find](https://scholar.google.com/scholar?q=K%2E+Yang%2C+G%2E+Poesia%2C+J%2E+He%2C+W%2E+Li%2C+K%2E+Lauter%2C+S%2E+Chaudhuri%2C+and+D%2E+Song%2E+Formal+mathematical+reasoning%3A+A+new+frontier+in+AI%2E+arXiv+preprint+arXiv%3A2412%2E16075%2C+2024%2E)
32. H. Ying, Z. Wu, Y. Geng, J. Wang, D. Lin, and K. Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. [find](https://scholar.google.com/scholar?q=H%2E+Ying%2C+Z%2E+Wu%2C+Y%2E+Geng%2C+J%2E+Wang%2C+D%2E+Lin%2C+and+K%2E+Chen%2E+Lean+workbook%3A+A+large%2Dscale+lean+problem+set+formalized+from+natural+language+math+problems%2E+In+The+Thirty%2Deight+Conference+on+Neural+Informatio)
33. Z. Yu, R. Peng, K. Ding, Y. Li, Z. Peng, M. Liu, Y. Zhang, Z. Yuan, H. Xin, W. Huang, et al. Formalmath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint arXiv:2505.02735, 2025. [find](https://scholar.google.com/scholar?q=Z%2E+Yu%2C+R%2E+Peng%2C+K%2E+Ding%2C+Y%2E+Li%2C+Z%2E+Peng%2C+M%2E+Liu%2C+Y%2E+Zhang%2C+Z%2E+Yuan%2C+H%2E+Xin%2C+W%2E+Huang%2C+et+al%2E+Formalmath%3A+Benchmarking+formal+mathematical+reasoning+of+large+language+models%2E+arXiv+preprint+arXiv%3A2505%2E)
34. J. Zhang, Q. Wang, X. Ji, Y. Liu, Y. Yue, F. Zhang, D. Zhang, G. Zhou, and K. Gai. Leanabell-prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025. [find](https://scholar.google.com/scholar?q=J%2E+Zhang%2C+Q%2E+Wang%2C+X%2E+Ji%2C+Y%2E+Liu%2C+Y%2E+Yue%2C+F%2E+Zhang%2C+D%2E+Zhang%2C+G%2E+Zhou%2C+and+K%2E+Gai%2E+Leanabell%2Dprover%3A+Posttraining+scaling+in+formal+reasoning%2E+arXiv+preprint+arXiv%3A2504%2E06122%2C+2025%2E)
35. X. Zhao, W. Li, and L. Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.16366, 2023. [find](https://scholar.google.com/scholar?q=X%2E+Zhao%2C+W%2E+Li%2C+and+L%2E+Kong%2E+Decomposing+the+enigma%3A+Subgoal%2Dbased+demonstration+learning+for+formal+theorem+proving%2E+arXiv+preprint+arXiv%3A2305%2E16366%2C+2023%2E)
36. X. Zhao, L. Zheng, H. Bo, C. Hu, U. Thakker, and L. Kong. Subgoalxl: Subgoal-based expert learning for theorem proving. arXiv preprint arXiv:2408.11172, 2024. [find](https://scholar.google.com/scholar?q=X%2E+Zhao%2C+L%2E+Zheng%2C+H%2E+Bo%2C+C%2E+Hu%2C+U%2E+Thakker%2C+and+L%2E+Kong%2E+Subgoalxl%3A+Subgoal%2Dbased+expert+learning+for+theorem+proving%2E+arXiv+preprint+arXiv%3A2408%2E11172%2C+2024%2E)
37. C. Zheng, H. Wang, E. Xie, Z. Liu, J. Sun, H. Xin, J. Shen, Z. Li, and Y. Li. Lyra: Orchestrating dual correction in automated theorem proving. Transactions on Machine Learning Research, 2024. [find](https://scholar.google.com/scholar?q=C%2E+Zheng%2C+H%2E+Wang%2C+E%2E+Xie%2C+Z%2E+Liu%2C+J%2E+Sun%2C+H%2E+Xin%2C+J%2E+Shen%2C+Z%2E+Li%2C+and+Y%2E+Li%2E+Lyra%3A+Orchestrating+dual+correction+in+automated+theorem+proving%2E+Transactions+on+Machine+Learning+Research%2C+2024%2E)
38. K. Zheng, J. M. Han, and S. Polu. miniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. [find](https://scholar.google.com/scholar?q=K%2E+Zheng%2C+J%2E+M%2E+Han%2C+and+S%2E+Polu%2E+miniF2F%3A+a+cross%2Dsystem+benchmark+for+formal+olympiad%2Dlevel+mathematics%2E+In+International+Conference+on+Learning+Representations%2C+2022%2E) [our card](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/)
39. A. Examples of Non-CoT and CoT Prompting for Proof Generation [find](https://scholar.google.com/scholar?q=A%2E+Examples+of+Non%2DCoT+and+CoT+Prompting+for+Proof+Generation)