I guess I'm a bit puzzled that some people reject computer proofs. I think they're just complicated calculations, and should be subjected to the same tests as other long calculations: Double checking, the code available for review, sometimes programmed twice by independent teams, etc. This is the same process as the Mersenne folks use, and it seems a reasonable approach. The chance of some sort of error is small but nonzero, but that's also true for long human proofs. The number of people who've checked every detail of the classification of simple groups must be tiny. I've personally checked that M13 = 8191 and M17 = 131071 are prime, and I could do M31 if pressed. But for M11213, I depend on the machine. Similarly, when I claim that 2^(1/5) generates a Euclidean number field, my proof depends on a computer check of 100,000 boxes. This in turn depends on my program, the Lisp interpreter, the editor, the bignum package, the particular machine not having hiccuped, etc. If the result is important enough, someone will do an independent check. --- There's a considerable body of machine verified proofs, from the basic axioms, of some pretty complex results: The Prime Number Theorem has been done. The Kepler Group might be able to use some of this material for a start. The issue of the reviewers giving up could be the subject of another long message. We need a way to give reviewers some credit for a thankless job. Rich rcs@cs.arizona.edu