Incentive to write proofs

• Mail folder: QED
• Next message: mthayer@BIX.com: "Other considerations"
• Previous message: Konrad Slind: "structure of qed"
• In-reply-to: beeson@cats.UCSC.EDU: "Re: Root Logics"
• Reply: guttman@linus.mitre.org: "Re: Incentive to write proofs "
• Reply: Zdzislaw Meglicki: "Re: Incentive to write proofs"

To: QED <qed@mcs.anl.gov>
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 <John.Harrison@cl.cam.ac.uk>
Message-id: <"swan.cl.cam.:223760:930424150614"@cl.cam.ac.uk>
Sender: qed-owner
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).