**Mail folder:**QED**Next message:**jt@linus.mitre.org: "Boyer's hypothesis"**Previous message:**mthayer@BIX.com: "Other considerations"**In-reply-to:**John Harrison: "Incentive to write proofs"**Reply:**chou@CS.UCLA.EDU: "Re: Incentive to write proofs "

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