TeethWhitener said:
Essentially, the detractors claimed that a computer can never prove a statement because we have no way of knowing in general with absolute confidence that the computer didn't go wrong (i.e., behaved in a way contrary to what we expected). Of course, this problem extends to the fact that our brains (the classic theorem proving tool) are also physical objects, which has led into discussion in the philosophy of mathematics about what exactly a proof is.
IMO a proof is an exercise in persuasion. There is a definite element of psychology and (dare I say it) marketing. I'm not being critical, the proof acceptance process is pragmatic, a system to make best use of finite resources.
About twenty years ago there was a movement toward automated verification of proofs. It was abruptly abandoned. I think automated proof is a worthy goal, but beyond what can be done at this time. I guess what they discovered is that it was far too much work to prove anything to a computer. If proving to a computer were a requirement, all mathematical progress would halt. First it would be necessary to enter all the basic proofs, a Herculean and entirely impractical effort. So the current methods of proof must suffice until artificial intelligence technology improves.
Kurt Godel proved that there is no limit to the minimum length of a proof. Starting with a simple proof it is possible to construct a proposition with a proof that must be longer than the first, and so on. So it is practically impossible to prove certain things.
There is a proposed proof of the abc conjecture. The claimant has excellent credentials and reputation. But the proof is so long and complicated that no movement has arisen to verify the alleged proof. If no group will make the effort then we may never know whether or not this is a proof. If a computer ever verifies a proof like that, or a proof with that complexity raised to a power of one thousand, then humans would have no other criteria than trust or lack thereof.
I think that quite often the proposition to be proved is of little importance. What really matters is the discovery of a fresh approach or insight in the course of the proof. It would seem to me that a proof of the Goldbach conjecture that occupies a centillion terabytes would be utterly useless.
There was the controversial computerized proof of the 4-color conjecture. It was useful in the sense that mathematicians (and cranks) could then stop wasting their time on attempted proofs. An expert (Gerhard Ringel) told me that he felt there was no other way to prove it, so good riddance. But it could very well be in some cases that an impenetrable computerized proof would discourage the discovery of a simple, worthwhile proof. In that case the computerized proof would serve the function of inhibiting progress. But probably not. I bet there are a thousand cranks right now trying to come up with a one-page proof of Fermat's last theorem.
IMO automated and natural methods of proof verification are complementary. It would be nice to have both. What's the problem?