  A fundamental problem in Distributed Computing is the Pattern Formation
problem, where some independent mobile entities, called robots, have to
rearrange themselves in such a way as to form a given figure from every
possible (non-degenerate) initial configuration.
  In the present paper, we consider robots that operate in the Euclidean plane
and are dimensionless, anonymous, oblivious, silent, asynchronous, disoriented,
non-chiral, and non-rigid. For this very elementary type of robots, the
feasibility of the Pattern Formation problem has been settled, either in the
positive or in the negative, for every possible pattern, except for one case:
the Square Formation problem by a team of four robots.
  Here we solve this last case by giving a Square Formation algorithm and
proving its correctness. Our contribution represents the concluding chapter in
a long thread of research. Our results imply that in the context of the Pattern
Formation problem for mobile robots, features such as synchronicity, chirality,
and rigidity are computationally irrelevant.
