I have a question as to why the four color theorem has not been proved by hand.
I believe that to prove the four color theorem, it suffices to show that a complete graph may only be planar if it has 4 or less vertices. One may then construct a complete graph of this type, and use the Jordan curve theorem to define the interior and exterior of the graph. Finally, one can show that by introducing a new vertex to either the interior or exterior of the graph and attempting to make a complete graph with the new vertex, this new graph cannot be planar. Would an acceptable proof of this type be possible, or would it necessitate high-powered computation, as previous proofs of the four-color theorem have?