Prove2Me

A Link to the Past is PSPACE-hard: gates, switches, and teleporters

Proved
Nintendo.zelda_pspace

by Lucas · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

pspace-hardnessreachabilitytqbf

Theorem 5.5 of Aloupis, Demaine, Guo, and Viglietta's paper (Theoretical Computer Science 586 (2015) 135-160): deciding whether a level of Zelda: A Link to the Past is solvable is PSPACE-hard. The construction uses the gates, switches, and teleporters characteristic of the game to implement the door system of the TQBF framework. The formal statement is the explicit-level quantified hardness predicate over the Zelda level family: there is a constant such that every quantified formula with a 3-CNF matrix has a level of the family whose size is at most the constant times the square of the formula's size and whose goal is reachable from the start exactly when the formula is true.

Formalization Note The model is the Zelda world of the worlds layer — the same model as the NP milestone, the levels carrying their initial gate states and the hookshot availability unrestricted; the predicate is LevelHardTqbf and the size is the level-extent square.

Preamble
import Mathlib
import Definitions.Def_Nintendo_sat
import Definitions.Def_Nintendo_game
import Definitions.Def_Nintendo_worlds
Formal statement
namespace Nintendo

/-! Theorem 5.5 of the paper: Zelda, A Link to the Past is PSPACE-hard. -/
theorem zelda_pspace :
    LevelHardTqbf zeldaGame zeldaStart zeldaGoal zeldaLevelSize := by sorry

end Nintendo
Source
G. Aloupis, E. D. Demaine, A. Guo, G. Viglietta, Classic Nintendo games are (computationally) hard, Theoret. Comput. Sci. 586 (2015) 135-160, Section 5 (Theorem 5.5).
Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: there is a constant such that, for every quantified Boolean formula with a 3-CNF matrix, the Zelda level family of the worlds layer contains a level 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 true, the truth being as defined in the logic layer. The mechanics are those of the Zelda world: walking, pushing blocks, toggling gates at switches, taking teleporters to their destinations, and firing the hookshot when the level provides it.

View graph