物理学家工作组验证 OpenAI 杨-米尔斯 Lean 构造：证实 Wightman 公理但未证质量隙

由诺奖得主 David Gross 担任主席的 Yang-Mills 工作组于 11 月 10 日正式发布对 OpenAI 构造的独立验证报告：OpenAI 于 10 月 28 日提交的 Lean 形式化代码（GitHub 仓库 OpenAI-YM-20261028）被认定证明了一个满足 Wightman 公理的量子 Yang-Mills 理论存在性。这是强相互作用力（量子色动力学 QCD）的数学基础，也是百万美元千禧年难题的一部分；但该难题的核心——质量间隙（mass gap）——并未被证明。这一进展若最终成立，将是 AI（LLM 生成证明）在基础数学物理领域的重要里程碑。

已确认

• Yang-Mills 工作组（科学委员会主席为 David Gross，Kavli 理论物理研究所相关协作）已发布第三份声明与正式验证报告，时间在 11 月 10 日前后。
• 验证对象为 OpenAI 10 月 28 日提交的 Lean 形式化构造，仓库为 yang-mills-group/OpenAI-YM-20261028。
• 验证结论：该构造证明了满足 Wightman 公理的量子 Yang-Mills 理论存在性。
• Andrew Curran 等亦转发了报告正式发布的消息，Reddit 用户 (@FateOfMuffins 转述) 也讨论了该仓库。

尚未确认

• 质量间隙（mass gap）部分未被证明，因此距离完整的千禧年难题解决仍有本质差距。
• 帖子均为转发或二手转述，工作组报告的完整细节与最终学界共识尚待更多一手材料确认。

为什么重要

• 量子 Yang-Mills 存在性是标准模型完备化的关键数学基础，此前从未被严格证明。
• 若 LLM 生成的形式化证明经受了独立验证，将标志 AI 在前沿数学研究中从辅助工具走向实质性贡献者，尽管质量间隙这一核心难题仍悬而未决。

2026-11-10 ~ 2026-11-11 · 5 条相关

• David Gross 领衔杨-米尔斯工作组验证 AI 数学成果，涉 QCD 存在性证明 — danintheory · 2026-11-10
• 【源头】诺奖得主领衔委员会验证 OpenAI 量子 Yang-Mills 存在性证明 — 141_1337 · 2026-11-10
• 转发:OpenAI Yang-Mills 构造验证报告由工作组正式发布 — calabi_and_yau · 2026-11-11
• Yang-Mills 工作组独立验证 OpenAI 构造:证实 Wightman 公理但未证质量隙 — calabi_and_yau · 2026-11-11
• Reddit 称 OpenAI 杨-米尔斯存在性「精益证明」已发布并通过验证 — FateOfMuffins · 2026-11-11