The 2020 paper “Recursed is not Recursive: A Jarring Result” by Demaine, Kopinsky, and Lynch (ISAAC 2020) proves that deciding whether you can win a level of the video game Recursed is RE-complete, which implies that there is no finite algorithm to solve the problem (undecidability).
Here are "screenshots" (actually SVG renderings of the rooms
produced by SVG Tiler)
of some of the key rooms in the level
(as generated by the Makefile).
See the paper for details about how the rooms work and interconnect.
The specific level presented here is a minimal example of the reduction
from that paper, representing an instance of the
Post Correspondence Problem
with just two dominoes: [a|ab] and [ba|b].
The level is winnable (by selecting each domino once in turn),
but it is quite difficult to do so in practice.
Lua level generated by recursed-xls2lua
To play the level, put the Lua file into Recursed's custom/missions folder;
see these instructions.
The level above is generated by recursed-xls2lua from this .xlsx input file, which in turn is exported from this Google Sheet.