> An automatic theorem prover is a kind of AI. Gödel showed its limitations.

Which of those limitations apply only to AI and not to human intelligence and mathematical reasoning?

Is it somehow surprising that AI can't prove mathematical contradictions to be true?