DeepSeek AI发布开源大语言模型DeepSeek-Prover-V2，专为Lean 4环境中的形式化定理证明设计。该模型引入创新的递归定理证明管道，利用DeepSeek-V3生成高质量初始化数据，在神经定理证明领域取得最先进性能，并附带新的基准数据集。