继2月论文“撞车”之后，梁文锋和杨植麟又在另一个大模型赛道上相遇了。
4月30日，DeepSeek上线新模型DeepSeek-Prover-V2，这是一个数学定理证明专用模型。
Prover-V2的参数规模进一步扩展到671B（6710亿规模参数），相较于前一代V1.5版本的7B规模增加了近百倍，这让其在数学测试集上的效率和正确率更高，比如，该模型的miniF2F测试通过率达到88.9%，它还解决了PutnamBench（普特南测试）的49道题。
巧合的是，4月中旬，月之暗面也曾推出一款用于形式化定理证明的大模型Kimina-Prover，这是Kimi团队和Numina共同研发的大模型，该产品也开源了1.5B和7B参数的模型蒸馏版本。该模型的miniF2F测试通过率为80.7%，PutnamBench测试成绩为10道题。
两者相比较，在miniF2F测试通过率以及普特南测试上，DeepSeek-Prover-V2的表现超过了Kimina-Prover预览版。
值得注意的是，两家公司在技术报告中都提到了强化学习。比如DeepSeek的题目为《DeepSeek-Prover-V2：通过子目标分解的强化学习推进形式数学推理》，而月之暗面的题目为《Kimina-Prover Preview：基于强化学习技术的大型形式推理模型》。
在2月的两篇“撞车”论文中，梁文锋和杨植麟都在作者行列，两家公司都关注Transformer架构最核心的注意力机制，即如何让模型更好地处理长上下文。
作为中国大模型领域最受瞩目的创业者，两人也正在面临不同的挑战。
对于梁文锋而言，在R1模型推出三个多月后，外界对DeepSeek“魔法”的痴迷程度正在下降，阿里巴巴的开源模型正在迅速赶上以及超过DeepSeek，外界热切期待其发布R2或V4模型，以加强领先优势。
对于杨植麟和月之暗面，Kimi正在遭受来自字节跳动的豆包和腾讯元宝的挑战，它也需要保持持续创新。
编程与数学，实现AGI的两条路径
对于AGI的实现路径，2024年，DeepSeek创始人梁文锋在接受《暗涌》采访时曾说，他们确实押注了三个方向：一是数学和代码、二是多模态、三是自然语言本身。数学和代码是AGI天然的试验场，有点像围棋，是一个封闭的、可验证的系统，有可能通过自我学习就能实现很高的智能。另一方面，多模态需要参与到人类真实世界里学习。他们对一切可能性都保持开放。
此次Prover-V2模型的推出，让DeepSeek的各个模型矩阵保持了同步进化。
Prover系列模型于2024年3月开始被发布，2024年8月被更新为DeepSeek-Prover-V1.5（后简称为Prover-V1.5），2025年4月再被更新至DeepSeek-Prover-V2。
DeepSeek代码系列模型Coder从2024年4月开始更新，6月升级为Coder-V2-0614，7月再次升级，9月，DeepSeek-V2-Chat和DeepSeek-Coder-V2合并，升级后的新模型为DeepSeek-V2.5，2024年12月，该模型更新至V3，今年3月，升级至V3-0324。
通用推理大模型，以1月20日发布的R1模型为代表，价格低廉，自然语言推理性能强劲，在数学、代码、自然语言推理等任务上，性能比肩OpenAI o1正式版。
从Prover-V2的技术报告上看，其与DeepSeek的其他模型进化有关联，其中，DeepSeek-Prover-V2-671B是以DeepSeek-V3作为基础模型来做微调，如在冷启动阶段，DeepSeek-V3将复杂问题分解为一系列子目标，而后，已解决子目标的证明被合成到一个思维过程链中，结合DeepSeek-V3的逐步推理，为强化学习创建一个初始冷启动。
算法工程师、知乎用户“小小将”告诉《中国企业家》，推理模型在进行推理时，要进行复杂的思考，代码与数学模型可以检验推理大模型能力进展，因为数学与代码的结果是可验证的。
他认为，Prover-V2的推出与新模型R2或V4的上线没有必然联系，它更像是一个独立模型的更新。
他预测，R2模型更像是GPT-o1到o3的过程，比如在提高强化学习的能力方面，DeepSeek可以基于V3，提升后训练效果，因此R2的研发周期可能会比较短。但V4就是一个大版本的更新，其研发周期有可能更长，因为预训练的工程量以及训练方法可能都会发生变化。
目前市场已经对DeepSeek的新模型充满了想象和期待。
市场上传言，R2模型将基于华为昇腾系列GPU芯片而推出，但一位行业人士说，这个消息不太可靠，在英伟达H20芯片被限之后，昇腾系列芯片在市场上也是一卡难求，“对于昇腾来说，如果用于大模型研发，可能鲁棒性没那么强”。
另有创业公司相关人士告诉《中国企业家》，华为昇腾芯片用于大模型的训练，效果一般，原因在于生态系统没那么完善，但用于大模型的推理与部署，是没有问题的。
DeepSeek与Kimi还能保持领先吗？
DeepSeek与月之暗面作为明星初创公司，正在遭受大公司的追赶和超越。
以月之暗面旗下的Kimi为例，据QuestMobile数据，Kimi上线不足1年，在2024年11月，月活突破2000万，仅次于豆包的5600万。
QuestMobile数据显示，截至2025年2月底，AI原生APP月活规模前三名从豆包、Kimi、文小言更迭为DeepSeek、豆包、腾讯元宝，规模分别是1.94亿、1.16亿、0.42亿。
2月中旬，腾讯元宝宣布接入DeepSeek，随后，在一个多月时间内，腾讯元宝利用超级产品微信引流加上疯狂买量投流，在用户数量上已经超过了Kimi，成为排名第三的AI产品。据AppGrowing数据，在今年一季度，腾讯元宝的投流费用为14亿元，远远超过Kimi的1.5亿元规模。
目前，Kimi最新的举动是内测社区功能，增加用户粘性。
DeepSeek同样也避免不了被大公司追赶甚至超越的挑战。近期，阿里巴巴在大模型方面展现出了强劲的竞争力。
4月29日，阿里巴巴发布新一代通义千问模型Qwen3，该模型被称作首个“混合推理模型”，是“快思考”和“慢思考”集成的一个模型，参数量仅为DeepSeek-R1的1/3，性能全面超越R1、OpenAI o1等同行产品。
此前，蔡崇信评价DeepSeek，它告诉了我们开源的价值。根据公开数据，阿里通义已开源200余个模型，全球下载量超3亿次，千问衍生模型数超10万个，已超越美国Llama，成为全球第一开源模型。
一位AI创业者告诉《中国企业家》，DeepSeek受到了过多的关注，被赋予过多光环，中国大模型产业需要两三个世界领先的大模型，而不是一个，这时候应鼓励这个领域的竞争和创业。
另一个重要玩家是百度。4月25日，百度发布文心4.5 Turbo和深度思考模型X1 Turbo，这两款模型性能更强大，成本更低，李彦宏更是数次提到DeepSeek，他说，DeepSeek也不是万能的，它只能处理单一的文本，还不能理解声音、图片、视频等多媒体内容，同时幻觉率比较高，很多场合不能放心使用。
“DeepSeek最大的问题是慢和贵，中国市场上绝大多数大模型API的价格都更低，而且反应速度更快。”李彦宏在发布会上说。
尽管如此，百度仍决定学习DeepSeek，今年2月，百度决定在6月30日开源文心大模型4.5系列。
越来越多的玩家参与大模型开源竞赛，但只有技术最先进的玩家才能定义标准。
继2月论文“撞车”之后，梁文锋和杨植麟又在另一个大模型赛道上相遇了。
4月30日，DeepSeek上线新模型DeepSeek-Prover-V2，这是一个数学定理证明专用模型。
Prover-V2的参数规模进一步扩展到671B（6710亿规模参数），相较于前一代V1.5版本的7B规模增加了近百倍，这让其在数学测试集上的效率和正确率更高，比如，该模型的miniF2F测试通过率达到88.9%，它还解决了PutnamBench（普特南测试）的49道题。
巧合的是，4月中旬，月之暗面也曾推出一款用于形式化定理证明的大模型Kimina-Prover，这是Kimi团队和Numina共同研发的大模型，该产品也开源了1.5B和7B参数的模型蒸馏版本。该模型的miniF2F测试通过率为80.7%，PutnamBench测试成绩为10道题。
两者相比较，在miniF2F测试通过率以及普特南测试上，DeepSeek-Prover-V2的表现超过了Kimina-Prover预览版。
值得注意的是，两家公司在技术报告中都提到了强化学习。比如DeepSeek的题目为《DeepSeek-Prover-V2：通过子目标分解的强化学习推进形式数学推理》，而月之暗面的题目为《Kimina-Prover Preview：基于强化学习技术的大型形式推理模型》。
在2月的两篇“撞车”论文中，梁文锋和杨植麟都在作者行列，两家公司都关注Transformer架构最核心的注意力机制，即如何让模型更好地处理长上下文。
作为中国大模型领域最受瞩目的创业者，两人也正在面临不同的挑战。
对于梁文锋而言，在R1模型推出三个多月后，外界对DeepSeek“魔法”的痴迷程度正在下降，阿里巴巴的开源模型正在迅速赶上以及超过DeepSeek，外界热切期待其发布R2或V4模型，以加强领先优势。
对于杨植麟和月之暗面，Kimi正在遭受来自字节跳动的豆包和腾讯元宝的挑战，它也需要保持持续创新。
编程与数学，实现AGI的两条路径
对于AGI的实现路径，2024年，DeepSeek创始人梁文锋在接受《暗涌》采访时曾说，他们确实押注了三个方向：一是数学和代码、二是多模态、三是自然语言本身。数学和代码是AGI天然的试验场，有点像围棋，是一个封闭的、可验证的系统，有可能通过自我学习就能实现很高的智能。另一方面，多模态需要参与到人类真实世界里学习。他们对一切可能性都保持开放。
此次Prover-V2模型的推出，让DeepSeek的各个模型矩阵保持了同步进化。
Prover系列模型于2024年3月开始被发布，2024年8月被更新为DeepSeek-Prover-V1.5（后简称为Prover-V1.5），2025年4月再被更新至DeepSeek-Prover-V2。
DeepSeek代码系列模型Coder从2024年4月开始更新，6月升级为Coder-V2-0614，7月再次升级，9月，DeepSeek-V2-Chat和DeepSeek-Coder-V2合并，升级后的新模型为DeepSeek-V2.5，2024年12月，该模型更新至V3，今年3月，升级至V3-0324。
通用推理大模型，以1月20日发布的R1模型为代表，价格低廉，自然语言推理性能强劲，在数学、代码、自然语言推理等任务上，性能比肩OpenAI o1正式版。
从Prover-V2的技术报告上看，其与DeepSeek的其他模型进化有关联，其中，DeepSeek-Prover-V2-671B是以DeepSeek-V3作为基础模型来做微调，如在冷启动阶段，DeepSeek-V3将复杂问题分解为一系列子目标，而后，已解决子目标的证明被合成到一个思维过程链中，结合DeepSeek-V3的逐步推理，为强化学习创建一个初始冷启动。
算法工程师、知乎用户“小小将”告诉《中国企业家》，推理模型在进行推理时，要进行复杂的思考，代码与数学模型可以检验推理大模型能力进展，因为数学与代码的结果是可验证的。
他认为，Prover-V2的推出与新模型R2或V4的上线没有必然联系，它更像是一个独立模型的更新。
他预测，R2模型更像是GPT-o1到o3的过程，比如在提高强化学习的能力方面，DeepSeek可以基于V3，提升后训练效果，因此R2的研发周期可能会比较短。但V4就是一个大版本的更新，其研发周期有可能更长，因为预训练的工程量以及训练方法可能都会发生变化。
目前市场已经对DeepSeek的新模型充满了想象和期待。
市场上传言，R2模型将基于华为昇腾系列GPU芯片而推出，但一位行业人士说，这个消息不太可靠，在英伟达H20芯片被限之后，昇腾系列芯片在市场上也是一卡难求，“对于昇腾来说，如果用于大模型研发，可能鲁棒性没那么强”。
另有创业公司相关人士告诉《中国企业家》，华为昇腾芯片用于大模型的训练，效果一般，原因在于生态系统没那么完善，但用于大模型的推理与部署，是没有问题的。
DeepSeek与Kimi还能保持领先吗？
DeepSeek与月之暗面作为明星初创公司，正在遭受大公司的追赶和超越。
以月之暗面旗下的Kimi为例，据QuestMobile数据，Kimi上线不足1年，在2024年11月，月活突破2000万，仅次于豆包的5600万。
QuestMobile数据显示，截至2025年2月底，AI原生APP月活规模前三名从豆包、Kimi、文小言更迭为DeepSeek、豆包、腾讯元宝，规模分别是1.94亿、1.16亿、0.42亿。
2月中旬，腾讯元宝宣布接入DeepSeek，随后，在一个多月时间内，腾讯元宝利用超级产品微信引流加上疯狂买量投流，在用户数量上已经超过了Kimi，成为排名第三的AI产品。据AppGrowing数据，在今年一季度，腾讯元宝的投流费用为14亿元，远远超过Kimi的1.5亿元规模。
目前，Kimi最新的举动是内测社区功能，增加用户粘性。
DeepSeek同样也避免不了被大公司追赶甚至超越的挑战。近期，阿里巴巴在大模型方面展现出了强劲的竞争力。
4月29日，阿里巴巴发布新一代通义千问模型Qwen3，该模型被称作首个“混合推理模型”，是“快思考”和“慢思考”集成的一个模型，参数量仅为DeepSeek-R1的1/3，性能全面超越R1、OpenAI o1等同行产品。
此前，蔡崇信评价DeepSeek，它告诉了我们开源的价值。根据公开数据，阿里通义已开源200余个模型，全球下载量超3亿次，千问衍生模型数超10万个，已超越美国Llama，成为全球第一开源模型。
一位AI创业者告诉《中国企业家》，DeepSeek受到了过多的关注，被赋予过多光环，中国大模型产业需要两三个世界领先的大模型，而不是一个，这时候应鼓励这个领域的竞争和创业。
另一个重要玩家是百度。4月25日，百度发布文心4.5 Turbo和深度思考模型X1 Turbo，这两款模型性能更强大，成本更低，李彦宏更是数次提到DeepSeek，他说，DeepSeek也不是万能的，它只能处理单一的文本，还不能理解声音、图片、视频等多媒体内容，同时幻觉率比较高，很多场合不能放心使用。
“DeepSeek最大的问题是慢和贵，中国市场上绝大多数大模型API的价格都更低，而且反应速度更快。”李彦宏在发布会上说。
尽管如此，百度仍决定学习DeepSeek，今年2月，百度决定在6月30日开源文心大模型4.5系列。
越来越多的玩家参与大模型开源竞赛，但只有技术最先进的玩家才能定义标准。
