User:Hakerh400/Angel problem

In this article we discuss the formalization of The Angel Problem and its proof.

Definition of the problem

The Angel Problem is about the Angel Game proposed by John Horton Conway. The Angel Game is played by two players on an infinite chessboard. In this article we refer to the players as A and D (think of them as Alice and Darth, but we refer to both players as he/him for simplicity). Player A has a power pw (a natural number) specified before the game starts.

The board starts empty with player A located in one tile (square). On his turn, player A jumps to a different empty tile whose distance from the current tile is at most pw in the infinity norm. On his turn, player D adds a block on any single tile not containing player A and that has not been blocked by D already. Player A may leap over blocked tiles, but cannot land on them. Player D wins if player A is unable to move. Player A wins by surviving indefinitely.

Question: For what values of pw does player A have a winning strategy?

History

The problem first appeared in 1982. Conway and Berlekamp proved that for power 1, D has a winning strategy. In 2006, Brian Bowditch proved that for power 4, A has a winning strategy. Later in 2006, András Máthé proved that A with power 2 has a winning strategy. This fully resolved the problem.

Our goal

We started the project to fully formalize András Máthé's proof in Lean 4, without using any form of AI. The goal is not only to ensure the proof is correct, but also to fully understand the proof and improve our formalization skills.

Formalizing theorems from abstract algebra or category theory is usually a piece of cake. Everything fits together nicely, it is often easy to come up with canonical definitions and all proofs are more-or-less canonical, because formal systems that are based of inductive types (such as Lean) are the ideal tools for reasoning about abstract algebras. However, formalizing the Angel Problem is significantly more difficult for two reasons:

There are almost no useful theorems from Mathlib that can be applied to this problem
Coming up with good definitions and developing API for them is a form of art and is often very challenging

Definitions

There are many ways to formally define the Angel Problem. We present the following definitions [1], but we also prove that this formulation is equivalent to two other formulations.

State transition system

Before we start defining the Angel Problem, we first developed the library of state transition systems. [2]

A system is a structure containing [3] :

The set of initial states
The transition function: takes a state and a transition, and returns a new state or nothing (nothing means the transition is not valid in that state)

Reachability [4] :

From every state we can reach itself (reflexivity)
If from state x there is a transition to state y, and from y we can reach z, then from x we can reach z

A state is said to be valid if it is reachable from some of the initial states. [5]

Applying a list of transitions to a given state results in a pair of two things: the resulting state up to the first invalid transition (or up to the end of the list if all transitions are valid), and the remaining transitions starting from the first invalid transition (or the empty list if all transitions are valid). [6]

Simulating a function that takes a state and returns a transition for n steps results in a pair of two things: the resulting state up to the first invalid transition reachable in less than n steps (or up to n steps if all transitions are valid), and the number of remaining steps that are not performed (or 0 if all transitions are valid). [7]

Transition function is a function that maps states to transitions, such that if there is a valid transition in the given state, the function must return a valid transition. [8]

The angel problem

Game state consists of [9] :

The A's power (does not change during the game)
The finite set of taken tiles (tiles blocked by D)
The current A's position
Whose turn it is
The history of moves

Transitions (moves) and tiles are points with integer coordinates. [10] Since A's move is a point (where it jumps) and D's move is also a point (what tile it blocks), we represent moves of both players using the same data type: the point. A strategy for player A, as well as for player D, is a function that takes a state and returns a move (transition). [11] [12] System strategy (simulation function for the entire system) is a pair of A strategy and D strategy. [13]

Initial game state is parametrized by A's power pw and A's starting position [14] :

A's power is pw
The set of taken tiles is empty
The current A's position is the starting A's position
It is D's turn (by convention D plays first, since it does not make much sense for A to play first)
The move history contains just the current A's position

After a move is performed, the player turn is flipped and the current move is prepended to the history of moves. [15]

For a given state and a given strategy (pair of A's and D's strategies), player A wins iff for any natural number n, simulating the strategy for n steps does not leave remaining steps (meaning the simulation successfully executed for n steps). [16] D wins if there exists a natural number n, such that simulating the strategy for n steps leaves remaining steps. [17]

For a given state, player A has a winning strategy iff there exists A strategy, such that for any D strategy, A wins. [18] D has a winning strategy iff there exists a D strategy, such that for any A strategy, D wins. [19]

For a given power pw, A has a winning strategy iff for any initial game state where A's power is pw, A has a winning strategy. [20] D has a winning strategy iff for any initial game state where A's power is pw, D has a winning strategy. [21]

Progress

Here is what we have formalized so far and what remains to be done.

✔ Determinacy: In any state, exactly one player has a winning strategy. [22] [23]

Proving that If one player has a winning strategy, then the other does not, was easy. [24] However, proving that if one player does not have a winning strategy, then the other does, was trickier. It follows from a compactness argument. To prove that A has a winning strategy when D does not, we have to construct A's strategy that always seeks a state in which D does not have a winning strategy. [25] [26]

✔ A's starting position does not matter. [27] [28]

This is a trivial observation. Since at the beginning all tiles are free, every tile in the grid is equivalent to any other tile. So, no matter where A starts, it does not influence the existence of winning strategy.

✔ Access to move history does not matter. [29] [30] [31] [32]

One may argue that since in our definitions we allow players to access the move history, it may somehow give them extra capabilities. We disprove this by showing that for each of the four combinations (no player sees history, only A sees history, only D sees history, both see history), the existence of winning strategies remain the same.

✔ If A has a winning strategy, then A of any higher power also has a winning strategy. [33]

This is simple: since A of a higher power can perform all the moves that the original A can, it can copy the winning moves of the original A.

✔ If D has a winning strategy, then there exists a natural number n, such that D can defeat any A in at most n moves. [34]

If that was not true, A could always make one more move, thus constructing a winning strategy. Therefore, D must be able to defeat any A in a fixed number of moves.

✔ A with power 0 does not have a winning strategy. [35]

This is trivial: since A has power 0, it cannot perform any move at all, loosing immediately. Some formulations of the problem do not allow A to have power 0, but we proved this theorem anyway.

⚠ A with power 1 does not have a winning strategy. [36]

This took a lot of effort to formalize. We first proved that if A (with power 1) is at least 6 tiles away from a horizontal or vertical edge, D can prevent A from ever reaching the edge. [37] Then we proved that we can combine a vertical and a horizontal edge to form an impassable corner [38] Then we proved that four corners can be combined to form a closed box (of size 213 x 213 tiles). [39] Conway and Berlekamp proved that D can entrap A in a box of size 33 x 32, but their proof is extremely difficult to formalize, so we decided to ignore their optimizations and use a large box. In the proof of this theorem, we used native_decide, which is a tactic that efficiently performs large computations, but relies on the Lean's external compiler. Therefore, this is technically not considered a trusted proof. We are working on getting rid of native_decide, but it may take a while.

✔ Subset of taken tiles: If A has a winning strategy in some state, then A has a winning strategy for the state obtained by unblocking any number of blocked tiles. [40]

Similarly, if D has a winning strategy in some state, then D has a winning strategy for the state obtained by blocking any number of additional tiles. [41]

✔ Fresh A: If A has a winning strategy, then A has a winning strategy that never jumps to a tile that he has already visited, or the tile where he could have already landed at a previous time, but did not. [42]

This was very difficult to prove. The Conway's original proof is only three paragraphs long, but it is very imprecise. We had to develop a framework for reasoning about player strategy modifications. [43] We actually proved a more general theorem: if A has a winning strategy disjoint [44] from a family of sets of points indexed by moves, then A has a winning strategy that never jumps to a tile that he has already visited, or the tile where he could have already landed at a previous time, but did not, and the new strategy is disjoint from a superset of the original family of sets of points.

🛇 Nice D: A Nice D is a D who never eats a tile on which A has previously stayed, nor a tile on which A could have jumped at a previous move, but did not. If D has a winning strategy, then Nice D can entrap A (restrain A in a finite set of tiles).

(in progress) We have a fully elaborated proof on paper, but we will only formalize it after we prove that the alternative formulations of the Angel Problem are equivalent to our definitions.

🛇 A with power 2 has a winning strategy. This is the final theorem.

(in progress) We are far from this theorem.

Alternative formulations

There are two known alternative formulations of the problem and we are working on proving that our definitions are equivalent to each of the alternative formulations.

🛇 Dependently typed formulation [45]

(in progress) This turned out to be harder than we expected, because in this formulation a single transition encompasses a pair of D's and A's move. Also, the move history is handled differently. It will take a while until we establish the equivalence.

🛇 Inductive formulation

(in progress) We will do this after we fully formalize the dependently typed version.