在人工智能的大模型赛道上，两位业界佼佼者梁文锋和杨植麟再次狭路相逢。继今年2月两人的论文“撞车”事件后，4月30日，梁文锋领导的DeepSeek推出了数学定理证明专用模型DeepSeek-Prover-V2。
DeepSeek-Prover-V2的参数规模空前庞大，达到了6710亿，是前一代V1.5版本的近百倍。这一升级使得模型在数学测试集上的效率和正确率显著提升，miniF2F测试通过率高达88.9%，并成功解决了PutnamBench的49道题。这一成绩令人瞩目。
几乎在同一时间，杨植麟的月之暗面也推出了形式化定理证明大模型Kimina-Prover。该模型由Kimi团队与Numina联合研发，同样提供了开源版本。虽然Kimina-Prover在miniF2F测试上的通过率为80.7%，PutnamBench测试成绩为10道题，表现不俗，但在与DeepSeek-Prover-V2的对比中仍稍显逊色。
值得注意的是，两款模型的技术报告中都强调了强化学习的应用。DeepSeek的论文标题为《DeepSeek-Prover-V2：通过子目标分解的强化学习推进形式数学推理》，而月之暗面的论文则题为《Kimina-Prover Preview：基于强化学习技术的大型形式推理模型》。这显示了强化学习在数学定理证明领域的重要性。
梁文锋和杨植麟的再次“交锋”也引发了对两人及其公司面临的挑战的关注。DeepSeek在推出R1模型后，外界的关注度有所下降，同时面临着阿里巴巴等巨头的迅速追赶。而月之暗面的Kimi则正在与字节跳动的豆包和腾讯元宝等竞争产品激烈竞争。
在探讨AGI（通用人工智能）的实现路径时，梁文锋曾表示DeepSeek押注了数学和代码、多模态、自然语言三个方向。此次Prover-V2模型的推出，进一步强化了DeepSeek在数学和代码领域的实力，同时也保持了其模型矩阵的同步进化。
DeepSeek的代码系列模型Coder也经历了多次升级，从Coder-V2到DeepSeek-V2.5，再到V3和V3-0324，性能不断提升。而通用推理大模型R1则以低廉的价格和强劲的自然语言推理性能赢得了市场认可。
尽管DeepSeek和月之暗面作为明星初创公司备受瞩目，但它们也面临着来自大公司的巨大压力。腾讯元宝利用微信引流和大量投流，用户数量迅速增长，成为排名第三的AI产品。而阿里巴巴的新一代通义千问模型Qwen3则以更小的参数量和更全面的性能超越了DeepSeek-R1和OpenAI o1等产品。
百度同样是大模型领域的重要玩家。李彦宏在发布会上多次提及DeepSeek的局限性，并宣布百度将学习DeepSeek，在6月30日开源文心大模型4.5系列。这一举动显示了百度在大模型领域的决心和实力。
随着越来越多的玩家加入大模型开源竞赛，竞争愈发激烈。但只有技术最先进的玩家才能定义标准，引领行业发展。DeepSeek和月之暗面能否保持领先地位，让我们拭目以待。
在数学定理证明领域，DeepSeek-Prover-V2和Kimina-Prover的推出标志着AI技术在这一领域的重大突破。两款模型都利用了强化学习技术，提高了数学推理的效率和准确性。未来，随着技术的不断进步和应用场景的拓展，数学定理证明模型有望在更多领域发挥重要作用。
对于AGI的实现路径，DeepSeek的探索为我们提供了宝贵的启示。数学和代码作为AGI的天然试验场，具有封闭性和可验证性，是实现高智能的潜在途径。同时，多模态学习也是实现AGI不可或缺的一部分。未来，随着技术的不断融合和创新，我们有望看到更加智能、更加全面的AI系统的出现。
在激烈的竞争环境中，DeepSeek和月之暗面等初创公司需要不断创新和突破，以保持领先地位。同时，它们也需要与大公司展开合作与竞争，共同推动人工智能技术的发展和应用。
