Delivery-Date: 
From: dam@ai.mit.edu (David McAllester)
Date: Thu, 22 Apr 93 10:47:26 EDT
Message-Id: <9304221447.AA01531@spock>
To: mumford@math.harvard.edu
Cc: qed@mcs.anl.gov, beeson@cats.ucsc.edu
In-Reply-To: david mumford's message of Wed, 21 Apr 93 16:04:58 EDT <9304212004.AA05327@math.harvard.edu>
Subject: Why should a mathematician be interested in QED?
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


What QED should strive for, I think, is a low cost way of reducing the
proofs of working mathematicians to complete formal rigor.  One
benefit is increased confidence.  Ultimately, the QED project could
also be used as a library in ways that current libraries can not.  For
example, a mathematician could enter a definition and ask if this
concept has been studied before.  If the system can "understand" the
definition, then it might be able to find appropriate references, or
even answer questions based on its preexisting knowledge of the
concept.

It seems to me that benefits for working mathematicians are not
achievable with current technology.  With current systems a formally
verified proof is probably an order of magnitude more work than a
proof published without machine verification.  I am quite confident
that this situation will change over time.  More and more of the
formal details in proofs are being filled in automaticaly by existing
verification systems.  I also think that one of the best ways to make
progress is to start the QED project.  I suspect that in the beginning
the primary participants will be computer scientists interested in
imporving the usefulness of the system.  The first mathematicians to
use it for their publishable mathematics will probably be some of
those same computer scientists.

	David