A slightly more
rigorous definition: The
faces of any
planar graph can be labeled with at most 4 "
colors" such that no two
adjacent faces have the same label.
The proof Soft Picasso alluded to involved breaking the problem into over 1000 test cases and checking each by computer. As such, there was very little theoretical mathematics involved, so nobody really knows why it's true.
The equivalent 6-color theorem can be easily proved using elementary graph theory. The proof of the 5-color theorem is more difficult but still understandable to a first-semester student of graph theory. Once again, there simply is not a known satisfactory theoretical proof of the 4-color theorem.