From owner-qed Mon Nov 14 10:37:56 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA29071 for qed-out; Mon, 14 Nov 1994 10:36:53 -0600
Received: from head.cs.wisc.edu (head.cs.wisc.edu [128.105.9.41]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA29066 for <qed@mcs.anl.gov>; Mon, 14 Nov 1994 10:36:48 -0600
Date: Mon, 14 Nov 94 10:36:46 -0600
From: kunen@cs.wisc.edu (Ken Kunen)
Message-Id: <9411141636.AA26476@head.cs.wisc.edu>
Received: by head.cs.wisc.edu; Mon, 14 Nov 94 10:36:46 -0600
To: qed@mcs.anl.gov
Subject: The Fermat-Wiles Theorem
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


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