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).
This is an issue that has already come up to some extent. The initial proof of the Robbins conjecture used automated proving systems for a large amount of it, and they made no intuitive sense. It took about 2 years for someone to grok the proof well enough to present a version that made sense to people.
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.
Hm, I thought it was already obvious what to do in the second scenario, and the only challenge was getting from the first to the second. See my reply to Nesov.
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).
This is an issue that has already come up to some extent. The initial proof of the Robbins conjecture used automated proving systems for a large amount of it, and they made no intuitive sense. It took about 2 years for someone to grok the proof well enough to present a version that made sense to people.
Hm, I thought it was already obvious what to do in the second scenario, and the only challenge was getting from the first to the second. See my reply to Nesov.