AI在数学证明领域的突破与影响 - AI在数学领域产出速度已远超人类消化能力，数学正从“证明稀缺时代”进入“证明过剩时代”，验证与理解证明成为新瓶颈[1] - OpenAI内部推理模型于2026年5月推翻了困扰离散几何领域近80年的“单位距离猜想”，被菲尔兹奖得主评价为具有划时代意义的里程碑[1] 形式化定理证明的解决方案：Goedel-Architect - 普林斯顿大学研究团队提出名为Goedel-Architect的智能体框架，其核心是使用形式化证明语言Lean，通过机器可检验的方式确保证明正确性[2] - 该框架采用“蓝图”概念，在证明前生成包含所有定义、引理及依赖关系的有向无环图，从而实现并行处理与全局策略调整[7][9] - 框架包含“蓝图精炼”机制，能对证明失败的节点进行结构化诊断，并根据失败原因（命题有误或证明太难）采取修复或分解策略[10][11][12] Goedel-Architect的性能与成本优势 - 在标准测试集PutnamBench（672道题）上，Goedel-Architect的通过率达75.6%，高于此前由谷歌Gemini 2.5 Pro驱动的Hilbert系统（70.0%）[3][4] - 完成PutnamBench评测的总花费仅为294美元，而Hilbert系统的API调用费用约为17万美元，成本相差约500倍[3][16] - 在借助自然语言证明辅助后，该系统在PutnamBench上的通过率进一步提升至88.8%（解决597/672题），总花费仍低于1000美元[15] 在多项数学竞赛基准上的表现 - 在MiniF2F-test（244道高中竞赛题）上，Goedel-Architect在pass@1设置下解决了242道题（99.2%），与最强开源系统持平[14] - 借助自然语言辅助后，成为首个完全解决MiniF2F-test全部244道题的系统[14] - 在更新的竞赛题上，解决了IMO 2025的4/6道题、Putnam 2025的11/12道题，以及在污染免疫测试USAMO 2026上解决了3/6道题[15][17] 技术架构与创新价值 - 性能提升主要源于pipeline设计创新，而非仅依赖更好的模型。在相同骨干模型（DeepSeek-V4-Flash）下，Goedel-Architect在MiniF2F上达到99.2%，而采用递归分解策略的Hilbert移植版仅为84.4%[18] - 蓝图策略允许全局视图和并行处理，避免了递归分解策略易陷入局部死循环的低效问题[9][18] - 该框架将形式化定理证明基础设施的访问成本降低了约两个数量级，使高质量、可验证的AI数学证明变得更为经济可行[19][20] 团队背景与核心模型 - 研究团队来自普林斯顿大学语言与智能研究中心（PLI），由计算复杂性理论权威Sanjeev Arora和知名学者陈丹琦共同领导[4][5] - 团队此前已发布Goedel-Prover系列开源模型，在MiniF2F基准上的性能从60%提升至90%[6] - 系统的核心模型采用了国内开源大模型DeepSeek-V4-Flash[2]