DeepSeek V4做数学证明，500倍成本优势：智能体系统刷新多项纪录

形式化证明成AI数学“信任锚点”，普林斯顿团队祭出蓝图精炼法

AI生成数学证明的速度已远超人类消化能力。菲尔兹奖得主陶哲轩直言，数学正从“证明稀缺时代”进入“证明过剩时代”，核心瓶颈从“如何生成证明”转向“如何验证证明”。普林斯顿大学语言与智能研究中心（PLI）团队选择用形式化系统Lean作为锚点——Lean要求每一步都经编译器检验，通过即由机器担保正确性。但直接生成本地Lean证明的技术难度远高于自然语言推导。该团队新推出的Goedel-Architect框架，基于DeepSeek-V4-Flash模型，核心创新在于“蓝图”机制：

• 全局策略先行：证明开始前，系统先生成一幅有向无环图，包含所有定义、引理及其依赖关系，作为整体战略。
• 并行验证与失败反馈：将蓝图中的未证明节点并行分发至Lean证明器。失败节点会被标记（命题错误为红色、证明过难为蓝色），并触发结构化“事后分析报告”。
• 蓝图精炼：错误命题会被修正并传播依赖修改；过难节点根据证明器建议拆分为子节点。已证明节点全程保留，避免递归分解中走入死胡同后全盘作废的低效问题。

五百倍成本碾压：294美元 vs 17万美元，效果反而更好

在形式化定理证明标准测试集PutnamBench（672道普特南竞赛题）上，Goedel-Architect的效率令人咋舌：

• Hilbert（谷歌Gemini 2.5 Pro驱动）：花费约17万美元API调用费，通过率70.0%。
• Goedel-Architect（DeepSeek-V4-Flash驱动）：仅花费294美元，通过率达75.6%。
• 成本差距约500倍，且新系统效果更优。借助自然语言辅助后，通过率进一步提升至88.8%（597/672），总花费仍不到1000美元。单题成本仅约0.44美元，较同类开源方案降低两个数量级。

多项基准封顶：首个刷完MiniF2F全量题库，直面污染免疫测试

Goedel-Architect在多个核心基准上展现了统治力：

• MiniF2F-test（244道高中竞赛题）：pass@1下解决242道（99.2%），成为首个攻克全部题目的系统，剩余两道IMO难题借助自然语言辅助后也得以解决。
• 最新竞赛题目：IMO 2025解决4/6题，Putnam 2025解决11/12题。其中USAMO 2026的出题时间晚于所有模型训练截止日期，构成污染免疫测试——Goedel-Architect仍解决3/6题，证明其泛化能力而非记忆。
• 控制实验：将Hilbert的递归分解策略移植到相同DeepSeek-V4-Flash骨干上，MiniF2F通过率仅84.4%，而Goedel-Architect达99.2%；在PutnamBench 200题子集上，工具增强单智能体方式仅54.5%，Goedel-Architect达76.0%且每道题消耗token更少。

开源推动可信AI数学基础设施落地

形式化证明系统的最终价值在于提供“可信”基础设施——当AI声称证明重要猜想时，Lean编译器的判断比任何同行评审更确定。Goedel-Architect的研发团队由计算复杂性理论权威Sanjeev Arora（2011年ACM计算奖得主）和计算机系教授陈丹琦共同领导，此前已发布两代Goedel-Prover开源模型系列。新框架将形式化证明门槛降低了约两个数量级：不仅成本从数十万美元降至数百美元，且框架本身开源、骨干模型开源，使得更多研究机构能够参与“用AI验证AI”的闭环。