Don't forget the kicker: the original computer-powered proof turned out to to have several serious flaws, brought to light after work done by several researchers unconnected to the original effort. ctrl-f for Schmidt.

As the Wikipedia article states, the main countermeasure to non-surveyability is to express the proof in formal logic, which can then be verified by an automated proof checker. In fact, this is exactly what the authors of the proof of Keller's conjecture have done. And likewise, the Four Colour Theorem has been verified in this way.

I don't think non-surveyability is really the issue here.

Non-surveyability was introduced precisely as a criticism of the 1976 proof. I believe that the four color theorem was proven with the help of an automated proof checker only in 2005.