Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sun, 25 Apr 1993 20:20:19 +0100
Received: by antares.mcs.anl.gov id AA07042 (5.65c/IDA-1.4.4 for qed-outgoing);
          Sun, 25 Apr 1993 14:07:08 -0500
Received: from Maui.CS.UCLA.EDU by antares.mcs.anl.gov with SMTP 
          id AA07035 (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>);
          Sun, 25 Apr 1993 14:07:05 -0500
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA08125;
          Sun, 25 Apr 93 12:07:02 -0700
Message-Id: <9304251907.AA08125@maui.cs.ucla.edu>
To: qed@mcs.anl.gov
Subject: Re: Incentive to write proofs
Date: Sun, 25 Apr 93 12:06:58 PDT
From: chou@CS.UCLA.EDU
Sender: qed-owner@mcs.anl.gov
Precedence: bulk

I guess everyone who's done machine-assisted theorem proving would
agree with John Harrison and Josh Guttman on its educational value.
But, is there any funding agency which is willing to fund such a
grand proposal as QED just because of its "educational value"?

- Ching Tsun