Re: Incentive to write proofs

guttman@linus.mitre.org
Message-id: <9304250202.AA09730@circe.mitre.org>
To: QED <qed@mcs.anl.gov>
Subject: Re: Incentive to write proofs 
In-reply-to: Your message of "Sat, 24 Apr 93 16:06:06 BST."
             <"swan.cl.cam.:223760:930424150614"@cl.cam.ac.uk> 
X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Date: Sat, 24 Apr 93 22:02:50 -0400
From: guttman@linus.mitre.org
Sender: qed-owner
Precedence: bulk

I like John Harrison's point about the educational value of proofs a
lot.   

> Speaking from personal experience, I think there is great
> *educational* value in doing proofs in a form acceptable to a computer
> theorem prover... 

I think that (when we manage to do it right) one of the biggest
pay-offs of computerized proofs will be to help students to get a
deeper understanding of mathematics.  I don't mean a deeper
understanding of logic and of foundations, but of ordinary
mathematics.  

Experience working with a good computer-based proof system will teach
which theorems are needed as lemmas for which others; it will teach
what role the lemmas really play in the proofs; and it will teach
which kinds of manipulations (computations) are valid in which kinds
of structures.

Not many students currently get a grasp at this level.  But I think it
will be easier to learn with a computerized mathematical laboratory.
Because then you can experiment and see what kinds of reasoning are
successful and where you find insurmountable gaps.

That's what I'd like to see come out of a qed-like enterprise.  The
foundational content of qed seems to me less important.  I even think
that as the quality of the computerized mathematical laboratory
gradually increases, that it will also provide a practical advantage
for the professional mathematician.

I think I disagree with John though when he says:  

> I think it is definitely the choice of logical basis that will be most
> problematic. 

Maybe he mean problematic in the sense of empirically difficult to get
people to agree, and if that's it then maybe he's right.  But if he
means that it's hard to choose the right one and disastrous to choose
the wrong one, then I disagree.  

I think that we know many logics that are expressive, and easy to
reason with, and well-understood.  I think we'll be much better off if
we settle in with one (or a few, arranged in Konrad's ring network
design, but please, not too many), and start figuring out how to carry
out interesting pieces of mathematics.

	Josh