DeepSeek V4 做数学证明：普林斯顿以 500 倍成本优势刷新纪录

数学领域正被 AI 深刻冲击。2026 年 5 月，OpenAI 推翻 80 年"单位距离猜想"，菲尔兹奖得主高尔斯称"划时代里程碑"，陶哲轩宣布放弃实时跟进所有新证明："数学正从证明稀缺时代进入证明过剩时代。"

在此背景下，普林斯顿大学 PLI 团队（Sanjeev Arora + 陈丹琦）用 DeepSeek V4 Flash 构建 Goedel-Architect 智能体框架，以 294 美元完成 PutnamBench 全部 672 题——此前谷歌 Gemini 2.5 Pro 驱动的 Hilbert 系统需 17 万美元。通过率 75.6% vs 70.0%，成本优势约 500 倍。MiniF2F-test 达 99.2%，成为首个刷完全部 244 题的系统。

Goedel-Architect 的核心创新

"蓝图（Blueprint）"概念是 Goedel-Architect 的关键突破——在证明前先生成有向无环图，包含所有定义和引理的依赖关系，再分发给 Lean 证明器并行处理。失败不是终点而是诊断信号：系统通过"蓝图精炼"自动修正错误命题并分解难证引理。控制变量实验证明，500 倍成本优势的关键在于 pipeline 设计而非更好的模型。

核心研发团队

PLI 创始主任 Sanjeev Arora（ACM 计算奖得主）与陈丹琦（谷歌学术引用 9 万+，清华本科/斯坦福博士）共同领导。此前团队已发布 Goedel-Prover 系列，将 MiniF2F 从 60% 提升至 90%。

基准测试成绩

• PutnamBench：75.6% pass@1（Hilbert 70.0%），自然语言辅助后 88.8%
• MiniF2F-test：99.2%（首个刷完全部 244 题）
• IMO 2025：4/6 题
• Putnam 2025：11/12 题
• USAMO 2026：3/6 题（污染免疫测试）

500 倍成本优势来自 DeepSeek 极致性价比与蓝图精炼框架的双重创新。形式化定理证明是 AI 对齐和可信度的重要方向——Lean 编译器提供的确定性比任何同行评审都更可靠。更具象征意义的是：一支普林斯顿顶级团队选择了中国开源模型而非美国闭源模型来完成这项突破性工作，这对全球 AI 研究生态具有深远影响。

后续值得跟踪：

1. 开源扩散：Goedel-Architect 框架能否被其他模型（豆包/GLM）复现类似效果？
2. 研究生态信号：普林斯顿选用中国开源模型的决策对全球 AI 学术圈的影响
3. 形式化验证的产业化：在关键软件验证、智能合约审计等场景的应用前景