The four color theorem is one of the least satisfying proofs I have ever seen, and I've gone through thousands by hand. It's because the final stage is reduced

The four color theorem is one of the least satisfying proofs I have ever seen, and I've gone through thousands by hand. It's because the final stage is reduced to computer verification...it's unsatisfying.