【导读】星星之火，可以燎原！证明的尊严在于可验证；这一次，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
本文来自微信公众号“新智元”，编辑：KingHZ ，36氪经授权发布。
