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 ; 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