[mikedodds]

I don't know if there are proofs unsuited to human minds, but for machine proofs, there's no essential difference between what a proof assistant like Coq can do, and what a human brain can do. Ultimately Coq boils down to a very simple core logic that could (in principle) be checked by a human. But the sheer scale of such proofs means they can't be meticulously checked. Proof tools are just the same as e.g. compilers - they can do things humans can't do because to do so would be so incredibly time consuming and tedious.