The Fermat-Wiles Theorem

Ken Kunen (
Mon, 14 Nov 94 10:36:46 -0600

Regarding Lyle Burkhead's comment:

>> But if you spend 20 years and millions of dollars to verify something
>> that is already known to be true, in what sense are you "demonstrating
>> the enormous usefulness of such a system"?

It seems to me that the long-range goal is not to verify one
specific theorem, but rather to construct a tool which
mathematicians in the future can use as a referee. This tool
should be 100% reliable (unlike human referees), and
easy and painless to use (unlike current verification systems).

I think that verifications (even if not painless) of individual hard
theorems are of interest primarily because they tend to indicate that this
long-range goal is attainable, eventually.

Ken Kunen