[wetmore]

People often talk about the proof as if they just enumerated every possible planar graph and checked. Which is true in a sense, but disregards the work that went into making it possible to enumerate the cases in the first place.

There are infinitely-many possible planar graphs, so you of course need to find some invariants that allow you to bring the necessary number of graphs to check to be finite. Beyond that, the techniques in the 4CT which make it actually possible to reduce the number of cases to a feasibly enumerable number are very clever and require some insight.