主要观点总结
DeepSeek团队发布了名为DeepSeek-Prover-V2的新模型，该模型是一款专为数学AI编程语言Lean 4打造的开源大语言模型，专注于形式化定理证明。它通过递归定理证明流程收集初始化数据，并能在定理证明赛道上实现最佳性能。新模型发布后引起了广泛关注，网友对其表示赞赏。
关键观点总结
关键观点1: DeepSeek-Prover-V2的发布
DeepSeek团队发布了DeepSeek-Prover-V2模型，它是专为数学AI编程语言Lean 4打造的大语言模型，旨在进行形式化定理证明。
关键观点2: 模型的技术特点
DeepSeek-Prover-V2通过递归定理证明流程收集数据，并在定理证明赛道上实现了最佳性能，达到了88.9%的通过率。
关键观点3: 模型的训练过程
DeepSeek-Prover-V2经历了两阶段训练，建立了两种互补的证明生成模式。第一阶段采用专家迭代训练非CoT证明模型，第二阶段则通过冷启动链式思维数据生成和强化学习阶段增强CoT模式。
关键观点4: 模型的性能表现
DeepSeek-Prover-V2在神经定理证明任务中达到了当前最先进的性能，并在多个基准数据集上进行了系统评估，包括高中竞赛题目和本科水平的数学问题。
关键观点5: 网友的评价和反响
DeepSeek-Prover-V2的发布引起了广泛关注，网友对其表示赞赏，并期待DeepSeek能够再次改变世界。
文章预览
机器之心报道 编辑：大盘鸡、泽南 DeepSeek R2 的前奏？ 五一劳动节到了，DeepSeek 的新消息可没停下来。 前些天到处都在流传着 DeepSeek-R2 即将发布的传言，DeepSeek 确实有新动作，不过大家没等来 R2，等来的是 DeepSeek-Prover-V2，它当然也是开源的。 Prover-V2 在定理证明赛道上实现了业内最佳性能，在 MiniF2F 测试中达到了 88.9% 的通过率，在 AIME 24、25 上也有不错的分数。 在 4 月 30 日晚，机器学习协作平台 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技术细节。 这次 DeepSeek 团队发布了两个版本的 DeepSeek-Prover-V2 模型，参数规模分别为 7B 和 671B。 其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基础上训练而成，而 DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，并支持最长 32K tokens 的上下文长度扩展。 DeepSeek-Prover-V2-7B 链接：https://huggingface.co/deepseek-ai/DeepSeek-
………………………………
