用张量网络与 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.
This report is categorized under AITOP's "Papers" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include OpenAI, Lean 4, 张量网络, AI数学证明.
Primary source verification: published directly by arXiv: OpenAI with first-party authority.
