OpenAI 邀请诺贝尔奖得主等外部专家审查其 AI 生成的数学与物理证明

OpenAI 针对其 AI 系统在计算机科学、数学和物理领域生成的三项重大证明，引入了由外部专家组成的“牧羊人”小组进行独立审查，并将部分成果翻译为 Lean 代码供计算机验证。其中计算机科学部分涉及指数时间假设（ETH）的证伪，该假设被数百篇论文作为基础；数学部分涉及局部平滑猜想在所有维度的证明；物理部分则涉及杨 - 米尔斯理论在四维空间的存在性证明。OpenAI 明确表示不主张科学发现的所有权，认为荣誉应归于解释结果的专家组，并承诺资助相关会议以推动行业讨论。

审查过程的具体执行存在显著差异：计算机科学组由 Ryan Williams、Russell Impagliazzo 和 Ramamohan Paturi 组成，他们未签署保密协议且无偿工作，计划公开中间结果；物理组由 David Gross 领导，包含 Michael Douglas 等人，目前暂不公开 AI 原始材料，计划由专家组自行撰写成果说明；数学组则无专门小组，直接公开了证明文本和 Lean 代码。尽管 Lean 能验证逻辑步骤是否自洽，但无法确认形式化陈述是否准确捕捉了原始问题意图，因此人类专家的判断仍不可或缺。

这一事件反映了 OpenAI 试图通过制度化审查来应对此前 Navier-Stokes 声明引发的公关危机，并回应关于 AI 突破如何验证、谁有权访问以及谁应获得荣誉的行业质疑。事实层面，OpenAI 已发布数据并承诺资金支持；推断层面，这种“专家牧羊人 + 机器验证”的模式可能成为未来高可信度 AI 科研的标准流程；猜测层面，若 ETH 证伪成立，将动摇复杂性理论的基石，但短期内对实际 SAT 求解器的影响尚不明确，正如 Williams 所言，实用进展可能在 12 个月内出现，也可能毫无动静。