From owner-qed Thu May 12 05:05:18 1994 Received: from ANLVM.CTD.ANL.GOV (anlvm.ctd.anl.gov [146.137.96.2]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id FAA24382 for ; Thu, 12 May 1994 05:01:42 -0500 Message-Id: <199405121001.FAA24382@antares.mcs.anl.gov> Received: from ANLVM by ANLVM.CTD.ANL.GOV (IBM VM SMTP R1.2.2ANL-MX) with BSMTP id 8984; Thu, 12 May 94 05:01:39 CDT Received: from PLBIAL11 by ANLVM (Mailer R2.07B) with BSMTP id 3845; Thu, 12 May 94 05:01:39 CDT Received: from PLBIAL11 (TRYBULEC) by PLBIAL11 (Mailer R2.07) with BSMTP id 2939; Thu, 12 May 94 11:51:53 CET Date: Thu, 12 May 94 11:36:15 CET From: Andrzej Trybulec Subject: Rusty Lusks question To: QED No, I do not believe that everything has been said. On the contrary, I do believe that we did not start as yet. I discussed QED Manifesto many times here with students and staff. The reaction to reasons to do QED is quite favorable, not so to objections and the remainig part. For instance Objection No 1, Controversies in mathematics. It seems that the common answer is: "these are controversies in the Philosophy of Mathematics, who cares ?". I do not claim that I share this opinion. The problem is that mathematicians believe that there are no doubts what it means that a proof is correct and that there is a huge koine that they use (much more than ZFC). And I believe that if we failed to get mathematicians involved, we would fail the QED project as well.And to get mathematicians involved, we have to find out how to talk to them. I meanregular mathematicians that use computer mostly for TeX. Regards Andrzej Trybulec