Indeed, and the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find. "Proved but not insightfully" is a problem status some mathematicians are starting to think of as closer to "open" than "closed", which is a good thing IMO. (I am not a mathematician, though)

Maybe the new heuristic auto tactics will lower the cost of finding the human proof of the four color theorem enough to be affordable in the current environment.