I agree that GIT limits human provers as much as it limits automated ones, but I don't agree that it's irrelevant to the issue.
A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician.
The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.
A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician.
The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.