Wang tiles are (by Wikipedia): "equal-sized squares with a color on each edge which can be arranged side by side (on a regular square grid) so that abutting edges of adjacent tiles have the same color; the tiles cannot be rotated or reflected."
The usual decision problem associated with them is: given a set of tiles, can they tile the plane?
This problem is known to be undecidable and has a nice history (Wang originally gave a decision procedure, but it works only if the tiles form a periodic tiling, while there exists sets which give rise only to nonperiodic tilings). It has fascinated me personally for a very long time
The state-of-the-art proof of undecidability I'm familiar with is that of Raphael Robinson ("Undecidability and Nonperiodicity for Tilings of the Plane," Inventiones Mathematicae, 12(3), 1971 pp. 177–209). It is quite a difficult proof, and I have never seen it in textbooks.
I'm familiar with a much easier version - this time the set only needs to tile a quadrant of the plane, and the corner tile is already given. This problem is much easier to handle - the given corner tile enables us to "run a Turing machine" in the tiling (each row is a configuration) and undecidability follows. However, this result is primarily a "folklore" version - I don't recall it in textbooks at all.
This leads to my question: has Robinson's method been improved but remains folklore, and so not shown in textbooks? Is there a relatively simple proof of the undecidability of the general tiling problem I'm missing?