I agree that the vast majority of math is built on firm foundations, as is the vast majority of most other fields. However, as is sometimes the case, a correct result may have an incorrect proof, so the proof of the pudding may not always be in the eating :-). While there are certainly problems for which the proof is as long as the search for the proof, there currently (at least until P=NP) appear to be problems for which the proof is considerably shorter than the search tree. Re Mersenne Primes, Rich would know better than me whether there exist shorter proofs of primehood for these particular primes than the program which find them. Vaughan Pratt showed a while ago that all primes have a relatively succinct proof, but finding that proof requires (as I recall) the factorization of p-1 & lots of other factorizations. Proving a number composite is (currently) very cheap compared with finding the factors in the first place. At 06:43 PM 3/2/2006, Schroeppel, Richard wrote:

An extreme endpoint of checking is verifying a Mersenne Prime, where you pretty much have to repeat the LL test. But of course they do that anyway.

A checkable proof of the Odd Order Theorem could be very useful, since it would likely result in the discovery and repair of some minor errors.

But it seems unlikely that much of our edifice is built on wrong stuff, so making checks required seems extreme. And it could chase the non-detail-oriented out of the profession. (Or perhaps they'd make their grad students do it. Hmmm. Would the 8th Amendment apply?)