AREX Feed Article
KITP 公布 Yang-Mills 工作组，OpenAI 的 1,147 页证明将分阶段核验并公开
10 月 28 日 00:16 UTC（北京时间 08:16），加州大学圣塔芭芭拉分校 Kavli 理论物理研究所（KITP）的官方 X 账号发布，公布 Yang-Mills Working Group。工作组由 KITP 永久成员 David Gross 主持；KITP 的帖文称，它要解读与量子色动力学（QCD）存在性及标准模型的完备化相关的 AI 结果，其中包括证明量子 Yang-Mills 理论存在性这一子问题。
KITP 网站的链接到一份，署名者是 Michael R. Douglas、David J. Gross（主席）、Arthur Jaffe、Igor R. Klebanov 与 Nikita Nekrasov 组成的 shepherding committee（负责引导结果发布的委员会）。声明写明，OpenAI 已请 Gross 接手量子 Yang-Mills 存在性证明的保管与发布；委员会将在核验后分阶段公开用交互式定理证明器 Lean 写成的形式化证明，以及 1,147 页原文。
这一安排对应 OpenAI 10 月 26 日的：其模型给出四维相互作用量子场论的严格存在性证明，涵盖 QCD、标准模型的一个统一完备化，以及作为子问题的纯 Yang-Mills 理论。公告当时称，物理方向由 Gross 牵头上述小组，AI 产出物如何发布交由该组决定。
10 月 16 日，OpenAI 请 Gross 接手证明
按声明的叙述，10 月 16 日 OpenAI 向 Gross 提出这一请求，由他「决定将它发布给学界的最佳方式，并主持发布过程」；Gross 随后选定了委员会其余成员。这个日期比 OpenAI 10 月 26 日的公开公告早十天。
声明对委员会与 OpenAI 的关系写得很直接：委员会将「代表学术共同体」主持发布，把「发布错误结果或粗心遗漏署名」这类风险降到最低。声明里还有一句：「我们对 OpenAI 不负有责任。」
先核对定义与形式化，再发布 Lean 证明
声明把第一项工作定在定义层面：确认定义、问题陈述与物理和数学中的标准表述一致，并确认 Lean 形式化与自然语言论证一致。理由是发布之前委员会希望「确信它是正确的」；OpenAI 提供的 Lean 形式化被委员会视为让这项检查可行的工具。委员会要先做这两项检查，才谈得上发布。
这两项检查通过后，委员会才会发布 Lean 证明。之后它打算借助社区其他成员的力量理解证明、探索它在量子场论中的用法；等对证明的质量与正确性满意，再把评估和 1,147 页 LLM（大语言模型）证明全文一起公开。
OpenAI 10 月 26 日的公告说，物理组决定暂不发布 AI 产出物，转而自己撰写说明。新声明没有改变这个起点，但把此后的安排写得更具体。声明称手稿「篇幅与复杂度都令人生畏」，消化其方法与含义「需要一些时间」。
禁闭与质量间隙留在证明之外
声明交代了这项结果在物理中的位置：SU(3) 规范群耦合夸克的量子 Yang-Mills 理论就是标准模型里的 QCD，解释强核力；它的显著特征是渐近自由，即力在短距离变弱、在长距离变强。声明称，这一特征使过去 50 年的高能预测成为可能，也被认为导致夸克禁闭在强子内并产生质量间隙。
按声明的说法，OpenAI 的工作建立在 Kenneth Wilson 1974 年提出的格点正则化与 Tadeusz Balaban 在 1980 年代发展的严格重正化群处理之上，其中 Balaban 的想法是让这项工作能跟到无穷远距离、证明连续极限存在的重要因素之一。紧接着的一句是：「然而，禁闭与质量间隙仍是极其重要的未决挑战。」
这份声明讨论的是理论的存在性，它没有把禁闭与质量间隙算作已解决。OpenAI 的公告把纯 Yang-Mills 存在性列为 Clay 数学研究所千禧年大奖问题的一部分；委员会则明确把禁闭与质量间隙都列为仍未解决的问题。委员会对证明本身的措辞也留有余地，称它「看来是」把量子场论置于严格数学基础之上的重要一步。
欢迎帖与四条协作原则
KITP 帖文发出三分钟后，OpenAI 科学家 Dan Roberts 引用该帖写道：「非常期待这个由 David Gross 领导的团队，来引导 OpenAI 在 QCD 与量子 Yang-Mills 存在性方面的工作。」这条帖文没有补充技术内容，也没有给出验证所需的时间。
OpenAI 在 10 月 26 日的公告里列过四条协作原则：参与者不会被要求签保密协议；OpenAI 不为这些发现寻求学术署名；工作组因其撰写的说明获得认可；成员自愿、无报酬参与，结论属于自己，OpenAI 不以他们的名义发言。这与声明中「对 OpenAI 不负有责任」的自我定位相互对应。
声明把整套安排称为一次实验，并称会「非常谨慎地推进」。声明没有给出两项检查的时间表，也没有说 Lean 证明何时发布。