AREX Feed Article
评审组认定 OpenAI 的 Yang–Mills 构造成立，质量间隙与极限唯一性未证
2026 年 11 月 10 日，审阅 OpenAI 物理结果的 Yang–Mills shepherding 评审组通过 GitHub 仓库 发布《》，对 OpenAI 于 10 月 28 日提交、以可机检证明语言 Lean 写成的形式化证明给出委员会意见：该提交证明了满足 Wightman（维格曼）公理的相对论性量子场论，可以作为任意单紧致规范群（simple compact gauge group）的四维 Wilson 格点规范理论的标度极限（scaling limit）构造出来。紧随其后的是另一句判断：它没有证明无穷体积极限唯一，也没有证明存在质量间隙（mass gap）。
评估以 PDF 形式存放在仓库 docs/assessment-1.pdf，仓库页面于 11 月 11 日更新，代码与文档按 Apache-2.0 许可发布。仓库的结果表里，OpenAI 11 月 4 日提交的第二份材料标注为“work in progress”（进行中）。
认定结论：证明的是 Wightman 构造，不是完整的千禧年难题
评估分两部分。第一部分把提交的定理陈述与 Jaffe 和 Witten 为 Clay 数学研究所千禧年难题撰写的表述对照，第二部分直接检查 Lean 代码。评审组的原话是：“OpenAI 的构造并未认证完整的 Jaffe–Witten 问题：没有主张质量间隙。”跨体积子列的唯一性、各分量理论之间是否一致，同样未决。评估第 2 节逐条清点构造提供了什么，其中第四条只有一句：“该构造没有为理论中质量间隙的存在与否提供任何证据。”
这与提交方的自述一致。 说明写明：“正质量间隙、对连续质量广义自由场的一般排除与全阶 MS-bar 匹配都在其范围之外。”
按 10 月 27 日的报道，Yang–Mills 问题分两半：证明理论在数学上自洽（“存在”），以及证明它有非零的质量间隙——后者“在物理世界有重要后果”。说明，纯 Yang–Mills 存在性是其四维量子场论存在性结果的子问题，属于 Clay 千禧年难题的范畴。
对未证唯一性，评审组在评估里表明了态度：“我们相信，未能证明大体积极限与真空的唯一性，与‘无穷体积极限及真正的 Yang–Mills 真空唯一’这一普遍预期并不矛盾。”
做出这份判断的小组来自 OpenAI 10 月 26 日公布的 shepherding（“牧羊人”式托管评审）安排：外部专家组织协作组来理解新结果，物理结果采取“小组决定材料发布”的策略。博文写明小组由 David Gross 牵头，成员包括 Michael Douglas、Arthur Jaffe、Igor Klebanov 和 Nikita Nekrasov，协作遵循四项原则——透明、不索取学术信用、承认小组贡献、独立且无偿；小组联络邮箱 与评审组仓库公布的投稿邮箱一致。OpenAI 的模型在 9 月 9 日产出 Yang–Mills 存在性的自然语言证明，10 月 16 日完成 Lean 形式化，10 月 28 日向小组提交源码包。评估致谢栏写明，评估文档由 Michael R. Douglas、Arthur Jaffe、Ron Nissim 和 Fred Rajasekaran 撰写，经全组批准。
这项安排在 10 月底曾有争议。Scientific American 报道，数学家 Levent Alpöge（Anthropic）与 Ethan Sussman（西北大学）的独立证明进度在 OpenAI 公告前数周已经公开，OpenAI 把证明交给专家小组而非直接发布的决定“引发了即时抗议”，抗议者中包括 OpenAI 自己早前为应对批评而组建的数学顾问小组成员。同篇报道里，后来执笔这份评估的 Douglas 称这项结果“是一项重大进展。数学家们 50 多年来一直试图让量子场论严格化，并取得了稳步进展，但像量子色动力学这样的真实世界理论看上去总是遥不可及——直到现在。”
构造链条：固定体积取紫外极限，体积无穷只取子列，再分相位重建
构造链从 Wilson 格点规范理论出发。用评估的话说，输入是具有非阿贝尔单实李代数的闭矩阵子群 G ⊂ U(m)：在边长 L_p、格距 a_N 的离散环面上放置 Wilson 作用量的概率测度，局域观测量定义为曲率 F 及其协变导数的规范不变多项式“标签”，并为其配备重整化后的格点代表。
第一步是固定体积的紫外极限（评估定理 4.1）：构造给出格距、物理边长与耦合的序列，使关联函数在格距趋于零时收敛，耦合按渐近自由要求的系数随 log(1/a) 标定。序列由构造自行选择，评估强调紫外收敛定理“不主张对所有可能的格距序列收敛”。
第二步是无穷体积极限（定理 5.1）：物理边长趋于无穷时，只证明存在子列使所有关联函数同时收敛。证明工具是紧性论证（Arzelà–Ascoli），输入的先验估计来自反射正性、棋盘估计、转移算子表示与 Cauchy 估计。评估直言，Jaffe–Witten 的千禧年难题表述“认为仅由紧性得到的子列极限是不够的”，除非另有论证补上极限所需的性质。
第三步把混合理论分解为分量。子列极限的关联函数可以写成 S^mix(v; f) = ∫ S^ξ(v; f) dν(ξ)，即各分量理论（纯相位）按概率测度组合，证明用到交换 C*-代数的 Gelfand 表示定理与 Riesz–Markov 表示定理；每个分量满足包括聚类（clustering）在内的 OS（Osterwalder–Schrader）公理变体。第四步是重建：提交证明了自己的 OS 重建定理，把每个分量解析延拓到实时间，得到带真空与场的 Wightman 理论。定理 6.1 逐条列出重建所得的性质：平移谱与正能量、真空唯一性、共同定义域与循环性、Poincaré 协变、局域对易、解析延拓复原关联函数。
Yang–Mills 身份的证据链：痕迹反常、渐近自由与算符乘积展开
“这是 Yang–Mills”的判断靠证据链支撑，评估第 7 节逐项给出。其一，构造定义了守恒应力张量，平移 Ward 恒等式以固定符号与系数对每个局域场、每个相位成立。其二，痕迹反常：对光滑联络，应力张量的迹本来为零，重整化后非零。定理 7.1 给出所选相位中中心化迹 Θ 两点函数的领先短距离行为——r⁸ log²(1/r) 乘以该两点函数趋于 3·dim_ℝ(g)/π⁴（dim_ℝ g 为李代数的实维数），评估写明系数与微扰论预言一致，这一非零极限同时证明构造非平凡。其三，自由场排除：有限个质量的自由场之 Wick 多项式组合无法在小区间上再现这种逆平方对数行为，但评估注明这并未排除高斯场复合的一切描述。其四，渐近自由（定理 7.2）：有效耦合 g_W(r) 满足 log(1/r)·g_W(r)² → 1/(2b₀)，其中 b₀ = 11C_g/(48π²)（C_g 为 Casimir 常数）；由连续关联函数定义的第二个耦合同样在 r → 0 时趋于 g_W；至于 g_W 是否独立于所取的子列极限，提交未证明。其五，算符乘积展开（OPE，operator product expansion）：系数统一、对每个相位一致、带显式余项界，但系数对子列极限的独立性未证，“全阶微扰匹配仍未证明”。
评估的总结措辞是：格点起源、局域场、归一化应力张量、领先短距离定律与 OPE，“为该构造描述的是 Yang–Mills 理论提供了实质性证据”。识别靠的是这条证据链；唯一性并不在已证结论之列。
核验记录：184 分钟干净重建、三次 Comparator 通过与 A1–A8 独立桥接
评审组区分了三层工作：形式验证（Lean 内核检查证明是否符合陈述与允许公理）、validation（陈述是否表达了预期的物理与数学），以及对检查本身是否被规避的复核。
机械记录 M1：10 月 29 日在 Apple Silicon、Lean 4.32.0、钉死的 Mathlib（Lean 官方数学库）缓存下从零重建 9,470 个项目模块，约 184 分钟，零错误；9,477 个源文件与提交清单一致。声明清单覆盖被构造导入的全部 250,319 个项目声明：没有项目自定义公理，没有占位公理 sorryAx，被审主结果依赖中没有 unsafe 声明。内核重放覆盖 17 条主结果依赖的 100,168 个声明，另审计边界处 14,364 个外部声明；用到的公理只有 propext、Classical.choice、Quot.sound 三个标准项。构建产生 2,453 条警告，评估认为多数属于证明脚本清理与弃用语法。
机械记录 M2：Comparator（提交方案与冻结参考陈述的比对工具）三次通过——10 月 30 日对公开定理 YangMills.jointExistence，11 月 3 日对评审组自定的合并目标 YMReview.Acceptance.combined_acceptance，11 月 5 日对 OPE 陈述对齐定理 YMReview.OPE.constructed。11 月 3 日与 11 月 5 日的记录各含四个对照实验：有效证明被接受，改动陈述、添加被禁公理、改动定义各被拒绝。评估还记录了一处提交方的更正：OpenAI 提交后告知评审组，原公开目标遗漏了证明所建立的与格点构造的部分联系；评审组因此让合并目标保留构造证书，把格点观测量、极限、相位与重建场绑在同一目标下检查。
A1–A8 是评审组自己写下的独立桥接。标量 OS 公理检查把所选相位中应力张量中心化迹的 Schwinger 函数（欧几里得关联函数），对照仓库 xiyin137/OSreconstruction 给出的 OS 公理与 E0′ 增长条件——评估强调这套目标公理“在评审组得知 OpenAI 构造之前已独立表述”；格点 Wilson 测度对照 mrdouglasny/lgt 的独立定义，在约定换算后逐项相等；其余为场内容、共同标度、Ward 恒等式、领先痕迹律、合并接受与 OPE 的检查，每项有规格、证明与带日期的验证记录。按日期排列：10 月 29 日干净构建，10 月 30 日、11 月 3 日、11 月 5 日三次 Comparator 通过；11 月 5 日的打包重放新编译全部 43 个审查模块、零警告，13 项端点审计与 96 份公理报告全部只含三个标准公理。
把边界写得很直白：形式检查成功“仍需人工审查来确认定义与陈述表达了预期的物理与数学”。评估自述做了“广泛（但不穷尽）”的人工定义审查。复现方式在：克隆后在包目录运行 python3 scripts/verify.py integrity 与 python3 scripts/verify.py all，运行器会构建提交与审查、构建钉住版本的工具、跑对照实验并检查三个 Comparator 端点，把新的带日期记录写入 runs/。仓库同时注明：历史记录使用 macOS 上的上游开发启动器 fake-landrun.sh，不提供 Linux/Landrun 的进程隔离，“不测试对潜在恶意构建代码的隔离”，外部独立内核实现也未使用。
评审组写下的边界：未读完的证明、五道开放题和一份“进行中”的新提交
评估没有回避自己看到的毛边。代码质量一节写道：250,319 个项目声明里只有 100,168 个进入主定理依赖树，差额显著；提交还使用了非常规命名，比如 TicketsChart.lean 里的 Farewell.dead、Kitchen.lean 里的 Cake 和 cookie、Parade.lean 里的 anxiety。工具方面，评审组用 OpenAI 的 Astra 辅助消化 Lean 代码，并明言“我们尚不主张已完全理解这个证明”；文档反馈使用了 Anthropic 的 Fable。评估同时声明：除接受提交与使用 Astra 外，小组与 OpenAI 没有其他关联，与 Clay 数学研究所现在也没有关联。
评估第 8 节列出五道未答之题：一，建立收敛（而非找到收敛子列）并证明无穷体积极限唯一；二，在合适空间上为连续理论定义概率测度，导出 OpenAI 构造的 Schwinger 函数；三，建立一致质量间隙，给出相应关联函数的指数衰减与 OS 哈密顿量的谱隙；四，构造 Wilson 圈观测量、与局域观测量建立联系，并证明面积律；五，构造单粒子态并分析其能动量谱——评审组注明，这类分析在 2、3 维时空的可构造模型中已有先例。
仓库结果表的最后一行是正在进行的后续：OpenAI 11 月 4 日的第二份提交，评估栏为空。检查范围说明注明，11 月提交及其新增的微扰匹配主张都在十月评估的范围之外；评审组对它尚无意见可发表。