One such result was that certain problems are undecidable, which means that any automated approach would be prone to become "stuck" and never terminate.
Another results showed that the complexity of general automated proof generation is exponential in nature.
Both these results mean, that it's impossible to tell whether a computation just takes a very long time (say years) or whether the problem is indeed undecidable (in which case the program would never halt.)
A human on the hand, is very well capable of solving the Halting Problem and can discern whether a problem is undecidable [1].
This is of course a corner case, but it goes to show that there are indeed limits to automated theorem proving.
A human would therefore - in principle - always need to proof that a problem is decidable in the first place before passing it to an ATP.
[1] https://en.wikipedia.org/wiki/List_of_undecidable_problems