数学界无视「30年漏洞」，GPT-5一眼看穿！陶哲轩：AI科研革命开始了

新智元报道

编辑：KingHZ

【新智元导读】星星之火，可以燎原！证明的尊严在于可验证；这一次，GPT-5让数学证据落在了代码里。

一雪前耻，ChatGPT为OpenAI「正名」！

被Hassabis吐槽太尴尬之后，GPT-5真启发了新的数学结论。

OpenAI的科学家Sebastien Bubeck高调宣扬GPT-5破解了十道Erdős难题。

但被指出GPT并非解决了Erdős问题，而是找到了已经解决这些问题的文献。

之后，他删除了推文并表示自己并非有意误导。

Yann LeCun斥之为「自食其果」：OpenAI被他们自己的GPTards所害。

之后，他在LinkedIn上的发帖，明显低调多了：

现在，事情来了反转——

Sebastien Bubeck被「冤枉」了，AI的确在加速科学进步。

反转

ChatGPT为OpenAI「正名」

昨天，这个故事来了一个反转——

普林斯顿大学数学博士Boris Alexeev（下图左）和俄亥俄州立大学副教授Dustin G. Mixon（下图右）发现，悬赏1000美元的707号Erdős问题，在被提出前30年，就已经被解决了。

论文地址：https://borisalexeev.com/pdf/erdos707.pdf

事情有些离谱，堪称数学家的「虚空索敌」——

答案比问题早30年，但直到前不久，外界还普遍以为问题没有被解决！

目前，707号Erdős问题已被标注为「Disproved」（被证伪）。

传送门：https://www.erdosproblems.com/go_to/707

这次，Sebastien Bubeck扳回一局，发推表示：

看来文献检索，终究不是件简单的事。

潜台词是说，GPT-5过去找到的10个已有解答，并非易事。

但后面的更精彩。

ChatGPT辅助数学证明，陶哲轩点赞

两位数学家也怀疑结果，于是决定用GPT5在Lean中生成形式化证明。最后，居然成功了！

注意⚠️：ChatGPT和Lean被列入了合作者，但论文内容中还是作者「手搓」。

不过，人类在这个过程中可没少花功夫，需要不断给GPT5提供反馈，完善形式化论证。

在「Erdős的难题」网站上，近期涌现了不少成功案例，研究者利用大语言模型在现有文献中找到了埃尔德什问题的解法。

值得一提的是，用AI找到Erdős问题的「已有答案」，

陶哲轩也注意到了这次新证明，认为这是计算机辅助证明的有趣例子。

在研究过程中，两位数学家确信Lean能帮助验证已有论文的真伪，但当时既不熟悉Lean，又觉得其操作界面不够友好。

然而由于ChatGPT能编写Lean代码，他们决定通过氛围编程（vibe coding）方式形式化整个证明。

这个过程耗时约一周，体验颇为煎熬，但最终意外成功了——

形式系统中，ChatGPT严格证明了Erdős猜想的否命题。

最终生成的证明超过6000行代码，包含26个定义、169个引理和4个定理（最终的反例验证部分）。在普通笔记本电脑上，代码验证耗时不足半分钟。

经过数轮往复的互动后，Boris和Dustin认为，如果大语言模型的接口能与Lean深度整合，并针对这种交互方式进行适当微调，许多问题都会大大缓解。

即使是少量的针对性优化，也足以让这种「人机协作证明」的体验更加流畅、自然。

陶哲轩高度认可这次AI辅助证明。他表示，这是在研究论文中负责任地使用LLM输出的罕见用例之一：

重要的是，没有任何LLM生成的输出被直接放入正文（除了为了说明目的引用LLM生成的 Lean 代码片段外）；

相反，这种输出仅用于完全可验证的上下文中（在本例中，用于生成可由 Lean进行类型检查的代码）。

不过，陶哲轩强调：「Lean形式化只是对人类证明的补充，并不能取而代之。」

此外，他几乎可以预见会有一些夸张的报道——「这回LLM真解决了一个Erdős问题！」

—— 但事实远比这复杂微妙。要得出任何结论，都需要先把来龙去脉仔细梳理清楚。

GPT-5推动研究，端倪初现

加州大学欧文分校数学教授Paata Ivanisvili，也把ChatGPT列为论文合作者。

新论文由数学教授Paata Ivanisvili、2022届中科大本科校友Xinyuan Xie (谢新元)合作，ChatGPT是第一作者。

这一探索起源于两人请GPT-5 Pro在公开的未解问题（下文）中寻找反例。

链接：https://simons.berkeley.edu/sites/default/files/openprobsmerged.pdf

标题：Real Analysis in Computer Science：A collection of Open Problems

经过若干数值实验后，它提出了一个关于带擦除的非交互相关蒸馏问题（Non-Interactive Correlation Distillation, NICD with erasures）的反例：

一个定义在5比特上的布尔函数，在擦除参数p=0.40时，其 E∣f(z)∣值 严格大于 5比特多数函数（majority function）的对应值。

他们记录了这一发现并验证全部计算过程。

这一结果与线性阈值函数中关于「Majority is Least Stable」的经典反例，形成了呼应：即便AI只是将已知的反例模式应用于新场景并加以验证，其贡献依然值得肯定。

传送门：https://arxiv.org/abs/1703.07657

这是理论计算机科学中AI的「星星之火」：以往大语言模型（LLMs）多用于文献检索或数值辅助，而此次则真正生成了一个具体、有限且可验证的反例。

此外，UCLA的数学教授Ernest Ryu，借助GPT-5 Pro解决了一个凸优化领域的开放问题。

尽管模型约有80%的证明尝试是错误的，却提出了多条新颖思路。

GPT-5 Pro的具体贡献：

• 给出了最终可行的证明思路与论证框架

• 通过快速排除无效路线，大幅加速了探索进程

这项工作耗时约12小时，分3天完成。事后，Ernest Ryu回想起来，这个证明其实非常简单。

ChatGPT生成的证明的关键步骤：

可以上下滚动的图片

Ernest Ryu总结了他自己的贡献：

• 筛选出不正确的论点，并积累一系列正确的事实。

• 识别有前景的新推理思路，并引导 ChatGPT 进一步探索这些思路

• 认识到何时某个策略已被充分探索，并决定何时转向其他方向。

他还将继续开发这个项目，并将结果发表在专业的优化理论期刊上，并分享更新和未来的部分。

被吐槽的OpenAI科学家Sebastien Bubeck，也复现了类似的场景——

GPT-5可以证明有趣的数学结论。

不过，人类实际上抢先了gpt-5 一步:-)。另一位作者完全填补了差距，证明了新的界限。

GPT-5提出的证明：

GPT-5已经提出了多个具有研究价值的新想法。不仅如此，它实际上自己想出了大部分提示词：

传送门：https://github.com/Dicklesworthstone/model_guided_research

AI辅助研究大门，正在打开。

或许，历史铭记的不是那句「太尴尬了」，而是那行悄无声息通过编译的qed。

参考资料：

https://x.com/SebastienBubeck/status/1980804267524116569

https://x.com/PI010101/status/1981014478969033156

https://borisalexeev.com/pdf/erdos707.pdf

https://mathstodon.xyz/@tao/115416211466664814

https://x.com/slow_developer/status/1980990021248160009