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 <qed@mcs.anl.gov>; 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 <Zdzislaw.Meglicki@cisr.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Wiles' proof of the Fermat Theorem
Cc: "John K. Slaney" <John.Slaney@cisr.anu.edu.au>
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