From owner-qed Mon Nov 14 13:11:03 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA01396 for qed-out; Mon, 14 Nov 1994 13:10:06 -0600 Received: from scapa.cs.ualberta.ca (root@scapa.cs.ualberta.ca [129.128.4.44]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id NAA01389 for ; Mon, 14 Nov 1994 13:10:00 -0600 Received: from sedalia.cs.ualberta.ca by scapa.cs.ualberta.ca id <18502-1>; Mon, 14 Nov 1994 12:09:37 -0700 Subject: Re: The Fermat-Wiles Theorem From: Piotr Rudnicki To: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Mon, 14 Nov 1994 12:09:33 -0700 (MST) Cc: qed@mcs.anl.gov In-Reply-To: <199411141655.JAA06851@chelm.nmt.edu> from "Victor Yodaiken" at Nov 14, 94 09:55:11 am X-Mailer: ELM [version 2.4 PL23] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 689 Message-Id: <94Nov14.120937-0700_(mst).18502-1@scapa.cs.ualberta.ca> Sender: owner-qed@mcs.anl.gov Precedence: bulk > > On Nov 14, 10:36am, Ken Kunen wrote: > Subject: The Fermat-Wiles Theorem > > This appears to be a case of the contagious C.S. disease first > exhibited by Babbage who applied for a grant for the > more ambitious project after the modest project failed. > When we can verify the theorems in Graham/Knuth/Pashniak > or those in, say, an introductory calc or graph theory > book, it might be reasonable to speak of Wiles theorem. > How about a qed for highschool mathematics? Which of the existing proof-checking/finding systems makes doing highschool mathematics painless? I am afraid that even if such a system existed, it would not make it to NYT. -- Piotr (Peter) Rudnicki