From owner-qed Sun Nov 13 23:09:45 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id XAA23765 for qed-out; Sun, 13 Nov 1994 23:06:40 -0600 Received: from earth.anu.edu.au (earth.anu.edu.au [150.203.20.5]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id XAA23754 for ; Sun, 13 Nov 1994 23:06:21 -0600 Received: by earth.anu.edu.au id AA01056 (5.67b/IDA-1.5 for qed@mcs.anl.gov); Mon, 14 Nov 1994 16:06:45 +1100 Received: from Messages.8.5.N.CUILIB.3.45.SNAP.NOT.LINKED.earth.sun4.51 via MS.5.6.earth.sun4_51; Mon, 14 Nov 1994 16:06:44 +1100 (EST) Message-Id: <0ilj1Y2KmlE503lp00@earth> Date: Mon, 14 Nov 1994 16:06:44 +1100 (EST) From: Zdzislaw Meglicki To: qed@mcs.anl.gov Subject: Wiles' proof of the Fermat Theorem Cc: "John K. Slaney" Sender: owner-qed@mcs.anl.gov Precedence: bulk In the last issue of the New Scientist, I've found a brief note that Andrew Wiles has fixed the problem in his proof of the last Fermat Theorem, which should really be renamed to "Fermat-Wiles" theorem, if the proof is correct. Chatting about it with John Slaney, we came to the conclusion that the verification of that proof would be an ideal Holy Grail for QED. In other words, if you could use the QED system in order to verify a proof as complex and convoluted as Wiles' proof, you'd demonstrate to all mathematicians enormous usefulness of such a system. Greetings to all, Zdzislaw Meglicki, Zdzislaw.Meglicki@cisr.anu.edu.au, Parallel Computing Research Facility, CISR && Plasma Theory Group, RSPhysSE The Australian National University, Canberra, A.C.T., 0200, Australia, fax: +61-6-249-0747, tel: +61-6-249-0158