  In this article, we develop a method to perform constructive proofs of
existence of smooth planar localized patterns in the Gray-Scott model.
Specifically, we construct a natural Hilbert space $H^l$ for the study of
systems of autonomous semi-linear PDEs, on which products and differential
operators are well-defined. Then, given an approximate solution $\mathbf{u}_0$,
we derive a Newton-Kantorovich approach based on the construction of an
approximate inverse of the linearization around $\mathbf{u}_0$. In particular,
we derive a condition under which we prove the existence of a unique solution
in a neighborhood of $\mathbf{u}_0$. Such a condition can be verified thanks to
the explicit computation of different upper bounds, for which analytical
details are presented. Furthermore, we provide an extra condition under which
localized patterns are proven to be the limit of an unbounded branch of
(spatially) periodic solutions as the period tends to infinity. We then
demonstrate our approach by proving (constructively) the existence of four
different localized patterns in the 2D Gray-Scott model. In addition, these
solutions are proven to satisfy the $D_4$-symmetry. That is, the symmetry of
the square. The algorithmic details to perform the computer-assisted proofs are
available on GitHub.
