本文来自微信公众号： 机器之心 ，编辑：Panda、泽南，作者：AI做题的
数学领域，最近着实被AI的产出冲击到了。
2026年5月20日，OpenAI宣布，其内部推理模型成功推翻了由数学家保罗・埃尔德什（Paul Erdős）于1946年提出的「单位距离猜想」——一个困扰离散几何领域近80年的核心开放问题。
菲尔兹奖得主蒂莫西・高尔斯（Timothy Gowers）对此表示：「如果AI能证明单位距离猜想，对于数学界和科学界而言是一个具有划时代意义的里程碑事件……这样高质量的数学论文如果是由人类提交给顶级学术期刊《数学年刊》的话，我会毫不犹豫地推荐录用。」
就在同一个月，另一位菲尔兹奖得主陶哲轩在斯坦福大学发表了一场题为《新数学工作流》的演讲。他宣布，自己已经放弃实时跟进所有新证明，AI生成证明的速度已经远超人类消化能力。他的判断更直接：数学正在从「证明稀缺时代」进入「证明过剩时代」，真正的瓶颈，已经从「如何生成证明」转移到了「如何验证与理解证明」。
这句话值得停下来想一想。AI正在以人类无法跟上的速度产出数学结论，而我们越来越难以判断这些结论是否真的站得住脚。数学这门最讲究严格性的学科，正面临一场前所未有的验证危机。
可能的解法是：让AI来验证AI的证明。
这正是「形式化定理证明」的核心思想。Lean是目前最主流的形式化证明语言之一，它要求每一个逻辑步骤都以机器可检验的方式写出，一旦编译通过，证明的正确性就由编译器担保，不依赖任何人的判断。但这也带来了新的挑战：让AI直接生成可通过Lean编译器检验的完整证明，技术难度远高于生成自然语言的数学推导。
近日，普林斯顿大学的研究团队发布了一篇新论文，提出了一个名为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，由谷歌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是他们在「如何用智能体框架组织证明过程」这一维度上的最新探索。
在新研究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%），与此前最强的开源系统持平。剩余两道（均为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次，无一成功；加入辅助后，全部解决。
论文做了一组控制变量的对比实验，核心结论是：提升来自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更是让这套基础设施的访问门槛降低了大约两个数量级。