Metroid is NP-hard
ProvedNintendo.metroid_npTheorem 6.1 of Aloupis, Demaine, Guo, and Viglietta's paper (Theoretical Computer Science 586 (2015) 135-160): deciding whether a level of Metroid is solvable is NP-hard. The formal statement is the explicit-level 3-SAT hardness predicate over the Metroid level family of the worlds layer: there is a constant such that every 3-CNF formula has a level whose size is at most the constant times the square of the formula's size and which is solvable — Samus reaching the goal alive from the start — exactly when the formula is satisfiable. The gadgets are Samus's own mechanics: the morph ball and its tunnels, the beam that clears the zoomers in its path, and the platforming moves between them.
Formalization Note The levels are levels of the worlds-layer Metroid model, Samus occupying two cells unmorphed and one morphed, the headroom conditions that the two-cell body forces being part of what the gadget corridors must respect; the predicate is LevelHard3Sat and the size is the level-extent square.
import Mathlib import Definitions.Def_Nintendo_sat import Definitions.Def_Nintendo_game import Definitions.Def_Nintendo_worlds
namespace Nintendo
/-! Theorem 6.1 of the paper: Metroid is NP-hard. -/
theorem metroid_np :
LevelHard3Sat metroidGame metroidStart metroidGoal metroidLevelSize := by sorry
end Nintendo
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: there is a constant such that every 3-CNF formula has a Metroid level — in the worlds-layer model, whose mechanics are Samus occupying two cells unmorphed and one morphed, walking, jumping unmorphed, falling, toggling the morph ball under support and headroom conditions, and shooting a beam of up to sixteen cells that kills every zoomer it meets until a solid tile, with zoomers killing — whose size is at most the constant times the square of one more than the formula's size and which is solvable, some goal configuration reached alive from the start, exactly when the formula is satisfiable.