A Lean 4 formalization of the area law for three-dimensional U(1) lattice gauge theory with the Wilson action
In plain words
The proof that charges stay bound in three-dimensional U(1) lattice gauge theory with the Wilson action runs to well over a hundred pages, and several of its steps adapt arguments from older papers. This companion paper writes all of it out, including the adapted steps, in the proof assistant Lean. The formal proof has 215,711 lines, and the main theorem rests on nothing beyond the basic rules of Lean’s logic. Writing it out turned up a list of corrections to the paper, none of which changes a main result.
Abstract
The paper [U1], "Area law for three-dimensional U(1) lattice gauge theory with the Wilson action at every coupling" (<a href="https://doi.org/10.5281/zenodo.23445737">doi:10.5281/zenodo.23445737</a>), proves that the Wilson loop of this theory obeys an area law at every coupling β > 0, uniformly in free finite boxes, with an explicit string tension for large β. We describe a formalization of this theorem in Lean 4 with Mathlib. The Lean statement of the main theorem quantifies over all rectangles in coordinate planes and all finite boxes containing them, with the perimeter constant chosen before the coupling, as in the paper. It has no hypotheses, and its proof uses only the three standard axioms of Lean and Mathlib. The formal proof follows the paper section by section. Where the paper carries a step over from the literature "with changes", that step is written out in full in a separate document, refereed in a separate session and formalized from that document. We also formalize the corollaries for compact gauge groups containing the scalars and for the Georgi–Glashow model at infinite Higgs coupling. The formalization has 215,711 lines of Lean in 862 files, builds from a clean checkout in 22 minutes on a shared many-core server, and certifies every numerical constant that the proof uses. It also yields a list of corrections to the paper, none of which changes a main result.
