Fetching the paper…
Reading the bibliography…
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.
Isabelle a Generic Theorem Prover
L. C. Paulson · 1994
Earlier work this paper cites.
The Coq proof assistant reference manual
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 · 1999
Earlier work this paper cites.
Recent advances in hierarchical reinforcement learning
A. G. Barto and S. Mahadevan · 2003
Earlier work this paper cites.
Proximal policy optimization algorithms
J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov · 2017
Earlier work this paper cites.
Data-efficient hierarchical reinforcement learning
O. Nachum, S. S. Gu, H. Lee, and S. Levine · 2018
Earlier work this paper cites.
Generative language modeling for automated theorem proving
S. Polu and I. Sutskever · 2020
Earlier work this paper cites.
Measuring mathematical problem solving with the MATH dataset
D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt · 2021
Earlier work this paper cites.
The Lean 4 theorem prover and programming language
L. d. Moura and S. Ullrich · 2021
Earlier work this paper cites.
Intelligent problem-solving as integrated hierarchical reinforcement learning
M. Eppe, C. Gumbsch, M. Kerzel, P. D. Nguyen, M. V. Butz, and S. Wermter · 2022
Earlier work this paper cites.
Hypertree proof search for neural theorem proving
G. Lample, M.-A. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, A. Rodriguez, and T. Lacroix · 2022
Earlier work this paper cites.
miniF2F: a cross-system benchmark for formal olympiad-level mathematics
K. Zheng, J. M. Han, and S. Polu · 2022
Earlier work this paper cites.
ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad · 2023
Earlier work this paper cites.
Draft, sketch, and prove: Guiding formal theorem provers with informal proofs
A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu · 2023
Cited alongside, same era.
Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving
X. Zhao, W. Li, and L. Kong · 2023
Cited alongside, same era.
AI achieves silver-medal standard solving international mathematical olympiad problems
DeepMind · 2024
Cited alongside, same era.
Deepseek-v3 technical report, 2024
DeepSeek-AI · 2024
Cited alongside, same era.
Formal theorem proving by rewarding llms to decompose proofs hierarchically
K. Dong, A. Mahankali, and T. Ma · 2024
Cited alongside, same era.
Lean workbook: A large-scale lean problem set formalized from natural language math problems
H. Ying, Z. Wu, Y. Geng, J. Wang, D. Lin, and K. Chen · 2024
Later among the works it cites.
Subgoalxl: Subgoal-based expert learning for theorem proving
X. Zhao, L. Zheng, H. Bo, C. Hu, U. Thakker, and L. Kong · 2024
Later among the works it cites.
Lyra: Orchestrating dual correction in automated theorem proving
C. Zheng, H. Wang, E. Xie, Z. Liu, J. Sun, H. Xin, J. Shen, Z. Li, and Y. Li · 2024
Later among the works it cites.
Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning, 2025
DeepSeek-AI · 2025
Closest in time.
STP: Self-play llm theorem provers with iterative conjecturing and proving
K. Dong and T. Ma · 2025
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
A. Jaech, A. Kalai, A. Lerer, A. Richardson, A. El-Kishky, A. Low, A. Helyar, A. Madry, A. Beutel, A. Carney, et al · 2024
Cited alongside, same era.
Y. Li, D. Du, L. Song, C. Li, W. Wang, T. Yang, and H. Mi · 2024
Cited alongside, same era.
DeepSeekMath: Pushing the limits of mathematical reasoning in open language models
Z. Shao, P. Wang, Q. Zhu, R. Xu, J. Song, M. Zhang, Y. Li, Y. Wu, and D. Guo · 2024
Cited alongside, same era.
PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition
G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri · 2024
Cited alongside, same era.
Z. Wu, S. Huang, Z. Zhou, H. Ying, J. Wang, D. Lin, and K. Chen · 2024
Cited alongside, same era.
Formal mathematical reasoning: A new frontier in AI
K. Yang, G. Poesia, J. He, W. Li, K. Lauter, S. Chaudhuri, and D. Song · 2024
Cited alongside, same era.
Proving theorems recursively
H. Wang, H. Xin, Z. Liu, W. Li, Y. Huang, J. Lu, Y. Zhicheng, J. Tang, J. Yin, Z. Li, et al
Cited in the paper.
Closest in time.
Goedel-Prover: A frontier model for open-source automated theorem proving
Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, et al · 2025
Closest in time.
CombiBench: Benchmarking llm capability for combinatorial mathematics
J. Liu, X. Lin, J. Bayer, Y. Dillies, W. Jiang, X. Liang, R. Soletskyi, H. Wang, Y. Xie, B. Xiong, et al · 2025
Closest in time.
Kimina-Prover Preview: Towards large formal reasoning models with reinforcement learning
H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, et al · 2025
Closest in time.
BFS-Prover: Scalable best-first tree search for llm-based automatic theorem proving
R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen · 2025
Closest in time.
Formalmath: Benchmarking formal mathematical reasoning of large language models
Z. Yu, R. Peng, K. Ding, Y. Li, Z. Peng, M. Liu, Y. Zhang, Z. Yuan, H. Xin, W. Huang, et al · 2025
Closest in time.
Leanabell-prover: Posttraining scaling in formal reasoning
J. Zhang, Q. Wang, X. Ji, Y. Liu, Y. Yue, F. Zhang, D. Zhang, G. Zhou, and K. Gai · 2025
Closest in time.