Papers With

← All papers
First page of Bridging Gaps with Tensor Networks: From the Haldane Gap and Beyond

Bridging Gaps with Tensor Networks: From the Haldane Gap and Beyond

Sirui Lu

quant-ph Nov 8, 2026 · v1 cond-mat.str-el
formalization verification physics quantum
Read PDF arXiv abstract Code
TL;DR
Formalizes a reflection-positive spectral gap theorem for spin chains in Lean 4, with the Lean kernel checking the mixed-field Ising gap arithmetic unconditionally.
Abstract
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.
Problem

OpenAI produced a computer-assisted proof of a uniform spectral gap in the periodic spin-1 Heisenberg chain (Haldane gap). The proof is hard to understand, generalize, or formalize directly. It was not accompanied by a Lean proof.

Approach

The authors reinterpret the proof with tensor-network diagrams of the partition function along space and imaginary time. This shows how finite-ring bounds propagate to all longer even rings via doubling. They identify reflection positivity as the underlying condition and reduce the spatial inequalities to finite-dimensional matrix algebra. A general reflection-positive gap theorem is then formalized in Lean 4: seed bounds are taken as hypotheses, or reduced to exact integer identities that the Lean kernel checks.

Results

From the same finite inputs, the spin-1 bound is sharpened by a factor of 19 to Δ_L > 0.0729 for all even L ≥ 36. Uniform gaps are certified for seven additional chains and ladders, and the mixed-field Ising gap is proved unconditionally in Lean. An open-chain extension gives Δ_n > 0.01556 for odd n ≥ 1921, also formalized.