I assume that he was going for something different, though; namely, that it's nuts that verifying proofs is simpler for humans than it is for machines.
Well, if the proof is first formalized, it's easier for machines to verify. But formalizing it is much harder. This is similar to the situation in software, where uptake of formal-verification tools that can prove correctness of programs is relatively low (though Agda is making some very interesting progress).