There is a step in the proof which is brute force. The proof is sort of giving a recursive algorithm for 4-coloring: for certain subgraphs, you simplify it, color the result, and use the coloring to color the original graph. There are 633 cases ("reducible configurations") in the recursion, and the annoying part is checking that all 633 actually work. After Haken and Appel, Gonthier wrote a Coq proof http://www.ams.org/notices/200811/tx081101382p.pdf

Sometimes I imagine that if we had much larger short term memories, an argument with only 633 cases would be obvious.