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.