Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 24 Apr 1993 18:07:57 +0100 Received: by antares.mcs.anl.gov id AA15306 (5.65c/IDA-1.4.4 for qed-outgoing); Sat, 24 Apr 1993 10:06:22 -0500 Received: from swan.cl.cam.ac.uk by antares.mcs.anl.gov with SMTP id AA15298 (5.65c/IDA-1.4.4 for ); Sat, 24 Apr 1993 10:06:17 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 24 Apr 1993 16:06:11 +0100 To: QED Subject: Incentive to write proofs In-Reply-To: Your message of Thu, 22 Apr 93 09:24:20 -0700. <9304221624.AA12041@si.ucsc.edu> Date: Sat, 24 Apr 93 16:06:06 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:223760:930424150614"@cl.cam.ac.uk> Sender: qed-owner@mcs.anl.gov Precedence: bulk Michael Beeson writes: > From my point of view, the aim is to provide > (1) the means for practicing mathematicians to write machine-checkable > proofs > (2) the means to check those proofs once written > (3) the incentive to write such proofs. > > I think it is (3) that is most problematic. [...] Perhaps not. Speaking from personal experience, I think there is great *educational* value in doing proofs in a form acceptable to a computer theorem prover: * Since you are forced to express yourself precisely, your own thoughts are often clarified. * You appreciate the need for subtle points in proofs, which all but the most conscientious would skim over in a textbook (even supposing they appear in the textbook!) Such niggly details are particularly common in model theory and proof theory. * Since it is (and is likely to continue to be in the foreseeable future) much more laborious than doing proofs by hand, you are more inclined to husband your resources. For example, you might make a critical comparison of several available proofs before starting to type, and this is interesting and valuable. Maybe you would even think up interesting new mathematical ideas to simplify the proofs. Doubtless the educative value would be much less for a professional mathematician, but I believe many students would find it both instructive and enjoyable to do proofs by machine. You could even set competitions to get them to find the most `elegant' way of doing things. I think it is definitely the choice of logical basis that will be most problematic. Indeed, I believe a consensus is almost impossible, and in the end some cadre will have to bulldozer opposition and go its own way. John Harrison (jrh@cl.cam.ac.uk).