MIT researchers prove Super Mario levels are undecidable

Researchers at the Massachusetts Institute of Technology have proved that determining whether a Super Mario level is solvable is undecidable. The finding places the problem in the RE-Complete complexity class, meaning it is impossible to write a computer program that always correctly predicts if Mario can reach the castle in certain constructed levels. This result supersedes previous classifications that placed Super Mario in the PSPACE complexity class.

Led by Professor Erik Demaine, a team of four students—Hayashi Ani, Holden Hall, Ricardo Ruiz, and Naveen Venkat—achieved this result through a final project in the 2023 class Algorithmic Lower Bounds: Fun with Hardness Proofs. The team used gadget theory to create levels that simulate counter machines, demonstrating that Super Mario logic can replicate the computational power of a universal computer.

The proof relies on constructing counter gadgets that tally monsters, such as Goombas, to simulate Minsky counter machines, which are known to be undecidable. Jayson Lynch, a CSAIL research scientist who spearheaded earlier formalisation of gadget theory, noted that while he did not study the game’s undecidability in this specific instance, the door gadgets he helped formalise were foundational to the work.

The research was conducted under the placeholder name MIT Hardness Group, which is not an official research group but a label for projects in Demaine’s class. The work offers theoretical insights applicable to robotic motion planning and chemical reaction networks, showing how problems in video games can inform broader computational challenges.

The finding highlights the depth of complexity theory, where even a simple platformer can encode problems as hard as the Halting Problem. By proving that Super Mario can simulate arbitrary computers, the researchers have provided a new framework for understanding the limits of algorithmic prediction in complex systems.