How Difficult is it to Prove Target Theorems?

This depends on the tasks and the initial axioms $\cal A$, of course. It is straight-forward to devise simple tasks and corresponding consistent $\cal A$ such that there are short and trivial proofs of target theorems. On the other hand, it is possible to construct set-ups where it is impossible to prove target theorems, for example, by using results of undecidability theory, e.g., [32,3,4].

The point is: usually we do not know in advance whether it is possible or not to change a given initial problem solver in a provably good way. The traditional approach is to invest human research effort into finding out. A Gödel machine, however, can do this by itself, without essential limits apart from those of computability and provability.

Note that to prove a target theorem, a proof technique does not necessarily have to compute the true expected utilities of switching and not switching--it just needs to determine which is higher. For example, it may be easy to prove that speeding up a subroutine of the proof searcher by a factor of 2 will certainly be worth the negligible (compared to lifetime $T$) time needed to execute the subroutine-changing algorithm, no matter what is the precise utility of the switch.