Allow me to quote part of the introduction of chapter 9 of Lovász: Combinatorial Problems and Exercises.
The chromatic number is the most famous graphical invariant; its fame being mainly due to the Four Color Conjecture, which asserts that all planar graphs are 4-colorable. This has been the most challenging problem of combinatorics for over a century and has contributed more to the development of the field than any other single problem. A computer-assisted proof of this conjecture was finally found by Appel and Haken in 1977. Although today chromatic number attracts attention for several other reasons too, many of which arise from applied mathematical fields such as operations research, attempts to find a simpler proof of the Four Color Theorem is still an important motivation of its investigation.
So here it's not so much the proof but the search for a proof that has given something extra over just believing the theorem. Does that still count as an answer to this question?
