The "proof" you're most likely talking about doesn't show why this is true. Merely shows that it is true.
Exhaustion doesn't qualify as a real argument, in my opinion.
Exhaustion doesn't qualify as a real argument, in my opinion.
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.
So, why make the cut-off point of when exhaustiong is an explanation at some finite number of cases?
To be fair, though it's a bit ambiguous, I read sebastialonso's post https://news.ycombinator.com/item?id=8799362 as indicating that he or she believes that the result is true—i.e., does not necessarily reject the validity of proof by exhaustion as a style of argumentation—but does not feel that the proof by exhaustion is an explanation.