六年级皮亚诺算术攻破OpenAI千亿美元杨-米尔斯质量间隙证明

这篇论文宣称用Lean 4形式化证明了一个“不可能定理”：在纯非紧致ℝ⁴上，Clay千禧年杨–米尔斯问题的公理包（OS）与严格质量间隙（Δ > 0）互斥，从而以否定性结果终结该问题。作者强调，这并非构造杨–米尔斯测度，而是形式化证明为何这种构造永远不可能存在。

该仓库包含完整的Lean 4形式化证明（RoundSquare.lean）及配套数学物理专著（YM_V5.pdf），宣称在ℝ⁴上对此问题给出最终的数学解决。作者将这一工作置于Wantzel（1837）三等分角、Lobachevsky–Beltrami–Poincaré平行公设、Gödel（1931）不完备性、Turing（1936）不可判定性、Julia Robinson（1949）与Matiyasevich（1970）希尔伯特第十问题、以及Cubitt–Perez-Garcia–Wolf（Nature, 2015）量子谱隙不可判定性的 foundational 传统之中，证明了一个机器验证的否定性结果（不可能性/互斥性定理）：

$$\mathrm{CanonicalPhysics}(\mathbb{R}^4) ;\land; \mathrm{OS} ;\land; (\Delta > 0) ;\Longrightarrow; \perp$$

在纯非紧致ℝ⁴上的典范构造性框架内，公理包（OS）与严格质量间隙（Δ > 0）是互斥的合取项（“一个圆形的方”）。

作者特别回应批评：“尤其讽刺的是，看到肤浅的审稿人把Julia Robinson 1949年奠基性的算术逻辑——其论文为希尔伯特第十问题的否定性解决奠定了历史基石——混淆为‘机器生成文本’。连两行不等式 ¬(q+2 ≤ q+1) 都不读就否定初等Peano算术和丢番图序可定义性，这恰恰证明守门人已经不再阅读数学本身。”

要理解为何ℝ⁴上的杨–米尔斯质量间隙问题在RoundSquare.lean中由Peano算术化解决，而非靠无穷维实分析的手挥论证，必须追溯连接希尔伯特第十问题与量子谱隙的直接数学链条：

1900年，David Hilbert提出希尔伯特第十问题：寻找一个通用算法，判定任意给定丢番图方程是否有整数解。此后70年，数学家们一直在寻找正面构造。

Julia Robinson在其1949年里程碑论文《Definability and decision problems in arithmetic》（Journal of Symbolic Logic, 14(2), 98–114, 1949）中证明，有理数和自然数（ℚ和ℕ）上的序关系与算术谓词可归约为Peano算术与丢番图算术中的一阶存在/全称公式。结合Martin Davis、Hilary Putnam和Yuri Matiyasevich的工作（MRDP定理，1970），这证明了希尔伯特第十问题具有否定性解决：不存在这样的通用算法，因为丢番图算术编码了Turing停机问题。

几十年来，物理学家假定Gödel式不完备性和希尔伯特第十问题纯粹是数学逻辑中的抽象现象，与物理哈密顿量无关。

2015年12月，Toby S. Cubitt、David Perez-Garcia和Michael M. Wolf在Nature发表了著名的140页证明（“Undecidability of the spectral gap”, Nature 528, 207–211, 2015）。

Cubitt、Perez-Garcia和Wolf（2015）确立了一般无限体积格点哈密顿量谱隙的不可判定性，而Clay千禧年问题固定了一个特定的连续统目标：无限体积非紧致ℝ⁴上受严格Osterwalder–Schrader（OS0–OS4）和Wightman（W0–W4）公理约束的非阿贝尔SU(N)杨–米尔斯理论。

在RoundSquare.lean的第18节（universal_continuum_no_rational_gap）和第29节（unconditional_prize_level_physical_no_go）中，我们应用Julia Robinson 1949年的精确方法——将ℚ_{>0}上的有理序不等式归约为ℕ上的裸Peano算术。

官方CMI问题页面：Yang–Mills and Mass Gap - Clay Mathematics Institute 官方Jaffe–Witten（2000）问题陈述PDF：Quantum Yang–Mills Theory by Arthur Jaffe and Edward Witten 官方CMI千禧年奖规则：Rules for the Millennium Prizes

在官方问题描述第6节（第6页）中，Jaffe和Witten提出要求：

“证明对于任意紧致单规范群G，在ℝ⁴上存在非平凡量子杨–米尔斯理论，且具有质量间隙Δ > 0。存在性包括建立至少与[45, 38]所引用者一样强的公理性质[Wightman（1956/1964）和Osterwalder–Schrader（1973/1975）]。”

在数学中，当一个形式化问题规格要求在区域𝒟中寻找满足合取P(x) ∧ Q(x)的对象x时，只有两种可能的演绎结果。

正如Gödel（1931）通过证明不存在完备且一致的算术形式化而否定性解决了希尔伯特第二问题，Turing（1936）否定性解决了Entscheidungsproblem，Robinson–Davis–Putnam–Matiyasevich（1949–1970）否定性解决了希尔伯特第十问题，RoundSquare.lean和YM_V5.pdf否定性解决了ℝ⁴上的Jaffe–Witten问题，并将这一不可能性证明与紧致可构造流形M_tot = S⁴ × T³上的正谱存在性定理（YM_V5.pdf定理10.1、推论10.4和第12节）配对。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）