DeepSeek_V4智能体系统：数学证明500倍成本优势刷新纪录
数学界近期被AI掀起了一场剧烈震荡。
2026年5月20日，OpenAI披露，其内部推理模型成功推翻了数学家保罗·埃尔德什（Paul Erdős）在1946年提出的「单位距离猜想」——这个离散几何领域的核心开放问题已屹立近80年。
菲尔兹奖得主蒂莫西·高尔斯（Timothy Gowers）给出高度评价。他直言，若人类能写出这样的论文投稿给顶级期刊《数学年刊》，他会毫不犹豫地推荐录用。
同月，另一位菲尔兹奖得主陶哲轩在斯坦福大学发表题为《新数学工作流》的演讲。他承认自己已不再实时跟进所有新证明——AI生成证明的速度远超人类消化节奏。他的判断直截了当：数学正从「证明稀缺时代」迈入「证明过剩时代」。真正的瓶颈不再是生成证明，而是如何验证和理解这些证明。
这句话值得深思。AI以人类完全无法追赶的速度批量产出数学结论，而我们越来越难以判断这些结论的可靠性。数学这门最讲究严格性的学科，正面临一场前所未有的验证危机。
可能的解法是什么？让AI来验证AI的证明。
这正是「形式化定理证明」的核心思路。目前最主流的形式化证明语言之一是Lean，它要求每个逻辑步骤都用机器可读的方式写出。一旦编译通过，证明的正确性由编译器担保，无需依赖任何人的主观判断。但这带来了新难题：让AI直接生成通过Lean编译器检验的完整证明，技术难度远高于撰写自然语言数学推导。
普林斯顿大学研究团队最近在arXiv上贴出了一篇新论文，提出了一个名为Goedel-Architect的智能体框架。而支撑这个框架的核心模型，是国内开源的大模型DeepSeek-V4-Flash。
论文标题：《Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement》
论文链接：https://arxiv.org/abs/2606.06468
先说一组硬核数据。
在形式化定理证明领域，标准测试集PutnamBench包含672道来自普特南大学生数学竞赛的题目。解决这672道题，不同系统的成本差距极为悬殊。
此前最强的开源pipeline之一是Hilbert，由Google的Gemini 2.5 Pro驱动。Hilbert跑完这672道题，仅API调用费用就花了约17万美元。而Goedel-Architect完成同样评测，花费仅294美元。两者相差约500倍。
更值得一提的是，Goedel-Architect在PutnamBench上的通过率（75.6%）还高于Hilbert（70.0%）。成本更低，效果更好——这已不只是节省经费的问题。
系统名字「Goedel-Architect」致敬库尔特·哥德尔，那位证明了数学存在根本性局限的著名数学家。普林斯顿与哥德尔渊源深厚：哥德尔晚年正是在普林斯顿高等研究院度过。而这篇论文的研究团队来自普林斯顿大学语言与智能研究中心（Princeton Language and Intelligence，PLI）。
PLI创始主任Sanjeev Arora，在计算复杂性理论领域享有盛誉，2011年获得ACM计算奖。他长期关注一个核心问题：AI能否成为超越人类的数学家？他在海德堡桂冠论坛上公开阐述过一条路径——用Lean这样的形式化系统作为锚点，让AI的「幻觉」倾向无处遁形，因为编译器不会接受逻辑有漏洞的证明。
共同领导团队的还有陈丹琦。她同样来自普林斯顿计算机系，谷歌学术引用量超过9万次。本科毕业于清华，博士在斯坦福师从Christopher Manning。她最早期也最知名的成果之一，是与Manning共同开发了谷歌SyntaxNet底层的依存句法解析算法。进入普林斯顿后，她长期聚焦于语言模型的训练与适配、知识表示与推理，以及问答系统的大规模构建。
这支团队此前已发布过两代Goedel-Prover，是专门用于形式化定理证明的开源模型系列。在MiniF2F基准上，成绩从最初的60%逐步提升到90%。而Goedel-Architect是他们在这个方向上走到的最新一步——重点已从模型本身转向如何用智能体框架来组织整个证明过程。
这个新框架的关键在于「蓝图」（blueprint）这个概念。
Goedel-Architect的整体架构。
想象一下大型建筑工地。多个工程队可以同时开工，但前提是有一张完整的施工图：哪个区域先建，哪个结构依赖哪个地基，哪些部分可以并行推进。没有施工图，整个工程效率会非常低。
形式化定理证明本质上也是类似的事情。现有许多系统采用「递归分解」的方式：遇到难题就拆成更小的子目标，再递归往下拆，形成一棵自上而下的树。问题在于，一旦某个分支走入死胡同，整棵树的劳动成果都可能报废，最终陷入低效的循环试错。
Goedel-Architect的思路不同。在正式动手证明之前，系统会先生成一张「蓝图」：这是一张有向无环图，里面包含通向最终定理所需要的所有定义和引理，以及它们之间的依赖关系。每个节点是一个经过精确定义的引理，每条边表明「这个引理依赖那个结果」。这张图就是整个证明策略的全局视图。
有了蓝图之后，系统就可以把图中所有尚未被证明的节点分发给Lean证明器，并行处理。每个证明器只看到自己负责的那个引理和它声明的上游依赖结果，不会被其他信息干扰。经过一轮并行证明，有的节点被成功证明（标记为绿色），有的失败了（标记为蓝色），还有的甚至被反向证明了——也就是说这个引理本身是错的（标记为红色）。
失败不是终点，而是一个「诊断信号」。这正是整个框架的第三个核心部分：蓝图精炼（blueprint refinement）。
当一个引理节点无法证出来时，系统不会直接记录一个失败就了事。它会要求证明器写一份结构化的「事后分析报告」，包含三块内容：失败原因是命题本身有误，还是证明思路太难？尝试过哪些策略，卡在了哪里？以及，建议的修复方案是什么？
系统专门设计了两类失败模式的处理路径。
第一类是「命题有误」。如果某个引理被反向证明为假，系统会提取导致反例的具体原因，并在下一轮迭代中修改这个节点的陈述。论文里举了一个例子：在处理Putnam 1989年的一道题时，蓝图里提出过一个关于二进制表示的辅助引理：「将一个数乘以2，相当于在二进制展开的末尾追加一个零」。证明器在n=5时找到了反例——Lean的数学库中，二进制位是从最低有效位开始存储的，所以乘以2实际上是在最高有效位前面加零，而不是末尾追加。一字之差，整个命题都错了。系统记录下这个「方向搞反了」的诊断，下一轮迭代直接就把引理改成了正确的版本，并且把这个修正传播给所有依赖该引理的节点。
第二类是「证明太难」。如果一个引理在逻辑上为真，但证明器在规定的token预算内就是搞不定，系统会要求它写下来：「如果给我更多步骤，我打算怎么分解这个引理」。这份分解建议会在下一轮迭代中被纳入蓝图，把一个难啃的节点拆成若干个更容易处理的子节点。论文中提到了Putnam 1985年的一道题：一个关于五次多项式根的引理，证明器认为正确但力量不足，于是建议按四种情形分类讨论。下一轮迭代接受了这个分解，所有子情形都顺利通过了证明。
已经成功证明的节点在迭代中会保留下来。整个过程就像在逐步完成一幅拼图，每一轮都在已有的完成部分上继续向前推进，而不是每次都从头开始。
团队在五个基准上测试了Goedel-Architect。
MiniF2F-test是最成熟的高中竞赛数学测试集之一，包含244道题。Goedel-Architect在pass@1的条件下解出了其中242道（99.2%），与此前最强的开源系统持平。剩余的2道题都是IMO级别的难题，借助自然语言证明辅助后也一并解决，团队因此成为首个完全刷完MiniF2F-test全部244道题的系统。
PutnamBench上的表现前文已提过：75.6%的pass@1通过率，超过了在16万美元预算下运行的Hilbert（70.0%）。加入自然语言辅助之后，通过率进一步拉到了88.8%（597/672），而总花费仍然不到1000美元。
在更新的竞赛题目上，系统也交出了不错的成绩：IMO 2025的4/6道、Putnam 2025的11/12道。值得单独拎出来讲的是USAMO 2026——这套题目的出题时间晚于所有模型的训练截止日期，所以不存在「记住了答案」的嫌疑，是一种真正意义上的污染免疫测试。Goedel-Architect解出了其中的3/6道。
系统还有一个可选的辅助机制：在生成初始蓝图时，可以额外提供一份自然语言的证明思路，作为结构上的参考。这份自然语言证明由参数更大的模型（比如Gemini 3.1 Pro）生成，但它只起到「脚手架」的作用——提供一个高层次的策略框架，最终的具体形式化实现仍然由Goedel-Architect自己完成。
对绝大多数题目来说，这种辅助是非必需的。但是对「非局部结构」的难题——比如需要循环求和、奇偶性链推导、或抽象代数结构——光靠形式化命题本身去做依赖图推导，就会遇到瓶颈。在这些情形下，自然语言提供的结构指引是决定性的。团队专门挑了9道这样的难题做了对照实验：在不使用自然语言辅助的情况下，每道题跑了4到12次，全部失败；而一旦加入辅助，9道题全部解决。
论文里做了一组控制变量的对比实验，核心结论很明确：提升主要来自pipeline设计，而不仅仅是更好的模型。
团队把Hilbert（采用递归分解策略的系统）移植到同样的DeepSeek-V4-Flash骨干上运行，在MiniF2F上只能达到84.4%，而Goedel-Architect在同样的骨干下达到了99.2%。在PutnamBench的200题子集上，工具增强的单智能体方式（tool-integrated reasoning）以相同骨干达到了54.5%，而Goedel-Architect达到了76.0%，而且每道题消耗的token数更少。
递归分解策略的问题在于，它经常在单个子目标上反复尝试，有时会在死胡同里绕来绕去。全局蓝图策略则允许系统先退后一步，看清整张图。在并行尝试的过程中，任何一个节点的失败信息都可以立刻反馈到整个策略的调整上，不需要等到整棵递归树完全走完才做判断。
这项工作的技术意义很清晰：一套成本极低的开源框架，在形式化定理证明的核心基准上达到了此前只有昂贵的闭源系统才能触及的水平。
形式化证明系统的价值，本质上在于提供了一类基础设施，让AI的数学输出变得「可信」。如果有一天AI声称自己证明了一个重要猜想，Lean编译器的判断比任何同行评审都要确定。而Goedel-Architect让这套基础设施的访问门槛降低了大约两个数量级——这大概是目前数学界最值得持续关注的进展之一。