DeepSeek Unveils DeepSeek-Prover-V2: Advancing Neural Theorem Proving with Recursive Proof Search and a New Benchmark

DeepSeek AI has released DeepSeek-Prover-V2, an open-source large language model specifically designed for Lean 4 theorem proving. The model employs recursive proof search methodology and uses DeepSeek-V3 for training data generation with reinforcement learning, achieving top performance results on the MiniF2F benchmark.

• →DeepSeek AI launched DeepSeek-Prover-V2 as an open-source LLM specialized for mathematical theorem proving in Lean 4.
• →The model utilizes recursive proof search techniques combined with reinforcement learning for enhanced performance.
• →DeepSeek-V3 is used to generate training data for the new theorem proving model.
• →The system achieved top results on the MiniF2F benchmark, demonstrating strong mathematical reasoning capabilities.
• →The open-source release makes advanced neural theorem proving more accessible to the research community.