Re: Incentive to write proofs

chou@CS.UCLA.EDU
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
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