To me, the four-color theorem is a very interesting proof of concept, perhaps the most interesting mathematical proof of the past 50 years. Perhaps the "pattern that can be used in future work" is the idea of having computers enumerate a large number of cases, which they then solve in individually straightforward ways.

But, I can understand if pure mathematicians don't feel this way. This might be only really an intriguing and beautiful concept to someone who is interested in scaling up algorithms and AI.