# Help me prove the Four Color Theorem!

This is not just another challenge asking you to color random maps... In this challenge, you are asked to write a program that is actually used in the formal proof of the Four Color Theorem.

First I shall describe the challenge without any background or motivation, for the impatient.

A chromogram is a list made of the symbols - [ ]0 ]1, where the brackets are required to match. A coloring is just a list made of 1, 2 and 3's whose bitwise sum is zero. A coloring is said to fit a chromogram if:

• They are of the same length.
• -'s in the chromogram corresponds to 1's in the coloring at the same positions.
• Brackets corresponds to 2's and 3's. For matching brackets, if they are [ ]0 then they correspond to the same color, and different colors if they are [ ]1.

Some examples:

Chromogram      <-> Coloring
[ [ - ]1 - ]0 - <-> 2 3 1 2 1 2 1
[ [ - ]1 - ]0 - <-> 3 3 1 2 1 3 1
[ ]1 -          <-> 2 3 1
[ ]1 -          <-> 3 2 1


Given colorings $$\C\$$, a compatible coloring is one such that each of its chromograms fits with some $$\c\in C\$$ (different chromograms can fit different colorings). We define a suitable coloring with the following rules:

• All colors in $$\C\$$ are suitable.
• For a suitable coloring, switching 1, 2 and 3's consistently produces another suitable coloring. E.g. 12321 -> 21312 or 32123 or 13231, but not 11311 or 12331. Formally, if $$\\rho\$$ is a permutation of $$\\{1,2,3\}\$$, then if $$\\langle c_1, c_2, \dots, c_n \rangle\$$ is a suitable coloring, $$\\langle \rho c_1, \rho c_2, \dots, \rho c_n \rangle\$$ is also one.
• For a set of suitable coloring, all its compatible colorings are suitable.
• All the suitable colorings are generated by the rules above.

Now the challenge:

Challenge. Input a set of coloring $$\C\$$, determine if all the colorings of the same length are suitable. This is .

A hint: A sequence of 1, 2 and 3's have the bitwise sum zero if and only if the parity of each kind of number are the same, i.e. the numbers of occurrences of 1's, 2's and 3's are all odd or all even. But probably checking bitwise sums are more golfy.

Now it's time for stories. The Four Color Theorem states that any planar map can be colored with four colors, so that the regions that meet at boundaries are colored differently. I'll try to briefly describe the proof of the Four Color Theorem, in steps.

1. First, if you create a tiny region at every corner (i.e. where three or more regions meet), you get a map where no more than three regions meet at a point, and if you can color these kind of maps, you can remove the added region and recover a coloring of the original map. These special maps are called cubic.
2. Now we reason by reductio ad absurdum. Consider the smallest cubic counterexample. Any map smaller than that will be 4-colorable.
3. Next, by a method of discharging, we compute a score for each region, ensuring that the average score is less than 6. This means that there must be at least one region with score less than 6. In this way we locate a "weak spot" of the putative counterexample, where we are going to attack.
4. We, by the aid of a program (not related to this challenge), prove that the neighborhood of the weak spots that we may find always falls in one of the 633 possibilities. This allows us to do a case-by-case analysis.
5. In each case, we remove some boundaries in the neighborhood of the weak spot, creating a smaller map. By hypothesis, this map is 4-colorable. We then try to recolor the original map based on the smaller map, only adjusting the colors in the neighborhood. This is not always possible. So we try to adjust the outer regions also. This is difficult because changing one regions's color may affect other regions. We now develop a more convenient tool.
6. Notice that if, instead of coloring the regions by colors $$\0,1,2,3\$$, we color the boundaries of the map, by computing the bitwise sum of the two regions on either side of the boundaries, we can color the boundaries with $$\1,2,3\$$. It can be proven that the original coloring can always be recovered from the boundary coloring. Now the situation is clearer. Note that exactly 3 boundaries meet at a corner, and they always have different colors. Suppose we want to change an boundary color from 2 to 3 (the boundary sticks out from the neighborhood we just considered, so it will be consistent with the colors in the neighborhood), the only hinderance is the edge colored 3 connected to it (there is only one such edge extending outwards, can you see why?). If we change that 3 into 2, a further edge colored 2 will protest! In this way, we can go on and on in a chain. And the key insight is that the chain cannot intersect itself, so it will always come back sticking into the neighborhood again.
7. So now, the boundaries colored 2/3 will form arches standing on the edge of the neighborhood we are considering. These arching structures are captured by our chromograms, and the colors of the boundaries sticking out of the neighborhood are represented by the colorings in our challenge. Now if you reread the challenge, you will understand that, given the recoloring that we have for the neighborhood, the challenge is to determine if every possible coloring for the outer map can be adjusted to match.

Phew! That was, alas, the briefest that I can manage without losing too much detail! You can see that our challenge is only concerned with the last step, and there are more potential challenges lurking about. But this I leave to those who are interested. You can consult this paper for a more detailed account. I hope this challenge can kindle some interest in the four color theorem and its proof.

Routine code-golf test cases:

T 123
T 1111,2323
F 1111,2332
T 11123,12113,12311
F 11123,12113,12131
T 111111,123132,123231,123312,123213,112323,121222,122122,122212
F 123132,123231,123312,123213,112323,121222,122122,122212
F 123231,123312,123213,112323,121222,122122,122212
F 111111,123312,123213,112323,121222,122122,122212
T 111111,123231,123213,112323,121222,122122,122212
F 111111,123231,123312,112323,121222,122122,122212
F 111111,123231,123312,123213,121222,122122,122212
F 111111,123231,123312,123213,112323,122122,122212
T 111111,123231,123312,123213,112323,121222,122212
F 111111,123231,123312,123213,112323,121222,122122
F 111111,123132,123312,123213,112323,121222,122122,122212
T 111111,123132,123231,123213,112323,121222,122122,122212
F 111111,123132,123231,123312,112323,121222,122122,122212
F 111111,123132,123231,123312,123213,121222,122122,122212
F 111111,123132,123231,123312,123213,112323,122122,122212
T 111111,123132,123231,123312,123213,112323,121222,122212
F 111111,123132,123231,123312,123213,112323,121222,122122


I hesitate to include larger test cases, because to do those in reasonable time, some algorithm other than the most naive one is needed. I don't want to complicate things too much, since they are already so complicated. Better algorithms can be found in the linked paper.

• This hasn't been through the sandbox, so please ask whenever you feel something is unclear. Explaining all these clearly is pushing my ability to explain clearly to its limits! – Trebor Jun 9 at 15:45