Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Mon, 14 Nov 1994 19:18:36 +0000
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 <qed@mcs.anl.gov>; 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 <piotr@cs.ualberta.ca>
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