美东时间10月6日傍晚6点，OpenAI发布的719篇数学手稿，刚撤了3篇，改了14篇，剩下的归在372个成果类别，啃下了四维Kakeya猜想、广义黎曼猜想这些顶级数学硬骨头。
3小时算力，换一个“数学证明”？
OpenAI称，每项成功结果的算力，相当于ChatGPT Pro思考3小时。但这个说法的背景，绕不开9月那场沸沸扬扬的优先权争议：9月1日，OpenAI启动智能体系统；9月5日，首批智能体约88小时后出结果，再花17小时用GPT-6 Astra做Lean形式化验证，整个过程发了490万条消息，耗了3000亿输出token；9月8日，OpenAI官宣解决纳维-斯托克斯千禧年难题（克雷数学研究所悬赏100万美元，他们没领）；可就在官宣12小时前，纽约大学数学家特里斯坦·巴克马斯特和Anthropic的合作者已公开了相近成果——这两人8月15日得出关键结果，8月22日完成Lean验证。巴克马斯特直言，OpenAI是“听到传闻就砸大量AI代理跟进”，处理成果发布、署名和优先权的方式有问题，OpenAI否认使用他们的私人数据。
Lean证明≠真证明，这是个坑
OpenAI这次只公布了平均3小时的算力，既没给提示词，也没公开模型和具体计算过程。米兰比可卡大学副教授瓦莱里奥·卡普拉罗已揪出两处关键差异：OpenAI的论文和Lean代码里，一个估计所需的输入导数数量不同，压力-通量估计的界限和证明方法也不一样。更核心的问题是：Lean验证只能查形式上的逻辑错误，没法证明结果真的对应那个数学难题，也没法判断成果有没有新意。MIT数学家安德鲁·萨瑟兰说得直接：“除非他们公布模型让人复现，不然所有‘单个智能体一次性解决问题’的说法，都得算未经证实。”数学界对难题的认可，从来靠的是同行逐字逐句的验证，不是AI的一次输出。
数学界怕的不是AI，是“证明过剩”
这次OpenAI一下扔700多篇手稿，等于把数学界消化成果的慢流程给压碎了：开普勒猜想的形式化验证用了10多年，四色定理的信任过程持续了几十年，有限单群分类定理更是几代人的积累。现在数学家连700多篇手稿的零头都读不完，更别说逐一验证。有人吐槽这是“把未经证实的工作倾倒给数学家”，也有乐观派，比如多伦多大学的丹尼尔·利特：“只要成果靠谱，对数学发展就是好事。”但陶哲轩的话戳中了痛点：数学不止要答案，更要概念理解、理论发展。当AI批量生产“证明”，人类要扛的不只是验证，还有怎么把这些成果纳入人类的知识体系——毕竟，数学家需要的是“能往前走的问题”，不是一堆堆没头没尾的草稿。
当AI能批量输出号称“解决顶级数学难题”的证明时，我们要的是“能复现的正确结果”，还是“能推动认知边界的新思考”？
素材来源：钛媒体 · AI情报、AI行业观察
查看报道原文
发表第一条评论吧