From owner-qed Thu Dec  8 10:42:19 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA13073 for qed-out; Thu, 8 Dec 1994 10:40:59 -0600
Received: from linus.mitre.org (linus.mitre.org [129.83.10.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id KAA13065 for <qed@mcs.anl.gov>; Thu, 8 Dec 1994 10:40:51 -0600
Received: from nausicaa.mitre.org (nausicaa.mitre.org [129.83.10.45]) by linus.mitre.org (8.6.7/RCF-6S) with ESMTP id LAA24504 for <qed@mcs.anl.gov>; Thu, 8 Dec 1994 11:40:49 -0500
From: "F. Javier Thayer" <jt@linus.mitre.org>
Received: (jt@localhost) by nausicaa.mitre.org (8.6.7/RCF-6C) id LAA16930; Thu, 8 Dec 1994 11:40:47 -0500
Date: Thu, 8 Dec 1994 11:40:47 -0500
Message-Id: <199412081640.LAA16930@nausicaa.mitre.org>
To: qed@mcs.anl.gov
Subject: disparaging remarks
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


That human beings can prove theorems is hardly remarkable.
Now if DOGS could prove theorems that would be truly remarkable.
The fact that computers can prove theorems lies somewhere in between,
I think.

F. Javier Thayer Fabrega