OpenAI又让数学界面对AI证明的新考题?722份手稿的裂痕:Lean校验得了逻辑,守不住翻译

据《商业内幕》10 日上午报道,OpenAI最新公布的大批数学研究成果在学术界引发了不同反应。有人振奋于突破,有人忧心合作传统。Lean守得住逻辑,守不住翻译。算力可批量生成证明,人的核验注意力不能。


722。719。

两个数字之间,只隔了不到一天。

数学大爆炸!OpenAI 一夜攻克722个数学难题,准黎曼猜想已被证明

当地时间10月6日,OpenAI在GitHub公开openai/math。722份数学手稿,372个问题家族,横跨数论、代数几何、组合与理论计算机。产出方是一个没有名字、没有API、也没有同行评审流程的内部模型。

最先被看见的是两份挂谷手稿。一份175页,指向四维:任何包含所有方向单位线段的四维集合,都有满的Hausdorff维数。另一份97页,回到三维,瞄准比王虹与Zahl的集合定理更强的极大函数猜想。

措辞需要停在这里。这是声称证明,不是已证。372个家族中,只有235个附有Lean形式化链接,其余一百多份,仍是自然语言。


麻烦也恰恰藏在这条缝里。

10月7日,一篇arXiv论文逐行对比了OpenAI纳维-斯托克斯手稿的两个版本:自然语言稿里要求m+4阶导数,Lean代码里悄悄变成了m+5;证明策略被整体替换。编译全部通过,但两个世界证明的,未必是同一个命题。同日,OpenAI自己撤回了3份手稿、修订14篇、更新13篇引用。起因是霍奇家族一份基础手稿里的一个符号错误,一个正负号,顺藤摸瓜拖垮了依赖链上的另外两篇。

这是一次昂贵的公开课:Lean守得住形式世界内部的逻辑,守不住两个世界之间那段翻译。

而真正让数学界坐不住的,还不是错,是形式。

722份手稿,作者栏统一写着OpenAI。没有人类署名,没有单篇时间戳,没有arXiv式的预印本秩序。对照组随手就有:同一个挂谷猜想,王虹与Zahl从2022年粘性情形走到2025年2月的127页完整证明,将近四年,每一步都有名字、有日期、可以被引用、可以被追讨。

王虹攻克三维挂谷猜想OpenAI发布175页四维证明论文


于是发布次日,制度性的反应比学术讨论来得更快。

人类数学协会(AHM)通讯工作组发出声明,呼吁数学家停止与OpenAI合作;陶哲轩次日以客座博文转发。

媒体称之为抵制,但声明没有强制机制,更像一次立界桩。

集合论学者Karagila走得更远:他公开拒绝承认OpenAI关于划分原理的预印本,理由是结构混乱,并把这种批量发布比作对专家的拒绝服务攻击。巴克马斯特的疑问则指向另一条暗河。

数学家的基金申请书,会不会在评审环节被输入模型,再以谁也认不出的样子回来?

温和的一端同样在收紧。此前OpenAI自己的数学顾问小组曾建议前沿公司不要在内部模型上测试高等数学问题,但项目依旧在10月6日如期发布;小组索要的提示词没有给,仓库的GitHub Issues被关闭。顾问组织随后的表态很克制,只留下一句警告:数学研究的未来,不能变成替实验室清理产出。


而在所有争论的底层,产业曲线已经悄悄改了斜率。

OpenAI发言人称,这次几乎全部成果,来自 交给单一智能体的一个提示词 。

要知道,9月的纳维-斯托克斯项目动用的是上万智能体、烧掉数百万美元;两个月后,平均每个被接受的成果,账面上只剩约三小时算力。三小时不是思考时长,是筛选、试证、回溯多轮迭代之后的平均账单。

这个降本幅度,比372个家族里的任何一篇都更像分水岭:长任务智能体已经从演示场景,走进了纯理论科研的深水区。

OpenAI搅乱数学界!科研项目没了,数学家遭毁灭性打击,学界还要数年消化

分歧的两端,其实共享同一个判断。

Karagila们担心的是注意力:顶尖数学家的人力有限,722份候选证明等着人读,海量草稿会淹没真正有价值的人类工作。王虹的表态则被广泛转发。AI更像需要被驾驭的工具,而非对手;它让研究更具主动性。两种说法不矛盾:算力可以批量生成候选证明,人类共同体的 核验注意力 却无法批量扩产。

所以这件事最后剩下的问题,朴素得近乎陈旧。

一条数学结论,什么时候算成立?

是模型输出时,是Lean编译通过时,是专家愿意写下我读过时,还是它被别人的证明反复使用之后?当产量第一次超过注意力,数学界不能只靠旧速度表达新不安。


发布不到24小时,OpenAI自己撤回了3份。

这不丢人。丢人的是,如果下一次没有人来得及发现那个正负号。

- END -


本文来源于DOIT传媒,文章内容仅供参考,不构成投资建议。

赞 ()

相关推荐

发表回复

评论列表

点击查看更多

    联系我们

    微信:百易小助手

    邮件:contact@doit.com.cn

    工作时间:周一至周五,9:30-18:30,节假日休息

    微信