正当大家纷纷进入“五一”假期模式时，AI 界的 “劳模” DeepSeek 再次证明：放假？不存在的。他们就在这个节骨眼上，悄然向开源社区投喂了一款重量级新模型——DeepSeek-Prover-V2-671B。

模型现已登陆 Hugging Face (链接: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B)，光看这 6710 亿（671B）的参数量，就足以让不少机器瑟瑟发抖。

这并非一款通用大模型，而是 DeepSeek 专为高难度数学领域，特别是使用 Lean 4 进行形式化定理证明而打造的“专业选手”。

作为 DeepSeek-Prover 系列的第二代产品，大家自然对其能力充满期待。要知道，其前身 V1.5（虽然只有 7B 参数）在去年的高中数学测试 (miniF2F) 中已能达到 63.5% 的成功率，在大学级别测试 (ProofNet) 中也有 25.3% 的准确率。如今参数量暴涨近百倍的 V2，潜力显然不可同日而语，但具体实力如何，还有待验证。

然而，DeepSeek 这次的操作颇有“先把孩子生下来，名字和体检报告稍后补上”的风格。模型权重已经大方开源，但至关重要的 Model Card (模型详细说明书) 和 Benchmark (官方性能成绩单) 却暂时缺席。

这不禁让人猜测，是团队为了赶在假期前“交卷”过于匆忙，还是有意让社区进行一轮“盲测”和探索？

总之，劳动节是得继续劳动了。