Pokémon is NP-hard: enemy trainers alone suffice
ProvedNintendo.pokemon_npTheorem 7.2 of Aloupis, Demaine, Guo, and Viglietta's paper (Theoretical Computer Science 586 (2015) 135-160): deciding whether a level of Pokémon is solvable is NP-hard, and the enemy trainers alone suffice — no wild Pokémon are needed. The formal statement is the explicit-level 3-SAT hardness predicate over the Pokémon level family of the worlds layer: there is a constant such that every 3-CNF formula has a level — walls and enemy trainers only — whose size is at most the constant times the square of the formula's size and which is solvable, the player reaching the goal alive from the start, exactly when the formula is satisfiable. The gadgets are the trainers themselves: their lines of sight, blocked by walls and by other trainers' bodies, the battles that interrupt a seen step, and the luring move that draws a line-of-sight trainer to the adjacent cell, with weak trainers defeated and strong trainers killing.
Formalization Note The levels are levels of the worlds-layer Pokémon model with no wild encounters; 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 7.2 of the paper: Pokemon is NP-hard, and enemy trainers alone suffice. -/
theorem pokemon_np :
LevelHard3Sat pokeGame pokeStart pokeGoal pokeLevelSize := 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 Pokémon level — walls and enemy trainers only, no wild Pokémon — 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. The trainers are as defined in the worlds layer: each sees along its line of sight, blocked by walls and by other trainers' bodies, or stands adjacent; a seen battle interrupts the step, a line-of-sight trainer being lured to the adjacent cell along its facing; a weak trainer is defeated and a strong one kills.