Formalized Mathematics as a Debugging Tool: falsifying an invariant and deleting a phantom difficulty in lattice gauge theory
Juan Carlos Paredes · Zenodo (CERN European Organization for Nuclear Research) · 2026
We present a machine-checked formalization in Lean 4 of a problem in lattice gauge theory: the Plateau Conjecture, which asserts that a charged magnetic flux family on a discrete torus is separated from all flat gauge fields by an operator-norm gap uniform in the system size. During formalization of a natural 1D invariant — the column-winding sum — the proof assistant exposed a fatal flaw: the shear family, a gauge configuration with trivial horizontal edges, carries the same winding as the charged flux family yet lies arbitrarily close to a flat family in the large-system limit. This falsification forced a correction: the invariant must read the full 2D plaquette data. We construct the corrected invariant (total flux), prove it passes the falsification test, and then formalize the reduction of the conjecture itself: a machine-checked theorem derives the full m-uniform statement from a single transported rigidity estimate for the magnetic-translation pair, exposing along the way that a distance-translation step previous drafts treated as half the open problem is not load-bearing at all. The library's only remaining sorry is that one estimate, stated over concrete objects with its classical unitary specialization known. The methodological contribution is the use of formal methods not as an after-the-fact certification but as an active research tool that catches subtle errors — twice, in opposite directions: once falsifying a plausible invariant, once deleting a phantom difficulty — in plausible mathematical reasoning.