数学：OpenAI 的 AI 解决了 372 个问题，却没人理解它的证明

10月6日星期二，纽约时间下午六点。OpenAI 把一个包含719篇数学论文的文件夹放到了 GitHub，这个开发者分享代码的大仓库里。不是高中练习题：372个结果，解决的是一些研究人员多年来，有时甚至几十年来都没能解决的问题。全都是由 OpenAI 自己开发的一款甚至还没来得及命名的 AI 写出来的。第二天，美国最知名的计算机科学研究人员之一 Scott Aaronson 在他的博客上写道，这“肯定是数学史上最伟大的日子之一”。就这？

更糟的是，他还补充说，几乎还没有任何人类理解这些证明。

719篇论文已送达。请在这里签字，祝你校对顺利

一生的猜想，一夜之间解决

猜想，就是所有人都认为是真的，但没人成功证明的说法。在没有证明之前，它仍然只是一场赌注，即使整个行业都在押同一个方向。

OpenAI 这批东西里，有一份证明了“唯一游戏猜想”的论文，这个猜想由研究人员 Subhash Khot 在2002年提出。简单说，它认为，对于一整类问题来说，就连找出一个大致正确的答案，也和找出完美答案一样难。这听起来很抽象，但二十四年来，它一直是理论计算机科学的重大问题之一。而 Aaronson 的妻子 Dana Moshkovitz 也是一名研究人员，她整个职业生涯都在研究这个问题。

她的反应由丈夫转述出来是：这份证明“写得糟糕透顶，不借助 AI 根本不可能读懂”，而且给人的感觉是它“出自某个服用了迷幻药的人之手”。想象一下，你用人生二十年的时间研究一个问题，在淋浴时想它，在度假时想它，在家庭聚餐时想它，然后在某个星期二晚上收到答案，乱七八糟地塞在一堆你必须让另一台机器翻译才能弄明白的鬼话里，而这台机器还把你的东西拿走了。哎哟。

没人读得懂的证明，要怎么核验？

部分证明附带了用 Lean 写成的核验程序，这是一款会逐步检查数学推理的软件，只要有一点漏洞，它就拒绝继续。就像拼写检查器，不过检查的是逻辑：它不理解其中的想法，只是检查楼梯的每一级是不是稳稳地放在前一级上。

但据专业网站 Implicator 报道，截至10月7日，719份手稿中只有300份有 Lean 核验。刚刚超过十分之四。而数学家们马上指出了一个陷阱：Lean 核验的是，对于输入机器的那个表述，证明是否正确。如果有人把表述抄错了，证明可能完美无缺，却回答了另一个问题，而不是我们原本在问的问题。总之，就是在一份没人读过的卷子上盖了一个“已核验”的章。

已核验。是否理解，那是另一回事

这事没拖多久：从10月7日开始，OpenAI因为一个符号错误撤下了三篇手稿，一个本该是减号的加号，并修正了另外十四篇。这正是真正的校对能抓出来的那种问题，看到确实有人在复核，还是让人放心的。我每天都在复核 Claude Code 写的代码，非常清楚这种感觉：东西能跑，但你还不知道为什么。

解决了372个问题，但总共有多少个？

372这个数字很吓人，但得把它放回合适的位置。根据 Aaronson 的说法，AI 被用于大约8,000个问题上，每个问题大约计算三个小时，最后解决了其中约5%。也就是说，失败率是百分之九十五。所以这仍然非常不得了，因为这5%是人类此前没有解决的问题，但这并不是一台能解决交给它的一切问题的机器。而且这些结果中没有一个解决了这个领域最重大的问题。这是研究员 Lance Fortnow提醒我们的。不过，他却在这份列表里找到了一个自己在1989年的博士论文中提出过的问题。等了三十七年！

MIT 数学家 Andrew Sutherland 直截了当地说：只要 OpenAI 不公布它的模型，也没人能重做这个实验，就应该把这些说法当成未经验证的。他有一点说得很准：OpenAI 既没有公布自己的指令，也没有公布自己的模型，尽管一个为它提供咨询的数学家小组在9月底就提出了这些要求。与此同时，一个数学家协会干脆呼吁抵制 OpenAI，称这是一场「武力展示」。

Aaronson 找到了一个让人难受的比喻：数学家就像一个花了一辈子学习如何在险恶森林里生存的狩猎采集者，某天早晨却看到一座巨大的豪华酒店在自己的小屋旁边拔地而起，配有直升机停机坪和加热泳池。

花了三十年学习用两根棍子生火。对面那家酒店却有地暖

那这对你有什么用？

明天早上？一点用都没有。但看看列表里的一个结果：一种更快地把两个巨大的数字表相乘的方法，数学家把它们叫作矩阵。这是你电脑的显卡为了运行游戏、照片滤镜或 AI，每秒重复数十亿次的运算。AI 于是找到了更快地完成自己的计算的方法。它在自己给自己改装引擎！

不过，先冷静一下。从20世纪90年代开始，这类纪录几乎都只停留在纸面上：它们只有在表格大到离谱、世界上任何一台电脑都永远不可能处理它们的情况下才会变快。没人能保证这一次会例外。这可能要花十年、二十年，也可能永远不会走出期刊。

对你来说，真正的变化在别处，而且更慢：数学是其他一切建立其上的地基，从天气预报到计算桥梁的承重能力，再到浏览器里保护银行卡的那把小锁。如果一台机器让这块地基的推进速度超过几代研究人员，最终建在上面的所有东西都会从中受益。但不是今年。

其实我们已经经历过这种事了。1976年，两位研究人员借助计算机证明，只需要四种颜色，就能给任何地图上色，而且不会让两个相邻国家使用同一种颜色。计算时间超过一千小时，手工验证根本不可能。数学家们抱怨了很多年，有些人拒绝把它称为证明。2005年，它由一种和 Lean 同类的软件完成了全面复核，如今已经没人再质疑它。

1976年：四种颜色，一千小时的计算，以及二十年的坏脾气

四天前，我还在琢磨Meta的人工智能是否真的解决了五个前所未有的问题。五个！第二天，OpenAI宣布了372个。

我的看法

我觉得这很迷人，同时我也完全理解数学家的愤怒。迷人是因为那些抵抗了二十年的问题就这样被攻克了，而我们会在拆解它们的过程中学到一些东西。但一下子丢出719篇难以阅读的文章，既没有模型也没有指令，还让全世界的研究人员自己想办法筛选，这不是做科学的方式。把箱子放在门口，然后转身就走！

所以，今天早上那些正在怀疑自己是不是选对了职业的数学系学生们：你们选对了！总得有人来读完这一切，而不会是机器来做这件事！

来源

文章在Claude Code的帮助下完成，由我审阅并修正。

0 0 评论

09-10-2026