One thing I haven't elaborated on here (and probably more hand-waving/philosophy than mathematics):

If Church-Turing thesis is true, there is no way for a human to prove any mathematical problem. However, does it have to follow that not every theorem has a proof?

What if every true theorem has a proof, not necessarily understandable to humans, yet somehow sound? That is, there exists a (Turing-computable) mind that can understand/verify this proof.

(Of course there is no one 'universal mind' that would understand all proofs, or this would obviously fail. And for the same reason there can be no procedure of finding such a mind/verifying one is right.)

Does the idea of not-universally-comprehensible proofs make sense? Or does it collapse in some way?