AI冲击数学领域在数学领域最近着实被AI的产出冲击到了。2026年5月20日OpenAI宣布其内部推理模型成功推翻了由数学家保罗・埃尔德什Paul Erdős于1946年提出的「单位距离猜想」这可是一个困扰离散几何领域近80年的核心开放问题。菲尔兹奖得主蒂莫西・高尔斯Timothy Gowers对此评价颇高他说“如果AI能证明单位距离猜想对于数学界和科学界而言是一个具有划时代意义的里程碑事件……这样高质量的数学论文如果是由人类提交给顶级学术期刊《数学年刊》的话我会毫不犹豫地推荐录用。”数学进入「证明过剩时代」就在同一个月另一位菲尔兹奖得主陶哲轩在斯坦福大学发表了一场题为《新数学工作流》的演讲。他宣布自己已经放弃实时跟进所有新证明因为AI生成证明的速度已经远超人类消化能力。他更直接地判断数学正在从「证明稀缺时代」进入「证明过剩时代」真正的瓶颈已经从「如何生成证明」转移到了「如何验证与理解证明」。这意味着AI正在以人类无法跟上的速度产出数学结论而我们越来越难以判断这些结论是否真的站得住脚数学这门最讲究严格性的学科正面临一场前所未有的验证危机。可能的解法让AI验证AI的证明可能的解法是让AI来验证AI的证明这正是「形式化定理证明」的核心思想。Lean是目前最主流的形式化证明语言之一它要求每一个逻辑步骤都以机器可检验的方式写出一旦编译通过证明的正确性就由编译器担保不依赖任何人的判断。但这也带来了新的挑战让AI直接生成可通过Lean编译器检验的完整证明技术难度远高于生成自然语言的数学推导。Goedel-Architect智能体框架登场近日普林斯顿大学的研究团队发布了一篇新论文提出了一个名为Goedel-Architect的智能体框架。他们用的核心模型是国内开源大模型DeepSeek-V4-Flash。Goedel-Architect的能力表现在形式化定理证明领域有一个标准测试集叫PutnamBench包含672道来自普特南大学生数学竞赛的题目。此前最具竞争力的开源pipeline之一是Hilbert由谷歌Gemini 2.5 Pro驱动跑完这672道题仅API调用费用就花掉了约17万美元。而Goedel-Architect完成同样的评测花费是294美元两者相差约500倍。更值得注意的是Goedel-Architect在PutnamBench上的通过率75.6%还高于Hilbert70.0%新方法更便宜了效果还更好。团队背景与研究渊源这个系统的名字「Goedel-Architect」致敬了库尔特・哥德尔那位证明了数学存在根本性局限的著名数学家。普林斯顿和哥德尔之间有深厚的历史渊源哥德尔晚年正是在普林斯顿高等研究院度过的而这支研究团队就来自普林斯顿大学语言与智能研究中心Princeton Language and IntelligencePLI。PLI的创始主任是Sanjeev Arora一位计算复杂性理论领域的权威学者2011年获得ACM计算奖。他长期致力于探索「AI能否成为超人类数学家」这一问题。他曾在海德堡桂冠论坛上公开阐述这条路径用Lean这样的形式化系统作为锚点让AI的「幻觉」倾向无处遁形因为编译器不会接受一个逻辑上有漏洞的证明。共同领导这支团队的还有陈丹琦同样来自普林斯顿计算机系谷歌学术引用量逾9万次。她本科毕业于清华大学博士就读于斯坦福师从Christopher Manning。她最广为人知的早期工作之一是和Manning共同开发了谷歌SyntaxNet底层的依存句法解析算法。进入普林斯顿后她长期聚焦语言模型的训练与适配、知识表示与推理以及问答系统的大规模构建。这支团队此前已发布过两代Goedel-Prover专门用于形式化定理证明的开源模型系列在MiniF2F基准上从最初的60%不断提升至90%。Goedel-Architect是他们在「如何用智能体框架组织证明过程」这一维度上的最新探索。Goedel-Architect的核心「蓝图」概念在新研究Goedel-Architect上关键点在于「蓝图」blueprint概念。想象一个大型建筑项目不同的工程队同时开工但前提是有一张完整的施工图明确哪个区域先建哪个结构依赖哪个地基哪些可以并行推进。没有施工图工程的效率就会很低。形式化定理证明本质上也是如此。现有的许多系统采用「递归分解」的方式遇到一个难题就把它拆成更小的子目标再递归拆分形成一棵自上而下的树状结构。这种方法的问题在于一旦某个分支走入死胡同整棵树的工作就可能白费陷入低效循环。Goedel-Architect的做法不同。在真正开始证明之前系统先生成一张「蓝图」这是一张有向无环图包含通向最终定理所需的所有定义和引理以及它们之间的依赖关系。每个节点是一个精确声明的引理每条边表明「这个引理需要依赖那个结果」。这张图是整个证明策略的全局视图。有了蓝图系统就可以将图中每个未证明的节点分发给Lean证明器并行处理。每个证明器只看到自己负责的引理和它声明依赖的上游结果不被其他信息干扰。经过一轮并行证明有些节点成功证明标记为绿色有些失败标记为蓝色还有些被反向证明也就是说这个引理本身就是假的标记为红色。蓝图精炼处理失败节点失败不是终点而是「诊断信号」。这是整个框架的第三个核心部分蓝图精炼blueprint refinement。当某个引理节点无法被证明时系统并不是简单地记录失败。证明器会被要求写一份结构化的「事后分析报告」包含三部分对失败原因的诊断是命题本身有误还是证明思路太难、尝试过的策略及其卡住的位置、以及建议的修复方案。系统设计了两类失败模式的处理路径。第一类是「命题有误」如果一个引理被反向证明为假系统会提取导致反例的具体原因并在下一轮迭代中修改这个节点的陈述。论文中有一个案例在处理Putnam 1989年的一道题时蓝图提出了一个关于二进制表示的辅助引理「将一个数乘以2相当于在二进制展开的末尾追加一个零」。证明器在n5时找到了反例Lean的数学库中二进制位是从最低有效位开始存储的因此乘以2实际上是在最高有效位前面加零而不是末尾追加。一字之差命题全错。系统记录下这个「方向搞反了」的诊断下一轮迭代直接将引理改为正确版本并把这个修正传播给所有依赖该引理的节点。第二类是「证明太难」如果一个引理在逻辑上为真但证明器在token预算内无法完成系统会要求它写下「如果有更多步骤该如何分解这个引理」。这份分解建议在下一轮迭代中被纳入蓝图把原来一个难啃的节点拆成若干个容易处理的子节点。论文介绍了一道Putnam 1985年的题目一个关于五次多项式根的引理证明器认为正确但无力完成于是建议按四种情形分类讨论。下一轮迭代接受了这个分解所有子情形都顺利证明问题得解。已经成功证明的节点在迭代中得以保留。整个过程就像一张正在逐步完成的拼图每一轮迭代都在已完成部分的基础上继续推进而不是从头开始。Goedel-Architect的测试表现团队在五个基准上测试了Goedel-Architect。MiniF2F-test是最成熟的高中竞赛数学测试集包含244道题。Goedel-Architect在pass1下解决了其中242道99.2%与此前最强的开源系统持平。剩余两道均为IMO难题在借助自然语言证明辅助后也得以解决使团队成为首个刷完MiniF2F-test全部244道题的系统。PutnamBench上的表现已在前文提及75.6%的pass1通过率超过在16万美元预算下运行的Hilbert70.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数更少。递归分解策略在单个子目标上反复尝试有时会在死胡同里不断循环。全局蓝图策略则允许系统「退后一步」看整张图在并行尝试的过程中任何一个节点的失败都可以反馈到整个策略的调整上不必等到整棵递归树走完。Goedel-Architect的技术意义这项工作的技术意义是清晰的一套成本极低的开源框架在形式化定理证明的核心基准上达到了此前只有昂贵闭源系统才能触及的水平。形式化证明系统的价值在于提供了一种让AI数学输出变得「可信」的基础设施。当AI有一天声称证明了一个重要猜想Lean编译器的判断比任何同行评审都更确定。而现在Goedel-Architect更是让这套基础设施的访问门槛降低了大约两个数量级。
Goedel-Architect：低成本开源框架，让形式化定理证明更高效！
AI冲击数学领域在数学领域最近着实被AI的产出冲击到了。2026年5月20日OpenAI宣布其内部推理模型成功推翻了由数学家保罗・埃尔德什Paul Erdős于1946年提出的「单位距离猜想」这可是一个困扰离散几何领域近80年的核心开放问题。菲尔兹奖得主蒂莫西・高尔斯Timothy Gowers对此评价颇高他说“如果AI能证明单位距离猜想对于数学界和科学界而言是一个具有划时代意义的里程碑事件……这样高质量的数学论文如果是由人类提交给顶级学术期刊《数学年刊》的话我会毫不犹豫地推荐录用。”数学进入「证明过剩时代」就在同一个月另一位菲尔兹奖得主陶哲轩在斯坦福大学发表了一场题为《新数学工作流》的演讲。他宣布自己已经放弃实时跟进所有新证明因为AI生成证明的速度已经远超人类消化能力。他更直接地判断数学正在从「证明稀缺时代」进入「证明过剩时代」真正的瓶颈已经从「如何生成证明」转移到了「如何验证与理解证明」。这意味着AI正在以人类无法跟上的速度产出数学结论而我们越来越难以判断这些结论是否真的站得住脚数学这门最讲究严格性的学科正面临一场前所未有的验证危机。可能的解法让AI验证AI的证明可能的解法是让AI来验证AI的证明这正是「形式化定理证明」的核心思想。Lean是目前最主流的形式化证明语言之一它要求每一个逻辑步骤都以机器可检验的方式写出一旦编译通过证明的正确性就由编译器担保不依赖任何人的判断。但这也带来了新的挑战让AI直接生成可通过Lean编译器检验的完整证明技术难度远高于生成自然语言的数学推导。Goedel-Architect智能体框架登场近日普林斯顿大学的研究团队发布了一篇新论文提出了一个名为Goedel-Architect的智能体框架。他们用的核心模型是国内开源大模型DeepSeek-V4-Flash。Goedel-Architect的能力表现在形式化定理证明领域有一个标准测试集叫PutnamBench包含672道来自普特南大学生数学竞赛的题目。此前最具竞争力的开源pipeline之一是Hilbert由谷歌Gemini 2.5 Pro驱动跑完这672道题仅API调用费用就花掉了约17万美元。而Goedel-Architect完成同样的评测花费是294美元两者相差约500倍。更值得注意的是Goedel-Architect在PutnamBench上的通过率75.6%还高于Hilbert70.0%新方法更便宜了效果还更好。团队背景与研究渊源这个系统的名字「Goedel-Architect」致敬了库尔特・哥德尔那位证明了数学存在根本性局限的著名数学家。普林斯顿和哥德尔之间有深厚的历史渊源哥德尔晚年正是在普林斯顿高等研究院度过的而这支研究团队就来自普林斯顿大学语言与智能研究中心Princeton Language and IntelligencePLI。PLI的创始主任是Sanjeev Arora一位计算复杂性理论领域的权威学者2011年获得ACM计算奖。他长期致力于探索「AI能否成为超人类数学家」这一问题。他曾在海德堡桂冠论坛上公开阐述这条路径用Lean这样的形式化系统作为锚点让AI的「幻觉」倾向无处遁形因为编译器不会接受一个逻辑上有漏洞的证明。共同领导这支团队的还有陈丹琦同样来自普林斯顿计算机系谷歌学术引用量逾9万次。她本科毕业于清华大学博士就读于斯坦福师从Christopher Manning。她最广为人知的早期工作之一是和Manning共同开发了谷歌SyntaxNet底层的依存句法解析算法。进入普林斯顿后她长期聚焦语言模型的训练与适配、知识表示与推理以及问答系统的大规模构建。这支团队此前已发布过两代Goedel-Prover专门用于形式化定理证明的开源模型系列在MiniF2F基准上从最初的60%不断提升至90%。Goedel-Architect是他们在「如何用智能体框架组织证明过程」这一维度上的最新探索。Goedel-Architect的核心「蓝图」概念在新研究Goedel-Architect上关键点在于「蓝图」blueprint概念。想象一个大型建筑项目不同的工程队同时开工但前提是有一张完整的施工图明确哪个区域先建哪个结构依赖哪个地基哪些可以并行推进。没有施工图工程的效率就会很低。形式化定理证明本质上也是如此。现有的许多系统采用「递归分解」的方式遇到一个难题就把它拆成更小的子目标再递归拆分形成一棵自上而下的树状结构。这种方法的问题在于一旦某个分支走入死胡同整棵树的工作就可能白费陷入低效循环。Goedel-Architect的做法不同。在真正开始证明之前系统先生成一张「蓝图」这是一张有向无环图包含通向最终定理所需的所有定义和引理以及它们之间的依赖关系。每个节点是一个精确声明的引理每条边表明「这个引理需要依赖那个结果」。这张图是整个证明策略的全局视图。有了蓝图系统就可以将图中每个未证明的节点分发给Lean证明器并行处理。每个证明器只看到自己负责的引理和它声明依赖的上游结果不被其他信息干扰。经过一轮并行证明有些节点成功证明标记为绿色有些失败标记为蓝色还有些被反向证明也就是说这个引理本身就是假的标记为红色。蓝图精炼处理失败节点失败不是终点而是「诊断信号」。这是整个框架的第三个核心部分蓝图精炼blueprint refinement。当某个引理节点无法被证明时系统并不是简单地记录失败。证明器会被要求写一份结构化的「事后分析报告」包含三部分对失败原因的诊断是命题本身有误还是证明思路太难、尝试过的策略及其卡住的位置、以及建议的修复方案。系统设计了两类失败模式的处理路径。第一类是「命题有误」如果一个引理被反向证明为假系统会提取导致反例的具体原因并在下一轮迭代中修改这个节点的陈述。论文中有一个案例在处理Putnam 1989年的一道题时蓝图提出了一个关于二进制表示的辅助引理「将一个数乘以2相当于在二进制展开的末尾追加一个零」。证明器在n5时找到了反例Lean的数学库中二进制位是从最低有效位开始存储的因此乘以2实际上是在最高有效位前面加零而不是末尾追加。一字之差命题全错。系统记录下这个「方向搞反了」的诊断下一轮迭代直接将引理改为正确版本并把这个修正传播给所有依赖该引理的节点。第二类是「证明太难」如果一个引理在逻辑上为真但证明器在token预算内无法完成系统会要求它写下「如果有更多步骤该如何分解这个引理」。这份分解建议在下一轮迭代中被纳入蓝图把原来一个难啃的节点拆成若干个容易处理的子节点。论文介绍了一道Putnam 1985年的题目一个关于五次多项式根的引理证明器认为正确但无力完成于是建议按四种情形分类讨论。下一轮迭代接受了这个分解所有子情形都顺利证明问题得解。已经成功证明的节点在迭代中得以保留。整个过程就像一张正在逐步完成的拼图每一轮迭代都在已完成部分的基础上继续推进而不是从头开始。Goedel-Architect的测试表现团队在五个基准上测试了Goedel-Architect。MiniF2F-test是最成熟的高中竞赛数学测试集包含244道题。Goedel-Architect在pass1下解决了其中242道99.2%与此前最强的开源系统持平。剩余两道均为IMO难题在借助自然语言证明辅助后也得以解决使团队成为首个刷完MiniF2F-test全部244道题的系统。PutnamBench上的表现已在前文提及75.6%的pass1通过率超过在16万美元预算下运行的Hilbert70.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数更少。递归分解策略在单个子目标上反复尝试有时会在死胡同里不断循环。全局蓝图策略则允许系统「退后一步」看整张图在并行尝试的过程中任何一个节点的失败都可以反馈到整个策略的调整上不必等到整棵递归树走完。Goedel-Architect的技术意义这项工作的技术意义是清晰的一套成本极低的开源框架在形式化定理证明的核心基准上达到了此前只有昂贵闭源系统才能触及的水平。形式化证明系统的价值在于提供了一种让AI数学输出变得「可信」的基础设施。当AI有一天声称证明了一个重要猜想Lean编译器的判断比任何同行评审都更确定。而现在Goedel-Architect更是让这套基础设施的访问门槛降低了大约两个数量级。
