In Robert Stoll's "Set Theory and Logic", there is the following passage on effectiveness of theorems (p. 375) :
Mathematical logicians have shown that for many interesting axiomatic theories the notion of theorem is not effective. We emphasize that this means the nonexistence of effective procedures for "theoremhood" has been proved for some theories and not merely the nondiscovery to date of effective procedures. It follows that human inventiveness and ingenuity is necessary in mathematics.
This seems to imply that human inventiveness/ingenuity can accomplish something which can not be accomplished by a machine, due to the impossibility of an effective procedure for deciding "theoremhood".
However, if for a certain theory, a human could decide whether any given sentence is a theorem, then he/she should be able to provide a formal demonstration of that claim (otherwise the claim would have little value). Such a demonstration could take two forms :
If the sentence is a theorem, the demonstration would simply be its proof. But if such proof exists, a machine can easily accomplish the same, simply by recursively enumerating all possible proofs of the theory.
If the sentence is in fact not a theorem, the demonstration would have to be expressed as a proof $P_M$ in some metalanguage - with supposedly a richer set of axioms, if formalized, than the subject theory at hand - which would allow it to show that no proof $P_S$ in the subject theory exists for the theorem. But by the same argument as in 1, if this metalanguage and its axioms are formalized, a machine can find $P_M$ by enumerating all the possible proofs in this richer language.
So, in all cases a machine accomplishes whatever a human is able to accomplish. What then is the advantage of human inventiveness/ingenuity?