This is also my first reaction, but it has two problems.

First, I think the best case is really just getting a much weaker machine like the one whose existence we are already positing. So maybe it can help you bridge the gap from the first scenario to the second, but I doubt it will be helpful in the second.

Second, I think its likely you would get something horribly, horribly strange out. It gives you proofs which you simply cannot comprehend, that don't even fit in the language of modern mathematics. Of course analyzing the proofs that come out is an incredibly interesting exercise, but I think I could imagine totally inscrutable 100 page formal proofs of the Riemann Hypothesis which are harder to understand than the Riemann Hypothesis is to prove directly. Human society really doesn't want proofs of hard theorems; it wants to advance human mathematics. This issue might come up if we develop some unexpectedly powerful automated theorem prover, so I guess it is interesting in its own right (and might have been discussed before).