OpenAI 三项 AI 证明，物理那项交五位学者先看

OpenAI 把三项 AI 证明拆成了三种放法，牵涉千禧年大奖难题的物理结果，眼下只有它点名的五位学者拿得到材料。

10 月 26 日，OpenAI 公布内部模型在数学、计算机科学和物理上的三项结果。数学和计算机两项的自然语言证明与 Lean 形式化证明已经放上 GitHub；物理那项由 David Gross 带队的小组决定先不公开。

就在前一天，设在高等研究院的数学与人工智能顾问组 AGMAI 发文，建议 AI 公司不要再指定少数学者先看材料。

对照两份文件，OpenAI 在形式化证明和资助上照着建议做了，在谁先看上没有。三项结果因此处在不同的可检验程度，物理那项目前只能当公告读。

三项结果分三种方式放出

据 OpenAI 公告，三项结果的放法由它请来的外部专家各自建议。下表对照三项各公开了什么、由谁先检验：

领域	公开了什么	由谁先检验
数学：局部光滑猜想，由此推出挂谷猜想	模型原文与 Lean 证明	不设小组，学界自行组织
计算机：否证指数时间假设	原文与 Lean 证明	Impagliazzo、Paturi、Williams 三人小组
物理：QCD 等理论的存在性证明	暂不公开	Gross 等五人小组，由他们自己执笔

从上往下看，越往下，材料越集中在少数人手里。

几处时间点也写在公告里：指数时间假设的否证 10 月 16 日得到，次日完成 Lean 形式化。杨—米尔斯存在性的自然语言证明 9 月 9 日就有了，形式化 10 月 16 日完成。

据 The Verge 报道，计算机小组里的 Impagliazzo 和 Paturi 正是 1999 年提出这个假设的人，如今由他们检验推翻它的证明。

顾问组前一天列出的五条理由

AGMAI 10 月 25 日的文件写得很直接：建议 AI 公司今后不要采用指定数学家先拿材料的做法。理由有五条：

• 先看的人抢到起跑时间，其他人拿不到材料；
• 由公司替学界决定谁来理解和检验，剥夺了学界的选择；
• 挑人反映的是公司的人脉和优先级，外人无从问责；
• 被点名学者的名字会替公司背书，挡掉批评；
• 没有必要，近来公开的 AI 输出已有学者自发读懂并写成论文。

文件给出的替代做法也很具体。材料放到不受实验室控制、有可引用编号的学术仓库；写明模型名称、提示词、尝试次数、算力和成本，并说明题目怎么挑、一共试了多少题。

此外，能形式化就形式化；资助由独立的非营利机构分配，不由实验室决定。

对照下来做到了两条

逐条对照，OpenAI 这次做到的有两条。数学和计算机两项写明已完成 Lean 形式化，物理那项写明杨—米尔斯存在性部分已完成；资助方面，公告提到已向 Simons 基金会捐 500 万美元，由基金会管理和发放，另承诺为计算机小组资助一场会议。

没做到的更多。材料放在 OpenAI 自己的 GitHub 仓库；公告页没有写模型名称、尝试次数和算力成本，也没有说明题目怎么选出来的；计算机和物理两项都指定了小组。

物理那项的延迟理由已经不成立了。这是 AGMAI 10 月 26 日第二份声明的论点：OpenAI 自己说等形式化完成才发布，而按它的说法形式化已经完成。顾问组因此要求立即公开杨—米尔斯相关的原文和 Lean 输出。

有人会说，物理不归数学顾问组管。AGMAI 自己也承认，它的建议针对数学，不一定适用于其他学科。

OpenAI 公告则强调小组成员无偿参与、不签保密协议，并承认先挑人会造成信息不对称。我们接受物理界可以有自己的规矩，但杨—米尔斯存在性同时是千禧年大奖难题的一部分，数学界要求同时拿到材料，理由站得住。

独立核查还没开始

能检验和已检验是两回事。独立核查网站 State of Proof 10 月 26 日的首页写明：指数时间假设的稿件它还没有独立核查，物理材料尚未公开、它没有审过。它还提醒，有 Lean 链接不等于有人核对过其中的公理、依赖，以及形式化陈述与原文是否一致。

核查能查出什么，可以看一个先例。OSVerify 审读了 OpenAI 此前一篇四维挂谷集的预印本，结论是 0 个重大问题、2 个小问题：一处引错了引理编号，一处把雅可比行列式的方向写反了，两处都不影响文中实际用到的式子。这类细账，要等材料公开后才有人能算。

所以三项结果眼下要分开读。数学和计算机两项已经进入任何人都能查的阶段；物理那项还停在公告阶段，这是分析推断，依据是材料至今只在五人小组手里。等物理材料连同 Lean 证明公开，或计算机小组发出第一份检验结论，我们会相应改写这个判断。