文章核心观点 - 新闻核心观点是GPT-5在数学研究领域展现出实质性应用价值，通过辅助生成形式化证明和发现反例，推动了科学进步 [6][13][22][24] GPT-5在数学证明中的应用 - 两位数学家利用GPT-5在Lean中生成形式化证明并成功验证，最终证明超过6000行代码，包含26个定义、169个引理和4个定理 [13][16] - 人类研究者需不断提供反馈以完善论证，过程耗时约一周，在普通笔记本电脑上代码验证耗时不足半分钟 [16] - 陶哲轩认可此次AI辅助证明，认为这是在研究论文中负责任地使用LLM输出的罕见用例，强调Lean形式化仅是对人类证明的补充 [14][17] GPT-5在发现反例和解决开放问题中的贡献 - 加州大学欧文分校数学教授Paata Ivanisvili与合作者请GPT-5 Pro在公开未解问题中寻找反例，GPT-5提出了一个关于带擦除的非交互相关蒸馏问题的反例 [18][19][21][22] - UCLA数学教授Ernest Ryu借助GPT-5 Pro解决了一个凸优化领域的开放问题，尽管模型约80%的证明尝试错误，但提出了多条新颖思路，整个工作耗时约12小时 [24][27][29] - GPT-5的具体贡献包括给出最终可行的证明思路与论证框架，并通过快速排除无效路线大幅加速探索进程 [29] 行业影响与未来展望 - 此次GPT-5的应用被视为理论计算机科学中AI的“星星之火”，以往大语言模型多用于文献检索或数值辅助，而此次真正生成了具体、有限且可验证的反例 [24] - 研究者认为，如果大语言模型的接口能与Lean深度整合并进行微调，许多人机协作证明的问题将大大缓解，体验会更加流畅自然 [16] - OpenAI科学家Sebastien Bubeck复现了类似场景，表明GPT-5可以证明有趣的数学结论，并能筛选不正确论点、识别新推理思路以及决定探索方向 [43][44]