DeepSeek发布了开源数学定理证明模型Prover-V1.5，通过将数学问题转换为Lean编程语言，引入强化学习系统，实现了自我迭代和Lean证明器监督。该模型在高中和大学数学定理证明测试中取得了63.5%和25.3%的成功率，超越了多款开源模型。DeepSeek-Coder-V2结合Lean证明器标注中间状态信息，提高了模型的形式化证明能力。模型训练采用GRPO算法进行强化学习训练，并引入RMaxTS算法解决证明搜索中的奖励稀疏问题。DeepSeek-Prover-V1.5在miniF2F和ProofNet基准测试中取得了新的SOTA。