Just how sophisticated are modern automated theorem provers? Are they capable of completely proving a theorem in any reasonable amount of time, or must they be guided by humans? Moreover, how ubiquitous are computer generated proofs in mathematical journals? Is it obvious when a proof is computer generated (I’ve seen criticism of ATPs stemming from the fact that they produce rigid and inelegant proofs, is this still the case?) Do mathematicians claim computer generated proofs as their own?
How contentious is this issue in mathematical circles? I’ve read that there was a big controversy over the proving of the four colour theorem back in the 70’s as the proof was too long winded to prove by hand in a reasonable amount of time (has it been proven by hand since then?) so the prover had to be trusted completely. Is this still a bone of contention, or is ATP widely accepted now? Do the major mathematical journals accept computer generated proofs or are they for humans only?
To clarify: The four-color theorem was not proven by an automated theorem prover. An automated theorem prover takes the axioms of a formal system, and combines them in every possible way. In this manner, any theorem which can be proven will eventually be proven. Furthermore, every proof of every theorem will eventually be reached by the prover, so it’ll come up with both the clunky proofs and the elegant ones. It is in general very easy to program a computer to do this. The problem is that everything that comes out of such a machine is a theorem, but only a small fraction of those theorems are interesting theorems (and it generally takes a human to tell the difference). Further, for complicated theorems (those for which the shortest proof is long), such programs will take a very long time indeed (longer than the lifetime of the Universe) to come up with the proofs. And if the machine hasn’t proven something yet, you don’t know if that’s because there is no proof, or if the proof is just one that the machine hasn’t gotten to yet.
The four-color theorem worked a little differently. There, human mathematicians determined, using non-automated methods, that the problem could be reduced to a finite (but large) number of specific maps. In other words, they proved that if all of those maps could be four-colored, then any map at all could be four-colored. Then, they programmed a computer to try to find colorings for all of those maps. The computer did in fact find colorings for all of those maps, so combined with what the mathematicians had already proven, the four-color theorem was proven.
The prover doesn’t have to be trusted completely. If you don’t trust the original authors, you can always write your own software to verify the result yourself. The published part of a good computer-aided proof will include enough detail as to how the computation was performed to allow a mathematician with some programming skill to replicate the programs used, or if not then the original software will be made publically available so other mathematicians can pick it apart.
In the 70’s that far was a more onerous burden on a would-be reviewer than it is today, of course. But there’s really no reason for computer-aided proofs to be controversial these days. (Especially if you’re working on discrete problems like the four-colour theorem; i.e., problems with don’t require floating-point arithmetic. And even with FP arithmetic there are proven techniques for getting rigorous computer-aided results.)
As for computer-generated proofs, see Chronos’s post.
It depends on what you mean by “aided”. While I’m playing with a structure, I sometimes let Maple do some of the annoying algebra for me or to check a computational detail. Is it in any way essential to the structure of the proof? No. So, if we discount that I’d say that the vast majority of mathematics (opp. applied mathematics) is not computer-aided.
One thing that nobody seems to have pointed out: “theorem-provers” prove things that are very different from the theorems that show up in math journals. What they do is work in very specifically delineated formal systems, in which a theorem is a formal string of symbols which can be derived from a specific set of starting strings by a finite number of specific moves. Some people believe that – in principle – all mathematics can be reduced to a sufficiently complex formal system, but in practice that method is about as far as you can get from the way mathematics is really done.