The four color theorem is one of the least satisfying proofs I have ever seen, and I've gone through thousands by hand. It's because the final stage is reduced to computer verification...it's unsatisfying.
Does anyone know if Cahit's Spiral Chains proof (<https://arxiv.org/abs/math/0408247>) was found to have issues? It is much more elegant, as it avoids the exhaustive computer case verification...
That's not actually what's happening really (edit: although an important prior result is that every planar graph must have at least one node of degree at most 5, i.e. at least one vertex that has at most 5 edges incident to it). Instead of that little bit say, "assume we're looking at the minimal counter-example. Then we're going to show how we can actually color a graph smaller than the minimal counter-example with 4 colors." The false proof is REALLY cool and is a correct proof of the FIVE-color theorem, which shows that you can color every graph with 5 or fewer colors.
It relies on a construct known as "Kempe chains" [0] which is a chain of C1-C2-C1-C2-C1-C2 starting at the first vertex and either never connecting back (in which case you can reverse the colors, no problem) or connecting back (in which case you must be able to reverse a chain of C3-C4-C3-C4).
The error is that the chain of C1-C2 and C3-C4 can connect back to the original vertex ADJACENTLY to each other. So it fails for the four-color theorem. But it does prove the 5-color theorem, as there is no room for a color C5 to squeeze in there without being allowed to change.
Kempe's true proof of the 5-color theorem is probably my favorite proof in all of math.
But you accept that it can be colored with (at most) four colors, e.g. by coloring the central one color 1 and the other one billion color 2? Then you also can imagine the reduction. Each of these outer-inner node pairs is a reduction. Your big graph consists of overlaying one billion two-node graphs by merging on the color 1 node.
