%======================================================================
\section{Introduction}\label{s:intro}

In three-dimensional $U(1)$ lattice gauge theory, Polyakov's mechanism predicts that static charges are confined at every
coupling: magnetic monopoles form a plasma that screens the magnetic field, and the electric flux between two
opposite charges is squeezed into a tube of finite tension, so that their energy grows linearly with their distance. In
the lattice model, the Wilson loop of a rectangle with sides $R$ and $T$ describes such a pair at distance $R$ over a
time $T$, and confinement means that it decays exponentially in the area $RT$. G\"opfert and Mack [GM82] proved confinement at every coupling for the Villain action.
For the Wilson action it remained open until the author's paper [U1]. This paper describes a formalization of that proof
in Lean~4. We first recall the theorem. Let
$\Lambda\subset\mathbb Z^3$ be a finite box, $\beta>0$ the coupling, and let $\langle\cdot\rangle^W_{\Lambda,\beta}$ be the expectation in the
$U(1)$ Wilson measure on $\Lambda$ with free boundary conditions. For a rectangle $C$ in a coordinate plane, with sides $R$
and $T$, write $\theta_C$ for the sum of the link angles around $C$.

\begin{theorem}[{[U1, Theorem 1.2]}]\label{thm:main}
There is a constant $c$ such that for every $\beta>0$ there are $\sigma(\beta)>0$ and $R_1(\beta)$ with
\[
\langle\cos\theta_C\rangle^W_{\Lambda,\beta}\le\exp\bigl(-\sigma(\beta)RT+c(R+T)\bigr)
\]
for every rectangle $C$ in a coordinate plane with $\min(R,T)\ge R_1(\beta)$ and every finite box $\Lambda\supseteq C$. Moreover,
for every $K>\Kstar=377.38$ there is $\beta_0(K)$ such that for $\beta\ge\beta_0(K)$ one can take
$\sigma(\beta)\ge1.35\cdot10^{-4}c_gc_L(K\beta)^{-1/2}e^{-2.49436K\beta}$, with $c_g=\frac14$ and $c_L=1.6\cdot10^{-19}$, and for $\beta<\beta_0(K)$ the values of $\sigma$ and
$R_1$ chosen at $\beta_0(K)$.
\end{theorem}

From here on, numbers of sections, results and displays without further indication refer to [U1], and sections of this
paper are cited with the sign~\S. [U1] also deduces an area law for compact gauge groups $G\subseteq U(n)$ that contain
the scalars, with or without a Higgs field blind to the centre of $U(n)$ (Corollary 1.3), and for the Georgi--Glashow model at infinite
Higgs coupling (Corollary 1.4). Appendix~E of [U1] shows why the proof compares the Wilson loop with Villain loops in which some couplings are infinite:
on every finite box, an inequality between Wilson and Villain loops that holds for all charges, even with a perimeter factor, forces the
Villain side to contain arbitrarily large couplings (Corollary E.4 and Proposition E.6).

The proof in [U1] is long, 155 pages with Parts S1 and S2 of its supplement and 185 more in Part S4, and its core carries over
the Debye-screening analysis of Brydges and Federbush [BF80] and the multiscale expansion of G\"opfert and Mack [GM82] to new
domains, ``with changes'' and with all constants explicit. A proof of this kind is hard to check by reading, and the sources
it adapts contain steps that need correction; [U1] itself notes one in a tree-graph count of [B78]. A formal proof checks
every step and every constant, including those of the adapted arguments.

We formalize Theorem~\ref{thm:main}, both corollaries, Fr\"ohlich's comparison (Proposition 9.1) and all results of
Appendix~E in Lean~4 [Lean4] with Mathlib [Mathlib]. Seventeen Lean theorems (Theorem~\ref{thm:formal} and
Table~\ref{tab:formal}) state these results and the infinite-volume form of the area law (Remark 8.1).

The proof in [U1] has four steps, which Section 8 combines into a chain. A comparison (Section 2) bounds the Wilson loop
by an average of Villain expectations at the coupling $\tau=K\beta$ over random sets of frozen plaquettes, whose Villain
coupling is infinite. A deterministic regularization (Sections 3--4) turns each frozen set into a slit domain with good
geometry, in which the frozen plaquettes are insulating walls. On each slit domain, an iterated Mayer expansion down to the Debye scale and a single-scale expansion, built on [BF80] and [GM82]
(Sections 6--7), prove a deterministic area law in terms of the minimal cut area, the least number of
unfrozen plaquettes in an integer $2$-chain bounded by the loop. A Peierls estimate, which [U1]
calls the min-cut lower tail and we call the contour bound (Section 5), shows that this area is close to $RT$ outside a rare
event. Section 9 deduces the corollaries. Appendix~E stands apart from this chain; its proofs combine the dual formula for
Gibbs expectations, Ginibre's inequality, Gaussian sums over lattices and H\"older's inequality with two computations on the
boundary of a cube.

We organized the formal proof as a chain of interfaces, that is, Lean structures and propositions that state exactly what
one part of the proof passes to the next, so that the parts could be formalized independently and the assembly checked separately
(\S\ref{s:arch}). Before formalizing the steps that [U1] adapts from the literature, we wrote each of them out as a
self-contained document that states its inputs and outputs, and during the formalization we did the same for the steps
that [U1] leaves out. Each document was checked line by line in a separate review, and the formal proof follows these nine documents
(\S\ref{s:blueprints}). Every numerical constant of the proof is certified in Lean by
kernel-checked computations, and the kernel itself decides the two rational inequalities behind the bounds on Watson's
integral (\S\ref{s:numerics}). Appendix~E is formalized with the same definitions (\S\ref{s:appE}). We also compiled a list
of corrections and improvements to [U1], each with replacement text (\S\ref{s:findings}).

\emph{Related work.} Long proofs have been formalized before, among them the odd order theorem in Coq [GAA+13], the Kepler
conjecture in HOL Light and Isabelle [HAB+17] and the main theorem of the Liquid Tensor Experiment in Lean [Sch22, LTE22]. As
in the formalization of the sphere eversion theorem [vDMN23], large parts of our formal proof follow informal documents
written for it; here they are the written-out proofs of \S\ref{s:blueprints}, which also state the inputs and outputs of each
part.