用张量网络与 Lean 4 验证 OpenAI 的 Haldane 能隙机器证明

研究者对 OpenAI 生成的周期自旋-1 Heisenberg 链均匀能隙的计算机辅助证明进行了验证、消化与形式化，工具是张量网络图和 Lean 4。沿空间和虚时间方向读取配分函数网络后，他们展示了有限环界如何在加倍长度和逆温度间传播到更长偶数环，在相同有限输入下把自旋-1 界 sharpening 19 倍，得到对所有偶数 L≥36 都有 Δ_L > 0.0729。 论文还识别出反射正定性是这一证明背后的普适条件，并据此在另外七条自旋链和梯子体系中认证了均匀能隙。这表明把机器生成的证明消化成透明的物理机制，能产出更尖锐的界、更广的定理以及可复用的形式化验证。