AI交出证明之后，科学还需要什么

一份机器生成的长篇证明，距离进入教科书有多远？OpenAI在2026年10月26日公布的学术协作安排，把这个问题推到了台前。它涉及调和分析、计算复杂性和量子场论三类研究，并尝试用不同的公开方式，让领域专家接手检查、解释与组织讨论。

这条新闻值得关注的重点，是AI研究产出正在进入怎样的验证流程。读者需要把公司宣称得到的结果、形式化证明检查、专家理解，以及学术共同体逐步形成的判断分开看。把几层证据压缩成一句“AI解决了科学难题”，会丢掉最重要的信息。

三类研究采用不同的开放路径

按照OpenAI公告，数学研究直接公开模型输出；计算机科学研究同时公开材料并组织外部协作；物理研究则由外部小组先推进解释工作，材料的发布节奏交由该小组决定。计算机科学部分围绕指数时间假设（ETH），由Russell Impagliazzo、Ramamohan Paturi和Ryan Williams牵头；物理部分由David Gross带领小组研究。OpenAI把这些模型产物定位为有待转化为科学理解的原始研究材料。

这种安排提示了一个值得认真讨论的变化：当产出速度超过解释速度时，研究组织的关键工作可能转向“谁来检查、怎样拆解、如何让更多人参与”。公开一个文件解决了访问问题，却没有自动解决阅读成本、背景知识和复现环境的问题。

从编辑判断看，三条路径各有取舍。直接开放允许更多人及早检查，但分散讨论可能重复劳动；组织工作组能集中专业力量，却要防止讨论只发生在最先获得材料的小圈子；先整理再公开可能提高可读性，同时也会延迟外部检验。不能仅凭开放时间早晚，就断言其中一种方式适合所有领域。

Lean检查解决的是哪一层问题

Lean是一套形式化证明工具。它要求把命题、定义和推理步骤表达在明确的逻辑系统中，再对证明对象进行检查。它的价值在于降低漫长推导中隐藏逻辑跳步的风险；Lean官方教材同时区分了寻找证明与验证证明这两类工作。

但理解一项研究还要问：形式化命题与人们讨论的原问题是否准确对应？证明依赖哪些假设？自然语言论文里更强的表述，是否也覆盖在已形式化的范围内？研究者能否解释关键构造为何有效、哪些方法值得复用？这些问题需要数学和计算机科学的专业判断。

这次公开的ETH形式化范围说明尤其值得读。说明区分了Lean覆盖的时间界与10月25日手稿中更强的时间界。对于普通读者，这个细节足以提醒我们：一句“有Lean证明”不能代替对具体证明范围的核对。范围文档与正式论文应当一起读，而不是只看新闻标题。

这张表是阅读框架，不是对本次成果完成度的评级。公告和公开文件的存在，并不能证明每一项工作都已经走完所有阶段。

为什么不能把ETH写成P与NP已解决

ETH讨论的是一类可满足性问题所需时间的更细尺度。公开的形式化范围涉及固定参数下的次指数时间算法。次指数时间与多项式时间之间仍有重要区别：比某个指数增长得慢，不等于存在多项式时间解法。

因此，即使相关ETH结论最终得到学界接受，也不能直接改写为“P等于NP”，更不能推导出所有困难计算任务都已经变得容易。与之相关的条件性复杂度结论需要重新检查各自依赖；某些理论下界的前提受到影响，也不等于现有软件马上出现可用的高速替代方案。这里应以公开形式化范围为边界，而不是扩大到没有被该命题证明的问题。

物理研究同样要避免跨越结论边界。关于某些量子场论数学存在性的研究，不能仅凭标题延伸成“标准模型已被最终证明”或“实验验证完成”。数学对象的严格构造、理论对现实的适用程度、实验观测之间，是需要分别论证的关系。

研究者和普通读者可以怎样跟进

一个实用办法，是为每项结果建立四栏记录：原始命题、公开材料、独立评论、尚待回答的问题。先看形式化范围，再读自然语言说明；记录材料的版本变化，不把后续修订与最初声明混在一起。遇到论文和代码给出不同强度的结论，应准确标出各自覆盖范围。

对参与复核的团队，值得优先做的工作是整理术语、缩小到关键引理、记录可复现环境和提出能被具体回答的问题。对传播者，最重要的是保留主语：机构“宣布”或“声称”的结果，与独立团队“复核完成”的结果，报道措辞应有所区别。专家参加工作组也不等于其已经为全部结论背书。

这次事件的长期价值，可能不仅取决于最终有哪些命题站得住，还取决于它能否形成一套可持续的协作方法：机器输出能被外部检查，检查劳动得到认可，争议有公开入口，读者知道每一层证据到哪里为止。AI可以加快提出研究结果；让结果成为可理解、可传递、可继续使用的知识，仍需要严密而开放的学术工作。