Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Dec 1993 15:30:37 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26465; Thu, 9 Dec 1993 08:17:12 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26461; Thu, 9 Dec 1993 08:17:02 -0700 Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA02949; Thu, 9 Dec 1993 07:13:43 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Thu, 9 Dec 1993 14:48:03 GMT From: David Shepherd Message-Id: <23328.9312091447@frogland.inmos.co.uk> Subject: Fermat's theorem To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Thu, 9 Dec 1993 14:47:11 +0000 (GMT) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 829 In case anyone was inspired by the recent proof that |- ! x y z. ((x EXP 4) = (y EXP 4) + (z EXP 4)) ==> (y=0) \/ (z=0) and are trying to formalise the recent proof for the general case |- ! n. (2 < n) ==> ! x y z. ((x EXP n) = (y EXP n) + (z EXP n)) ==> (y=0) \/ (z=0) then you may be interested in a small article in today's Telegraph which says that the person who presented his proof last summer has now admitted that on reflection there turn out to be some problems with his proof! -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "you might think that --- I couldn't possibly comment"