1. OpenAI 推翻数学猜想数学领域近期受到 AI 产出的冲击。2026 年 5 月 20 日OpenAI 宣布其内部推理模型成功推翻了数学家保罗・埃尔德什于 1946 年提出的「单位距离猜想」这是困扰离散几何领域近 80 年的核心开放问题。菲尔兹奖得主蒂莫西・高尔斯表示如果 AI 能证明单位距离猜想对于数学界和科学界而言是具有划时代意义的里程碑事件若这样高质量的数学论文由人类提交给顶级学术期刊《数学年刊》他会毫不犹豫地推荐录用。2. 数学进入「证明过剩时代」同月另一位菲尔兹奖得主陶哲轩在斯坦福大学发表《新数学工作流》演讲宣布放弃实时跟进所有新证明因为 AI 生成证明的速度远超人类消化能力。他认为数学正从「证明稀缺时代」进入「证明过剩时代」真正的瓶颈已从「如何生成证明」转移到「如何验证与理解证明」。AI 以人类无法跟上的速度产出数学结论数学面临前所未有的验证危机。3. 形式化定理证明的解法与挑战可能的解法是让 AI 来验证 AI 的证明这是「形式化定理证明」的核心思想。Lean 是目前最主流的形式化证明语言之一要求每一个逻辑步骤以机器可检验的方式写出编译通过则证明的正确性由编译器担保不依赖任何人的判断。但让 AI 直接生成可通过 Lean 编译器检验的完整证明技术难度远高于生成自然语言的数学推导。4. Goedel - Architect 智能体框架发布近日普林斯顿大学研究团队发布新论文提出名为 Goedel - Architect 的智能体框架核心模型是国内开源大模型 DeepSeek - V4 - Flash。5. Goedel - Architect 的能力表现在形式化定理证明领域的标准测试集 PutnamBench 上此前最具竞争力的开源 pipeline 之一 Hilbert 由谷歌 Gemini 2.5 Pro 驱动跑完 672 道题仅 API 调用费用就花掉约 17 万美元而 Goedel - Architect 完成同样评测花费 294 美元两者相差约 500 倍。且 Goedel - Architect 在 PutnamBench 上的通过率75.6%高于 Hilbert70.0%新方法更便宜且效果更好。6. 团队背景与前期成果Goedel - Architect 名字致敬了库尔特・哥德尔普林斯顿和哥德尔有深厚历史渊源研究团队来自普林斯顿大学语言与智能研究中心PLI。PLI 创始主任 Sanjeev Arora 是计算复杂性理论领域权威学者2011 年获得 ACM 计算奖长期探索「AI 能否成为超人类数学家」问题。共同领导团队的陈丹琦来自普林斯顿计算机系谷歌学术引用量逾 9 万次本科毕业于清华大学博士就读于斯坦福师从 Christopher Manning早期和 Manning 共同开发了谷歌 SyntaxNet 底层的依存句法解析算法进入普林斯顿后聚焦语言模型相关研究。团队此前已发布两代 Goedel - Prover 用于形式化定理证明在 MiniF2F 基准上从最初的 60% 提升至 90%Goedel - Architect 是最新探索。7. Goedel - Architect 的「蓝图」概念Goedel - Architect 的关键点在于「蓝图」概念。现有许多系统采用「递归分解」方式遇到难题拆成更小的子目标形成树状结构但易陷入低效循环。Goedel - Architect 在证明前先生成一张有向无环图的「蓝图」包含通向最终定理所需的所有定义和引理及它们之间的依赖关系是整个证明策略的全局视图。有了蓝图系统将图中未证明的节点分发给 Lean 证明器并行处理证明器只看到负责的引理和其声明依赖的上游结果不受其他信息干扰。一轮并行证明后节点有成功证明绿色、失败蓝色、反向证明红色三种情况。8. 蓝图精炼机制当引理节点无法被证明时系统要求证明器写一份结构化的「事后分析报告」包含对失败原因的诊断、尝试过的策略及其卡住的位置、建议的修复方案。系统设计了两类失败模式的处理路径。第一类是「命题有误」如处理 Putnam 1989 年的题时蓝图提出的引理被证明错误系统记录诊断并在下一轮迭代中修改节点陈述修正传播给依赖该引理的节点。第二类是「证明太难」如 Putnam 1985 年的题目证明器建议按情形分类讨论下一轮迭代接受分解问题得解。已成功证明的节点在迭代中保留整个过程像逐步完成的拼图。9. Goedel - Architect 的测试表现团队在五个基准上测试了 Goedel - Architect。在 MiniF2F - test 测试集上Goedel - Architect 在 pass1 下解决了 242 道题99.2%与此前最强的开源系统持平剩余两道 IMO 难题借助自然语言证明辅助后也解决成为首个刷完 244 道题的系统。在 PutnamBench 上pass1 通过率为 75.6%超过 Hilbert借助自然语言辅助后通过率提升至 88.8%总花费不到 1000 美元。在更新的竞赛题目上解决了 IMO 2025 的 4/6 道题Putnam 2025 的 11/12 道题USAMO 2026 的 3/6 道题。10. 自然语言辅助机制Goedel - Architect 有可选的辅助机制生成初始蓝图时可提供自然语言的证明思路作为结构参考由参数更大的模型如 Gemini 3.1 Pro生成只起「脚手架」作用具体形式化实现由 Goedel - Architect 完成。对于大多数题目辅助非必需但对于具有「非局部结构」的难题自然语言提供的结构指引是决定性的团队对照实验显示不使用辅助无一成功加入辅助后全部解决。11. 对比实验结论论文的对比实验核心结论是提升来自 pipeline 设计而非仅更好的模型。将 Hilbert 移植到相同的 DeepSeek - V4 - Flash 骨干上运行在 MiniF2F 上只能达到 84.4%而 Goedel - Architect 达到 99.2%。在 PutnamBench 的 200 题子集上工具增强的单智能体方式以相同骨干达到 54.5%而 Goedel - Architect 达到 76.0%且每道题消耗的 token 数更少。递归分解策略易在死胡同循环全局蓝图策略可让系统调整策略。12. 技术意义与价值这项工作的技术意义清晰Goedel - Architect 是成本极低的开源框架在形式化定理证明的核心基准上达到了此前只有昂贵闭源系统才能触及的水平。形式化证明系统提供了让 AI 数学输出变得「可信」的基础设施Goedel - Architect 降低了这套基础设施的访问门槛约两个数量级。