说实话，AI 在文本、图片、甚至代码生成领域已经卷得飞起，但有一个领域一直是“硬骨头”——形式化数学证明。这玩意儿不仅要求强大的逻辑推理能力，还得遵循一套极其严谨、不容出错的符号系统（比如 Lean 4）。直到昨天（2025年4月30日），DeepSeek 突然丢出了一个「王炸」：DeepSeek-Prover-V2-671B，一个参数量高达 6710 亿、专攻数学证明的超大型 MoE 模型，直接把这个领域的 SOTA（State-of-the-Art，当前最佳水平）推到了一个新高度！ 这还不算完，DeepSeek…