DeepSeek推出了新模型DeepSeek-Prover-V2，专注于数学定理证明，并在多项高难度基准测试中刷新了记录。在普特南测试上，Prover-V2解决了49道题，远超当前第一名的10道和未针对定理证明优化的DeepSeek-R1的1道。

　　论文中特别提到“通过强化学习发现新技能”的现象。例如，在普特南测试中，参数量较小的DeepSeek-Prover-V2-7B用非CoT生成模式成功解决了13个671B模型未能解决的问题。团队检查后发现，7B模型处理涉及有限基数的问题时，经常使用Cardinal.toNat和Cardinal.natCast_inj，而671B模型没有这些内容。这表明7B模型学会了671B模型未学会的新技能。

　　DeepSeek-Prover系列模型已推出三款：2024年3月的DeepSeek-Prover、2024年8月的DeepSeek-Prover-V1.5以及2025年5月的DeepSeek-Prover-V2。Prover-V1主要通过大规模合成数据集微调DeepSeek-Math-7B来推进定理证明。Prover-V1.5增加了证明助手反馈的强化学习（RLPAF）和蒙特卡洛树搜索方法。Prover-V2进一步提出“子目标分解的强化学习”，基础模型从DeepSeek-Math-7B升级到DeepSeek-V3，整合了高上下文窗口和强大的自然语言推理能力，统一了形式化和非形式化数学证明。

　　Prover-V2还继承了Prover-V1.5提出的CoT和非CoT生成两种模式。通过递归证明搜索合成冷启动推理数据，利用DeepSeek-V3将定理分解为高级证明草图并在Lean 4中形式化，从而产生一系列子目标。使用70亿参数模型处理每个子目标，减轻计算负担。一旦具有挑战性的问题的分解步骤得到解决，就将完整的逐步形式化证明与来自DeepSeek-V3的相应思维链配对，创建冷启动推理数据。