AI不只是在答题了：OpenAI一口气交出三张科学“成绩单”
10月27日，OpenAI公布了一组足以让不少数学家和计算机科学家停下来看几遍的结果。
这回不是模型在测试题上拿了高分。
它一次给出三份证明：所有维度下的局部光滑猜想、推翻指数时间假设，以及量子色动力学与纯杨–米尔斯理论的严格数学存在性证明。
前两项已经通过 Lean 数学验证工具进行形式化验证，自然语言证明和 Lean 代码也公开在 GitHub 仓库。物理成果仍在专家审查，结论待核实。
先别急着欢呼，也别急着说这是一场营销。
这三张“成绩单”指向的事情，确实不太一样。
01｜数学这次不是碰巧猜对
局部光滑猜想，研究的是波动的能量集中在空间里能持续多久。OpenAI 的模型给出了适用于所有维度的证明。
这个结果还连着另外两个著名猜想：挂谷猜想和斯坦因限制猜想。
挂谷猜想可以理解成，一根针要在有限空间里转向所有方向，最少需要多大的空间。斯坦因限制猜想，则涉及复杂波动规律里的限制问题。
10月18日，OpenAI 拿到 AI 生成的证明。第二天，Lean 形式化证明也完成了。
这一步很关键。
数学证明最怕一句“显然”。自然语言写得再漂亮，人也可能看漏一个条件。形式化以后，证明里的定义和逻辑步骤要交给机器检查。
这次证明的关键，是一种新构造的辅助偏微分方程。模型不是把已有证明换了一套说法，而是补出了一条此前没有被走通的证明路径。
Lean 在这里充当了**“验钞机”**。验钞机能检查一张钞票是不是真的，却不能替使用者判断这张钱值不值得花。数学结果仍要接受学术界的进一步独立确认，但至少，它不只是一段看起来很像证明的文字。
02｜ETH 被判为假，影响的不只是数学题
指数时间假设，英文缩写是 ETH。
简单说，它认为某些复杂计算问题，计算量会随着问题规模急剧增长，很难找到特别快的算法。
OpenAI 的模型给出了一份推翻 ETH 的证明，并在 Lean 中完成形式化验证。
按公布结果所描述的含义，相关计算任务可能存在比原先设想更快的算法。
这不等于所有难题突然变简单，也不等于电脑性能一夜之间翻倍。它更像是在复杂度理论里拆掉了一块用了很久的基石：原来的判断不再必须被相信，算法设计者可以重新寻找那些原本被认为不存在的快办法。
这也是三项成果里，最容易直接碰到工程和产业的一项。
算力、算法、调度、优化，本来就是计算机行业绕不开的词。如果 AI 不只是在别人写好的框架里调参数，而是能对一条长期被接受的理论假设提出反证，它在科研里的位置就变了。
03｜物理这项最诱人，也最需要沉住气
物理成果更炸。
量子色动力学，也就是 QCD，解释夸克如何结合成质子、中子等粒子；杨–米尔斯理论，则用来描述基本粒子之间的相互作用。
OpenAI 公布的结果包括 QCD 与纯杨–米尔斯理论的严格数学存在性证明，涉及世界七大千禧年数学难题之一。
但这一项目前还在专家审查，参与审查的包括诺贝尔物理学奖得主等专家，相关结论待核实。
这里有个特别容易误读的地方。
“给出严格存在性证明”，不能直接改写成“整个杨–米尔斯难题已经全部解决”。这次涉及的是相关问题的一部分，不是把一个延续多年的难题连根拔起。
该庆祝的部分，是模型试图给出严格数学证明，而不只是用数值模拟展示一条漂亮曲线。
该谨慎的部分，也很明确：物理学成果还没有走到和数学、计算科学成果相同的确认阶段。
把三项成果捆成一句“AI连千禧年难题都解决了”，很容易；认真拆开每项工作的证明、验证和审查状态，才是该有的读法。
04｜真正被改写的，是科研流程
这批结果最值得看的地方，可能不只是“哪三个名字被写进了论文”。
而是证明是怎样被生产出来的。
1.10月18日，AI 生成证明。
2.10月19日，完成 Lean 形式化验证。
3.随后，OpenAI 联系外部专家，讨论围绕成果建立合作机制，并根据专家建议公开证明材料。
整个流程里，AI 不再只是查文献、跑代码、做总结。它开始进入提出猜想、寻找证明路径和生成证明草稿的环节。
人类的任务则往后挪：选择什么问题值得做，检查假设是否合适，审查证明有没有偷换概念，再决定是否接受结果。
这不是“人从此不用做科研了”。
科研的瓶颈会从推导题，转向提出对的问题和验证 AI 的答案。
而当模型可以快速吐出大量看起来新颖的结论，人的审查能力，就成了更稀缺的资源。
05｜以后看到惊世骇俗的 AI 结论，先问三件事
•证明在哪。
•谁验过。
•验到了哪一步。
这三句话会比“它是不是要取代科学家”更实际。
因为真正改变正在发生的地方，不只是 AI 会回答问题，而是它开始主动提交主张。
数学和计算机科学的两项成果，已经有 Lean 验证和公开证明材料。物理成果仍在审查，结论待核实。
边界很清楚。
但方向也已经很清楚了。
以后看 AI 宣布攻克难题，别先问这句话听起来够不够炸。
先看看它交出来的，是答案，还是一份真的证明。