there is a 125-page attempt at the Poincare' conjecture. Try it. If these "provers" find heretofore unobserved flaws, THEN I'll concede that they would be useful tools in mathematics--in uncovering flaws. But they _still_ don't "prove" that these theorems are correct. They only convince themselves. But convincing me that I should believe them involves convincing me that there has been no failure in the program--at any of the levels I've previously discussed. And, by the way, this is why the general mathematical community is still suspicious of the 4-color theorem. In fact, the orginal "proof" contained a number of flaws. All discovered were all easily patched, but the fact that they existed in the first place means that we have no reason to believe that something subtle is yet to be discovered.
All you need to do is verify yourself (i.e. formally prove the correctness of the theorem prover) to rely on the results of the theorem prover. It's the web of trust model. And before you jump up and say "but how can you prove the theorem prover, maybe Godel...", there is a very simple theorem prover that is provable via mathematical induction. If you don't trust induction, then I don't know what to tell you. (it's like denying the Peano postulates) The theorem prover works like this: Start off with your axiom set and your rules of production. (for instance, a context free grammar, that might say "if x+y=z is a theorem, then x+(y+1)=z+1 is a theorem") And enumerate all possible theorems on the parse tree. If you reach theorems of length N that exceed the theorem you're trying to prove than either it is a nontheorem or undecidable. This procedure will never produce a "yes" answer for a false theorem, although it will fail to prove some theorems. And it is news to me that "the general mathematical community is still suspicious of the four color theorem." Not only are they not suspicous of the theorem, they aren't suspicious of the proof. It's been verified and reproduced over and over again, and it has also been shortened down from the original (I believe 2000+ special graph cases) to just over 400. Physicists aren't suspicuous of relativity either. [note above: the theorem prover fails if the production rules allow theorem shortening. The system must be primitive recusive, but there are many restricted domains of theorem proving which are.] The classification of the simple groups was a 1000+ page written proof. Which one is would you trust to have a mistake somewhere? The computer checked one, or the human checked one? This general line of discussion is getting out of hand. You can't *prove* anything for sure. Even if it seems logical to you, how do you know your own mind isn't buggy? How do you know you're not hallucinating? Even something as simple as Euclids proof of the infinitude of primes. You think it's been proved? ha! You are merely delusional. The rest of us sane people saw the disproof years ago, but every time you start to read the disproof, your mind goes into its own little universe and starts substituting in screen memories making you *think* you just read a proof, not a disproof. Ultimately, you can't even trust yourself. The world is a risky place, and sometimes you just have to live with the fact that one day, something you chose to place faith in and rely on is going to be pulled from underneath you. -Ray