五一劳动节期间，DeepSeek 发布了其开源大语言模型 DeepSeek-Prover-V2，该模型在定理证明领域表现出色，特别是在 MiniF2F 测试中达到了 88.9% 的通过率，展示了其在数学推理和形式化证明方面的强大能力。
DeepSeek-Prover-V2 是专为数学 AI 编程语言 Lean 4 设计，通过递归式证明搜索生成冷启动推理数据，并结合强化学习技术，实现了非形式化和形式化数学推理的一体化融合。
该模型经历了两阶段训练，包括非思维链模式和思维链模式，最终在神经定理证明任务中达到了当前最先进的性能。
