The hard part in proving the four color theorem is proving that there aren't any possible maps that can't be colored with four colors. Perhaps there's one out there that needs five and can't be colored with only four.

Proving some maps can't be colored with three colors is easy, you only need to find one and enumerate all the three-colorings and find none of them work.

It's not really a theorem about colors though, they're just labels.

I know it's not about actual colours, I did say it was off-topic. :)

Re proving any, I replied to a sibling comment. What I was imagining was the inverse - proving that you can't construct one that requires a fifth.

It's straightforward to prove that you can't have more than four plane regions that all mutually touch; K5 is a nonplanar graph. But you can construct maps (planar graphs) that have no K4 subgraphs that nevertheless have chromatic number 4. C5 plus an additional node connected to all 5 of its nodes, for example. The challenge is to show that the same thing can't happen with chromatic number 5. I think it does happen with chromatic numbers 6 and 7 on the surface of a torus (but you can also just map K7 onto a toroidal map.)

I recognize that this comment includes jargon, but I assume you'll Google it. I'd include diagrams but HN doesn't support them.

Thank you for giving me the terminology - I think I do see why it's hard mathematically, I just struggle to understand that graphically, it seems so obvious on paper - looking by cases at how many existing regions a necessarily new colour touches.

But, I understand and trust the mapping of the problem to a graph, so perhaps if I see why the problem is hard on a graph that should be enough for me.

But my reasoning was along the lines (but now in my newfound terminology) of:

K1 - trivially 1 colour needed. K2 - 2.

If we add another region on the map, we either have K3 or K1,2. In the latter case the third region/vertex need only be different to the one it touches, but K3 clearly needs 3 colours.

Adding the fourth region is similar, and again K4 clearly needs 4.

The fifth region touches at most 3 others, since K5 is non-planar. Thus, it can take the colour of the untouched region.

That's not very formal, but why isn't proof by induction easy from there? i.e. if we can't build a map that ever requires a fifth colour, then it can't be that there exists a map which requires more than four?

Try the C5-plus-another-thing exercise.

But why does it matter if I can tell you how to colour it,* isn't it sufficient to show that we can't construct one that can't be coloured in at most four, as I tried to outline above? Surely it must then be that any exercise is either 4-colourable, or non-planar/otherwise out of scope of the problem?

* It's easy starting from the end, just put one colour in the middle, then alternate second/third colours around the edge until you get back to the start and have to add a fourth. From construction, the worst case is from K1,2 then adding another for K1,3 at which point we need four colours already, but when we add two more on what will be the C5# around they each only connect to one each side and the center. In adding each one you can simply use the colour one hop over on the circumference.

# Since the center of K1,3 must be the center of the final C5-plus-thing, as it already had 3 spokes.

It's correct, as you say, that if we can't build a map that ever requires a fifth colour, then it can't be that there exists a map which requires more than four.

It's just that the C₅-plus-thing requires four colors, even though it doesn't contain any K₄ induced subgraphs. So we could imagine that there might be some larger planar graph that requires 5 colors without containing K₅. As it turns out, there isn't, but that's the thing that's hard to prove.

Hm, many thanks for the pointers. It's still not completely clear to me, but I have a much better idea and know the story of thing to search/read up on. Cheers.