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

The paper [U1], "Area law for three-dimensional U(1) lattice gauge theory with the Wilson action at every coupling" (doi:10.5281/zenodo.23445737), 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. Files: u1-lean-formalization.pdf: this paper, which describes the formalization; u1-lean-formalization-source.zip: its LaTeX source. u1lean-02a34e3.zip: the Lean formalization. It contains the library (U1/, U1.lean), the build files (lakefile.toml, lake-manifest.json, lean-toolchain), PrintAxioms.lean, LICENSE, README.md, AXIOMS.md (the interfaces and hypothesis structures of the proof, and how each was discharged), LABELS.tsv (the LaTeX labels of [U1] with their printed numbers), FINDINGS.md (the issues that the formalization found in [U1], with the status of each), blueprint/ (the map from paper results to Lean names) and audit/ (the audit reports, with the Lean check files in audit/probes/). stageC-written-out-proofs.zip: the nine written-out proofs that the formalization follows, in their final versions after the review, with the corrections made since, together with their PDFs and the nine referee reports. They are kept unmodified as a record; the current versions form Part S4 of the supplementary material of version 2 of [U1]. changes.md: the list of corrections to [U1], 70 entries, each with replacement text. To check the main theorems, install elan and run lake exe cache get, lake build U1 and lake env lean PrintAxioms.lean in the root of the unpacked Lean archive. The last command prints the statements of the main theorems and their axioms. The Lean code (in the Lean archive) is released under the Apache License 2.0, see its LICENSE file; the papers and other texts are released under CC BY 4.0. The statement on the use of AI tools in this paper applies to every file of this record. Mathematics Subject Classification (2020): 68V20, 03B35, 81T25, 82B20.