In some sense, proof-checking is a trivial linear-time operation: you check that each step follows from the last, and if they all do, the proof is correct. Proof checking is something that computers do well, except that describing a proof to a computer is usually non-trivial.

Where proof-checkers -- human and otherwise -- will get hung up, especially with the new maths, is that it may not be obvious how each step follows from the last.

What will happen is something a bit interactive: if the proof checker cannot intuitively see the logic in one step of the proof, he may first try to prove the lemma himself. If he can't, he'll go back to the original author of the proof and say, "Hey, I don't see how you go from step 518 to step 519. Can you prove it?" Sometimes the author easily can; he just didn't elaborate on that step in the proof because it was so obvious to him. Sometimes he can't; either in trying to prove that lemma he finds a contradiction, in which case the proof is incorrect, or maybe he just can't prove it, and the proof is ... incomplete.

It's this last situation which causes these grand proofs to drag out for so many years. At some point in the 500 pages, there is a jump which the author didn't notice, and it takes him another few years to prove that jump. The checkers have a much easier job, because they just have to try to follow the logic; if they fail, the burden is on the author to make the point at which they stick more clear.