物理学家更正：OpenAI Lean 代码确实证明了 Yang–Mills 非自由理论
danintheory · x · 2026-11-14
物理学家 Scott Armstrong 公开更正自己此前对 OpenAI Lean 形式化证明的评价：他此前回复称该构造「未证明非高斯」，这一表述有误导性。
要点：
- OpenAI 的 Lean 代码确实证明了该理论不是自由 Yang–Mills：自由理论中应力张量的迹恒为零，而 Lean 构造中非零，且符合渐近自由与 UV RG 计算的预言。
- 证明还给出了更强的结论：该理论无法用任意有限个普通自由场的 Wick 多项式描述。
- Armstrong 确认该理论是相互作用的（interacting）；未被证明的是更强、更技术性的命题——理论不能由更多自由场构造出来。
这一更正强化了 OpenAI Lean 项目在 Yang–Mills 质量间隙形式化上的实质贡献。
「研究」频道最新
- PiHand：手物交互先验让灵巧手 RL 训练样本需求降 10 倍 — KyleMorgenstein · 2026-11-14
- 新论文：对称性是层级涌现与抽象的共同起源 — mjdramstead · 2026-11-14
- MoE combine 通信量从 16 位压到 8.25 位：RHT+S2F6 量化技巧引热议 — snowclipsed · 2026-11-14
- 科学家在计算机中 4D 模拟完整活细胞，登 Cell 期刊 — tomchapin · 2026-11-14
- 质疑 Anthropic 算法大跃进：同算力下 bpb 大幅提升不可信 — teortaxesTex · 2026-11-14
- 蚂蚁 Mara Chain：失败编辑留证据，AppWorld 少 6 千次_rollout 追平 GEPA — jiqizhixin · 2026-11-14