index_new5.html
../../../zaker_core/zaker_tpl_static/wap/tpl_guoji1.html
![]()
近期，AI在数学研究领域展现出令人瞩目的进展。最初，GPT-5被指破解Erdős难题，后因误解文献而被撤回，引发争议。然而，事情出现反转，AI被证实能够加速科学发现。两位数学家利用ChatGPT辅助，成功生成了对Erdős悬赏问题的形式化证明，并将其标注为“已被证伪”，证明答案比问题提出早了30年。此外，AI还在寻找未解问题的反例以及在凸优化领域提供新的证明思路，尽管过程中存在错误，但其加速研究进程和提供新颖想法的潜力已初步显现。AI正从文献检索和数值辅助，转向生成可验证的反例和证明框架，标志着AI辅助研究的大门正在开启。
💡 AI正成为数学研究的有力助手。最初关于GPT-5破解Erdős难题的说法虽有误，但后续发展表明AI确实能加速科学发现，例如通过辅助生成形式化证明，有效验证数学猜想的真伪。
✅ AI在数学研究中的角色正在深化。通过与ChatGPT等工具的协作，研究者能够生成超过6000行的代码来形式化证明，这不仅验证了现有理论，还为数学界发现“答案比问题早30年”的情况提供了新视角。
🚀 AI正推动理论计算机科学的研究前沿。AI不再局限于文献检索或数值辅助，而是能够生成具体、可验证的反例，并为凸优化等领域的开放问题提供新的证明思路和论证框架，加速了研究进程。
🤝 AI与人类研究者的协作模式日益成熟。尽管AI可能产生错误尝试，但通过人类的筛选、引导和反馈，AI能够识别有前景的新推理思路，并最终导向可行的证明，这种“人机协作证明”的模式预示着未来研究的新方向。
【新智元导读】星星之火，可以燎原！证明的尊严在于可验证；这一次，GPT-5让数学证据落在了代码里。一雪前耻，ChatGPT为OpenAI「正名」！被Hassabis吐槽太尴尬之后，GPT-5真启发了新的数学结论。OpenAI的科学家Sebastien Bubeck高调宣扬GPT-5破解了十道Erdős难题。但被指出GPT并非解决了Erdős问题，而是找到了已经解决这些问题的文献。之后，他删除了推文并表示自己并非有意误导。GPT-5破解世纪难题，竟是上网抄来的！哈萨比斯：太尴尬了。
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_researchAI辅助研究大门，正在打开。或许，历史铭记的不是那句「太尴尬了」，而是那行悄无声息通过编译的qed。https://x.com/SebastienBubeck/status/1980804267524116569https://x.com/PI010101/status/1981014478969033156https://borisalexeev.com/pdf/erdos707.pdfhttps://mathstodon.xyz/@tao/115416211466664814https://x.com/slow_developer/status/1980990021248160009 文章原文
