  We establish the undecidability of 2019 puzzle game Baba is You through a
reduction from the Post correspondence problem. In particular, we consider a
restricted form of the Post correspondence problem introduced by Neary
(arXiv:1312.6700) that is limited to five pairs of words. Baba is You is an
award winning tile-based game in which the player can reprogram the game's
mechanisms by pushing blocks that spell out the rules. We achieve
undecidability through a generalization of the size of the playfield in the
horizontal direction, adding a "hallway" to one side of the level. The
undecidability of Baba is You has been claimed several times online using
different source problems, including the simulation of Turing machines and
Conway's Game of Life, however, this contribution appears to be the first
formal proof of the result.
