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 automate

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.