• DeepSeek 发布 DeepSeek-Prover-V2：这是一个专为 Lean 4 中的形式定理证明设计的开源大型语言模型，基于 DeepSeek-V3 基础模型的递归定理证明管道构建，Lean 4 是微软研究院开发的 Lean 定理证明器的最新版本，该功能编程语言和交互式定理证明系统允许数学家和计算机科学家编写经过机器检查验证的形式证明。
• 项目目标：朝着弥合形式和非形式数学推理的差距迈进，利用通用语言模型的能力处理形式定理证明的结构化领域，其方法通过将复杂定理分解为更易管理的组件来模拟人类证明构建方法。
• 评估框架扩展：DeepSeek 研究团队用专门为形式定理证明评估设计的新基准集合扩展了评估框架，包括 325 个形式化问题，其中 15 个来自最近的美国数学邀请赛（AIME）竞赛。
• 测试结果：在 AIME 问题上的初步测试结果显示，专门的定理证明模型表现出有希望的性能，DeepSeek-Prover-V2 成功解决了 15 个 AIME 问题中的 6 个，而通用的 DeepSeek-V3 模型在使用多数投票技术时解决了 8 个。
• 证明构建方法：通用模型在生成完整的 Lean 证明方面存在困难，因此指导 DeepSeek-V3 仅生成带有省略细节的高级证明草图，然后采用递归解决策略系统地解决每个中间证明步骤，提取子目标表达式并将其用作前提，以促进更局部的依赖结构和更简单引理的开发。
• 资源优化：为优化计算资源，系统使用较小的 7B 参数模型处理分解的引理，以管理广泛证明搜索的计算需求，当所有分解步骤成功解决时，最终得出自动派生的完整证明。
• 架构与数据合成：算法框架分两个阶段运行，利用 DeepSeek-V3 进行引理分解和 7B 证明器模型完成相应的形式证明细节，为合成形式推理数据建立了自然途径，将高级数学推理与严格的形式验证要求相结合。
• 专家担忧：一些专家对研究的实施细节表示担忧，如潜在的错误形式化示例和隐含的 sorry 等问题，凸显了形式验证领域的持续挑战。
• 模型版本与资源：DeepSeek 发布了两种不同模型大小的 Prover-V2，7B 参数版本基于之前的 Prover-V1.5-Base，具有 32K 令牌的扩展上下文长度，671B 参数版本在 DeepSeek-V3-Base 上训练，两者都在 HuggingFace 上可用，同时还有包含 325 个形式化问题的 ProverBench 数据集。