用张量网络与 Lean 4 验证 OpenAI 的 Haldane 能隙机器证明
Bridging Gaps with Tensor Networks: From the Haldane Gap and Beyond
LLM 证明出 Haldane 能隙后，这篇工作用张量网络把它拆成看得懂的物理机制，还用 Lean 4 形式化，界直接收紧了 19 倍。做数学形式化或计算物理的人可以看看机器证明怎么被消化成可复用结果。
研究者对 OpenAI 生成的周期自旋-1 Heisenberg 链均匀能隙的计算机辅助证明进行了验证、消化与形式化，工具是张量网络图和 Lean 4。沿空间和虚时间方向读取配分函数网络后，他们展示了有限环界如何在加倍长度和逆温度间传播到更长偶数环，在相同有限输入下把自旋-1 界 sharpening 19 倍，得到对所有偶数 L≥36 都有 Δ_L > 0.0729。
论文还识别出反射正定性是这一证明背后的普适条件，并据此在另外七条自旋链和梯子体系中认证了均匀能隙。这表明把机器生成的证明消化成透明的物理机制，能产出更尖锐的界、更广的定理以及可复用的形式化验证。
Bridging Gaps with Tensor Networks: From the Haldane Gap and Beyond
Proofs generated by large language models are often difficult to understand, generalize, or formalize directly. Here we verify, digest, and formalize OpenAI's computer-assisted proof of a uniform gap in the periodic spin-1 Heisenberg chain using tensor-network diagrams and Lean 4. Reading the partition-function network along space and imaginary time shows how finite-ring bounds propagate across doubled lengths and inverse temperatures to all longer even rings, sharpening the spin-1 bound from the same finite inputs by a factor of 19 to $Δ_L > 0.0729$ for all even $L \geq 36$. We identify reflection positivity as the general condition behind the proof and certify uniform gaps in seven additional spin chains and ladders. More broadly, digesting machine-generated proofs into transparent physical mechanisms yields sharper bounds, broader theorems, and reusable formal verifications.
本条情报归属 AITOP「论文」核心栏目，重点聚焦北美前沿实验室与硅谷科技巨头。在跨区域产业观察坐标中，该动态直接关联「AI 开发者工具链、Coding Agent 与工程化实践」研究主线，反映出当前技术演进与商业落地的最新风向。涉及核心实体与技术议题包括：OpenAI、Lean 4、张量网络、AI数学证明，读者可通过下方标签进入对应专题页查阅历史脉络与关联对比。
信源核验说明：本文原始信息发布自一手权威信源「arXiv: OpenAI」（Tier-1 一手发布），具备高确定性参考价值。
