GPT-6 的孪生素数进展

GPT-6 Astra 发布后，OpenAI 称其用 Lean 形式化证明把孪生素数猜想中“存在无穷多对连续素数，间距不超过某上界”的上界从 246 推到 186。同期 Anthropic 与 Axiom 也宣布把上界缩小到 188 与 212。就在 8 月 31 日，牛津数学家 Julia Stadlmann 刚凭借对大平滑模数的新估计把上界压到 240。

陶哲轩对此的评论是：“这可真是令人无语的一幕。”他同时庆幸 Stadlmann 赶在问题被“污染”之前公开了自己的分析，否则她为带大平滑因子整数构造等分布估计的思路可能被埋没。

担忧不只是“答案由 AI 给出”

在长文中，陶哲轩以纳维-斯托克斯方程全局正则性问题为例展开：数学家公认的路线是先设计近似自相似的爆破拟设，再逐步验证其稳定性与残差。对 AI 而言，这套流程恰好可以拆成机器学习模拟、区间算术、形式化证明与大模型提拟设的组合，最终构造可能复杂到人类无法独立验证。

真正的风险在于过程不透明：一个自主运行的 AI Harness 若在内部完成全部试错并直接给出证明，那么数学界得到的是“问题已解决”的结论，而不是迭代过程中长出的新思想——历史上证明或否证全局正则性的尝试，正是 Leray-Hopf 弱解、Prodi-Serrin 部分正则性等一批基础理论诞生的土壤。

陶哲轩警告，如果 AI 过早地以黑盒方式解决开放问题，问题原本能孕育的数学进展可能遭到“污染”，严重时 AI 对数学发展的整体影响甚至可能从正面变成净负面。他并非反对 AI for Math，而是提醒：解题的人或系统如果提前知道最终拟设，很容易抑制对其他路线的探索。

一道难题的重要，不只在于等待揭晓的答案，更在于通向答案的路上被发掘出的新思新想。