Compactness of domino tilings I've read in Lemma 2 of the paper 1 that if every square region of the plane admits a tiling, then the whole plain admits a tiling, but the proof is omitted.  This sounds like a compactness property, but I don't see how easy can be proven.

I added the tag "automata theory" because there is a correspondence between Wang tilings and finite state transducers.
Yes, this is a compactness property.

Let $X$ be the region you want to tile, and $T$ the finite set of possible tiles. The space $T^X$ of all assignments of tiles to $X$ is compact by Tychonoff’s theorem. For any finite $X_0\subseteq X$, the set $C_{X_0}\subseteq T^X$ of all correct tilings of $X_0$ is closed (in fact, clopen), and since $C_{X_0\cup X_1}\subseteq C_{X_0}\cap C_{X_1}$, they generate a filter. Thus, assuming every finite subset of $X$ can be tiled, the system $\{C_{X_0}:X_0\subseteq X\text{ finite}\}$ has fip, and by compacteness, its intersection is nonempty. This intersection is the set of all correct tilings of $X$.

Instead of all finite $X_0$, it suffices to use any family of finite subsets which is upwards directed and covers $X$, such as, in your case, the set of all finite square subregions of the plane.

Alternatively, you may set up the argument to use the compacteness of classical propositional logic: let $\{p_{x,t}:x\in X,t\in T\}$ be a set of propositional variables, and let $C$ be the theory consisting of the formulas
$$\begin{gather*}
\bigvee_{t\in T}p_{x,t},\qquad x\in X,\\
\neg(p_{x,t}\land p_{x,t'}),\qquad x\in X,t\ne t'\in T,
\end{gather*}$$
and
$$\neg(p_{x,t}\land p_{x',t'})$$
for all $x,x'\in X$ that are neighbours, and $t,t'\in T$ that are incompatible when placed on $x$ and $x'$, respectively. If each finite subset of $X$can be tiled, then $C$ is consistent, and any satisfying assignment gives a tiling of $X$.