Most of this proof is very dense. But Theorem 7 seems like an interesting tactic that allows the authors to infer nonexistence from rarity:

>Theorem 7. If there is a map L which cannot be 4-coloured then only an exponentially small fraction of the maps with n edges can be 4-coloured.

It's one of those things that seems obvious in retrospect — of course large random graphs should be likely to contain any particular graph! But it hadn't occurred to me in my own (very amateur) considerations of the problem.

Will be interesting to see if it's correct. We've gone from an argument too long for a human to read to one in just seven pages.