The current best proof of the 4CT is a human proof, it's just that there are a lot of cases to check. It's largely just the same as the 5CT, but with more examples to run through. Using the computer is faster and avoids errors of tiredness and boredom. However, in contrast to the way it's always presented, the basic proof is simple and generated by humans in a way that computers can't yet do.

It's like using advanced techniques to prove that all even numbers from 10^100 onwards are the sum of two primes, then using computers to check everything up to 10^100, and thus claiming a proof of the Goldbach conjecture. The difficult bit was creating the proof. The easy bit was getting the computer to check that the cases worked.

It's not a proof by computer, despite what you've heard.