I think the 4-color theorem is rather different though. It reduced to a large number of cases that can in principle each be verified by a human, if they were so

I think the 4-color theorem is rather different though. It reduced to a large number of cases that can in principle each be verified by a human, if they were so inclined (indeed a few intrepid mathematicians have done so over the years, at least partially.) The point of using a computer was to reduce drudgery, not to prove highly non-obvious things. Thinking back to Wiles' proof of FLT, it took the community several years of intense work just to verify/converge on the correct result. And that proof is ~130 pages. So, what if the computer produced a provably correct, 4000-page proof of the Goldbach conjecture?