2026年5月，数学领域接连被AI的产出冲击。先是OpenAI宣布其内部推理模型成功推翻了困扰离散几何近80年的"单位距离猜想"，菲尔兹奖得主蒂莫西·高尔斯评价这篇论文质量足以直接发表在《数学年刊》上。紧接着，陶哲轩在斯坦福大学宣布自己已放弃实时跟进所有新证明，原因是AI生成证明的速度已经远超人类消化能力。
数学正在从"证明稀缺时代"进入"证明过剩时代"。真正的瓶颈，已从"如何生成证明"转移到"如何验证与理解证明"。这场验证危机的可能解法是：让AI来验证AI的证明。
这正是"形式化定理证明"的核心思想。Lean是目前最主流的形式化证明语言之一，它要求每个逻辑步骤都以机器可检验的方式写出，一旦编译通过，证明的正确性就由编译器担保。近日，普林斯顿大学研究团队发布了一篇新论文，提出了名为Goedel-Architect的智能体框架，核心模型使用的是国内开源大模型DeepSeek-V4-Flash。
500倍成本差距背后的技术革命
在形式化定理证明领域，PutnamBench是一个标准测试集，包含672道来自普特南大学生数学竞赛的题目。不同系统解决这些题目的成本差距悬殊。
此前最具竞争力的开源pipeline之一是Hilbert，由谷歌Gemini 2.5 Pro驱动。Hilbert跑完672道题，仅API调用费用就花掉了约17万美元。而Goedel-Architect完成同样评测，花费是294美元，两者相差约500倍。
更值得注意的是，Goedel-Architect的通过率为75.6%，还高于Hilbert的70.0%。新方法不仅更便宜，效果还更好。
团队还在五个基准上进行了全面测试。MiniF2F-test是最成熟的高中竞赛数学测试集，包含244道题。Goedel-Architect在pass\@1下解决了其中242道（99.2%），与此前最强开源系统持平。剩余两道IMO难题在借助自然语言证明辅助后也得以解决，使团队成为首个刷完MiniF2F-test全部244道题的系统。
在更新的竞赛题目上，系统解决了IMO 2025的4/6道题、Putnam 2025的11/12道题。USAMO 2026的出题时间晚于所有模型的训练截止日期，是真正意义上的污染免疫测试，Goedel-Architect解决了其中3/6道题。
蓝图：智能体系统的核心创新
Goedel-Architect的名字致敬了库尔特·哥德尔——那位证明了数学存在根本性局限的著名数学家。普林斯顿和哥德尔之间有深厚的历史渊源：哥德尔晚年正是在普林斯顿高等研究院度过的。
这支研究团队来自普林斯顿大学语言与智能研究中心（PLI），创始主任是计算复杂性理论权威学者Sanjeev Arora，2011年获得ACM计算奖。共同领导团队的还有陈丹琦，谷歌学术引用量逾9万次，本科毕业于清华大学，博士就读于斯坦福，师从Christopher Manning。
Goedel-Architect的核心创新在于"蓝图"（Blueprint）概念。
想象一个大型建筑项目，不同工程队同时开工，但前提是有一张完整的施工图：哪个区域先建，哪个结构依赖哪个地基，哪些可以并行推进。没有施工图，工程效率就会很低。
形式化定理证明本质上也面临同样问题。现有的许多系统采用"递归分解"方式：遇到难题就拆成更小的子目标，再递归拆分，形成一棵自上而下的树状结构。这种方法的问题在于，一旦某个分支走入死胡同，整棵树的工作就可能白费，陷入低效循环。
Goedel-Architect的做法不同。在真正开始证明之前，系统先生成一张"蓝图"：一张有向无环图，包含通向最终定理所需的所有定义和引理，以及它们之间的依赖关系。每个节点是一个精确声明的引理，每条边表明"这个引理需要依赖那个结果"。这张图是整个证明策略的全局视图。
有了蓝图，系统就可以将图中每个未证明的节点分发给Lean证明器并行处理。每个证明器只看到自己负责的引理和它声明依赖的上游结果，不被其他信息干扰。
蓝图精炼：失败是诊断信号
经过一轮并行证明，有些节点成功证明（标记为绿色），有些失败（标记为蓝色），还有些被反向证明——也就是说，这个引理本身就是假的（标记为红色）。
失败不是终点，而是"诊断信号"。这是整个框架的第三个核心部分：蓝图精炼（Blueprint Refinement）。
当某个引理节点无法被证明时，证明器会被要求写一份结构化的"事后分析报告"，包含三部分：对失败原因的诊断、尝试过的策略及其卡住的位置、以及建议的修复方案。
系统设计了两类失败模式的处理路径。
第一类是"命题有误"：如果一个引理被反向证明为假，系统会提取导致反例的具体原因，并在下一轮迭代中修改这个节点的陈述。论文中有一个典型案例：在处理Putnam 1989年的一道题时，蓝图提出了一个关于二进制表示的辅助引理——"将一个数乘以2，相当于在二进制展开的末尾追加一个零"。证明器找到了反例：Lean的数学库中，二进制位是从最低有效位开始存储的，因此乘以2实际上是在最高有效位前面加零，而不是末尾追加。一字之差，命题全错。
系统记录下"方向搞反了"的诊断，下一轮迭代直接将引理改为正确版本，并把修正传播给所有依赖该引理的节点。
第二类是"证明太难"：如果一个引理在逻辑上为真，但证明器在token预算内无法完成，系统会要求它写下"如果有更多步骤，该如何分解这个引理"。这份分解建议在下一轮迭代中被纳入蓝图，把原来一个难啃的节点拆成若干个容易处理的子节点。
已经成功证明的节点在迭代中得以保留。整个过程就像一张正在逐步完成的拼图，每一轮迭代都在已完成部分的基础上继续推进，而不是从头开始。
成本优势来自pipeline设计，而非仅仅是更好的模型
论文做了一组控制变量的对比实验，核心结论是：提升来自pipeline设计，而不仅仅是更好的模型。
团队将Hilbert（采用递归分解策略的系统）移植到相同的DeepSeek-V4-Flash骨干上运行，在MiniF2F上只能达到84.4%，而Goedel-Architect在同样骨干下达到99.2%。在PutnamBench的200题子集上，工具增强的单智能体方式以相同骨干达到54.5%，而Goedel-Architect达到76.0%，且每道题消耗的token数更少。
递归分解策略在单个子目标上反复尝试，有时会在死胡同里不断循环。全局蓝图策略则允许系统"退后一步"看整张图，在并行尝试的过程中，任何一个节点的失败都可以反馈到整个策略的调整上，不必等到整棵递归树走完。
让AI数学输出变得可信的基础设施
形式化证明系统的价值，在于提供了一种让AI数学输出变得"可信"的基础设施。当AI有一天声称证明了一个重要猜想，Lean编译器的判断比任何同行评审都更确定。
而现在Goedel-Architect更是让这套基础设施的访问门槛降低了大约两个数量级。
这项工作的技术意义是清晰的：一套成本极低的开源框架，在形式化定理证明的核心基准上达到了此前只有昂贵闭源系统才能触及的水平。对于大多数题目，这个辅助是非必需的。但对于具有"非局部结构"的难题——比如需要循环求和、奇偶性链推导、或抽象代数结构——仅从形式化命题出发推导依赖图会成为瓶颈。在这些情况下，自然语言提供的结构指引是决定性的。团队对9道此类难题进行了对照实验：在不使用自然语言辅助的情况下，每道题运行4到12次，无一成功；加入辅助后，全部解决。
AI正在以人类无法跟上的速度产出数学结论。而这套系统，正在让这些结论变得可验证、可依赖。