formal proof and ordinary mathematics (fwd)

[piotr@cs.ualberta.ca]

Hi:

I think we could help Donald.

If you have any info please forward it to me and I will prepare
a summary unless someone else wants to do this.

It is the right time to summarize whatever ommisions were found
in CCL and there is this erroneous construction of real numbers in one
of the (Birkhoff's ?) books.

PR


Forwarded message:
> From DMACKENZ@afb1.ssc.ed.ac.uk Tue Oct  6 09:11:56 1998
> From:	<DMACKENZ@afb1.ssc.ed.ac.uk>
> Organization:  Edinburgh University
> To:	piotr@cs.ualberta.ca, romat@mizar.org
> Date:	Tue, 6 Oct 1998 16:11:25 +0000
> Subject:       formal proof and ordinary mathematics
> Reply-to: D.MacKenzie@ed.ac.uk
> Priority: normal
> X-mailer: Pegasus Mail/Mac (v2.2.1)
> Message-ID: <BA466D27CC3@afb1.ssc.ed.ac.uk>
> X-Orcpt: rfc822;piotr@cs.ualberta.ca
> 
> Bob Boyer suggested I get in touch with you because he thought you might 
> be able to give me a professional guestimate of the probability of error 
> in articles in mathematical journals like the Proceedings of the AMS. 
> I'm writing a history of the automation of mathematical proof, and was 
> struck by the absence of cases where formal, mathematical proof reveals 
> serious errors in ordinary mathematics. I'm wondering how much that is 
> the result of Bob and his colleagues formalizing not "raw" journal 
> mathematics but results which dozens of people have scrutinized and 
> refined. 
> 
> Best regards,
> 
> Donald MacKenzie
> 
> From:          Self <DMACKENZ>
> To:            Boyer
> Subject:       formal proof and ordinary mathematics
> Reply-to:      D.MacKenzie@ed.ac.uk
> Date:          Tue, 6 Oct 1998 11:42:36
> 
> 
> Bill McCune suggested that I get in touch with you. I'm writing a book 
> on the history of formal, automated proof.
> 
> Can I trouble you with a question I will deal with 
> in the conclusion of the book? It has to do with the relation between 
> formal proof and less formal arguments such as ordinary informal 
> mathematical proofs. It is clear that, within computer science, formal 
> proof often shows "theorems" to be incorrect (i.e. shows designs have 
> errors) and there are cases I can point to of formal proof showing 
> journal-level proofs to be wrong (e.g. Rushby and von Henke on the clock 
> convergence algorithm).
> 
> My question is this. Are there analogous cases to be cited where formal 
> proof has shown "theorems" within * mathematics *  ( rather than 
> computer science) to be wrong, or has found errors in ordinary 
> journal-level mathematical proofs? In my reading of the literature, what 
> I've found little of this, but I may simply not have read fully enough.
> 
> I'm sure that if anyone has found errors in ordinary mathematics by 
> using formal, mechanical proof, it will be the Mizar group, so I hoped 
> you 
> might be able to give me a quick reply to the question.
> 
> Best regards,
> 
> Donald
> 
> *********************
> Donald MacKenzie
> Department of Sociology
> University of Edinburgh
> 18 Buccleuch Place
> Edinburgh EH8 9LN
> Scotland
> tel: 44 131 650 3980 or 650 4001;  fax: 44 131 650 3989
> *********************
> 
> 
> *********************
> Donald MacKenzie
> Department of Sociology
> University of Edinburgh
> 18 Buccleuch Place
> Edinburgh EH8 9LN
> Scotland
> tel: 44 131 650 3980 or 650 4001;  fax: 44 131 650 3989
> *********************
> 


-- 
Piotr Rudnicki