10月6日,OpenAI 在官网发布报告《Sharing AI progress in mathematics》,公开一批由内部前沿模型产出的数学新结果。这批结果放进 GitHub 仓库,附论文修订与引用协议,大量证明同步给出 Lean 形式化版本,可被计算机逐行验证。
数百个结果里有什么
据 Scientific American 报道,清单声称包含四维挂谷猜想的解、对若干最重要计算机算法的改进,以及朝黎曼假设方向的实际进展——注意是「进展」而非「解」。背景颇具戏剧性:今年菲尔茨奖得主王虹正是因证明三维挂谷猜想获奖,如今 OpenAI 的内部模型声称把同一问题推到了四维。多家科技媒体清点的口径约为 372 个问题家族、七百余篇论文,而消化这批结果预计要花数学界数月时间。
发布方式的三个变化
九月 OpenAI 放出「解决百余个开放问题」的说法后,菲尔兹奖得主们曾联名警告 AI 偏离数学本质。这次 OpenAI 按高等研究院 AGMAI 顾问组的公开建议做了改良:结果进 GitHub 带引用协议;公开 Lean 形式化;附上透明度材料——10 份模型推理摘要,以及按官方口径以 ChatGPT Pro 用量估算的算力开销,平均每个结果约相当于三小时 Pro 级思考。不过 Engadget 指出,委员会的部分建议仍被忽略:逐题算力时间与提示词都没有公开。
陶哲轩:问题不在发布,在激励
UCLA 数学家陶哲轩在社交平台发表长评(Solidot 编译)。他说数学 1.0 时代,知名难题的证明会引发演讲、研讨与精简,最终沉淀为下一代数学家的教材;而 AI 的证明由对数学兴趣不大的人用提示词「解决」,既无法出席研讨会,也无法与领域专家对话。更尖锐的判断是:AI 公司的抢发行为正迫使数学界把开创性研究秘而不宣。他的结论是,数学 2.0 时代应降低「抢先解决难题」的核心地位,把学术阐释、社区建设与开辟新方向提升为衡量进步的维度。
所以呢
Lean 验证回答「对不对」,回答不了「谁理解了它」。当机器数小时堆出数百个结果,稀缺的不再是证明本身,而是把证明变成知识的人类流程——研讨、教材、传承。OpenAI 承诺资助系列研讨会来消化结果,方向对了;但只要抢发头条的激励还在,陶哲轩担心的保密循环就不会停。这对整个 AI 行业是个通用命题:生成速度超过消化速度时,产出越快,知识负债越多。