HEXAGONbeta

A Lean 4 formalization of the area law for three-dimensional U(1) lattice gauge theory with the Wilson action

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Sciencemath-ph — Mathematical Physicsmath.LO — Logic

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

In three-dimensional U(1)U(1) lattice gauge theory with the Wilson action, static charges are confined at every coupling: rectangular Wilson loops obey an area law, uniformly in the finite box. This was proved recently by the author in a separate paper; the proof runs to over three hundred pages with its supplement and adapts the Debye-screening analysis of Brydges and Federbush and the multiscale expansion of Göpfert and Mack. We describe a formalization of this proof in Lean 4 with Mathlib, which also covers the paper's corollaries and its appendix on comparing Wilson and Villain loops. The formal theorems take no hypotheses and use only the standard axioms of Lean. The proof became formalizable through explicit interfaces between its parts, written-out versions of the steps that the paper adapts from the literature or leaves out, and certified values for every numerical constant. The formalization also yielded 70 corrections and improvements to the paper, none of which changes its main results.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.23752572

References

  1. T. S. Tomar, Area law for three-dimensional U(1)U(1) lattice gauge theory with the Wilson action at every coupling, Zenodo, https://doi.org/10.5281/zenodo.23445737; HAL hal-05804891.DOI
  2. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction -- CADE 28, LNCS 12699, Springer, 2021, 625--635.
  3. The mathlib Community, The Lean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367--381.
  4. D. C. Brydges, A rigorous approach to Debye screening in dilute classical Coulomb systems, Commun. Math. Phys. 58 (1978) 313--350.
  5. D. C. Brydges and P. Federbush, Debye screening, Commun. Math. Phys. 73 (1980) 197--246.
  6. M. Göpfert and G. Mack, Proof of confinement of static quarks in 3-dimensional U(1)U(1) lattice gauge theory for all values of the coupling constant, Commun. Math. Phys. 82 (1982) 545--606.
  7. P. Hartman and G. S. Watson, ``Normal'' distribution functions on spheres and the modified Bessel functions, Ann. Probability 2 (1974) 593--607.
  8. G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O'Connor, S. Ould Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi and L. Théry, A machine-checked proof of the odd order theorem, in: Interactive Theorem Proving (ITP 2013), LNCS 7998, Springer, 2013, 163--179.
  9. T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison, L. T. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, Q. T. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, T. H. A. Ta, N. T. Tran, T. D. Trieu, J. Urban, K. Vu and R. Zumkeller, A formal proof of the Kepler conjecture, Forum Math.\ Pi 5 (2017), e2.
  10. L. H. Loomis and H. Whitney, An inequality related to the isoperimetric inequality, Bull. Amer. Math. Soc. 55 (1949) 961--962.
Show all 14 referencesShow fewer references
  1. P. Scholze, Liquid tensor experiment, Exp.\ Math.\ 31 (2022) 349--354.
  2. The Lean community, The Liquid Tensor Experiment, https://github.com/leanprover-community/lean-liquid, 2022.link
  3. F. van Doorn, P. Massot and O. Nash, Formalising the hh-principle and sphere eversion, in: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), 121--134.
  4. The Zenodo record of this paper (all versions), https://doi.org/10.5281/zenodo.23480809, whose current version also holds the formalization and its working records: the Lean sources of the audited commit e8e86d3 (§ s:stats ), with the report of their release checks; the written-out proofs and their referee reports; and the list of findings.DOI

Version history

  1. v1 · 19 pagesSubmitted by Tejasvi Singh TomarPublished on Zenodo: https://doi.org/10.5281/zenodo.23752572CurrentNov 12, 2026