QED-like Efforts

• Mail folder: QED
• Next message: jt@linus.mitre.org: "Re: From idea to project "
• Previous message: Randall Holmes: "Context"

Date: Fri, 6 Aug 93 13:22:46 CDT
From: Robert S. Boyer <boyer@CLI.COM>
Message-id: <9308061822.AA01372@dilbert.CLI.COM>
To: holmes@diamond.idbsu.edu
Cc: qed@mcs.anl.gov
Subject: QED-like Efforts
Reply-To: boyer@CLI.COM
Sender: qed-owner

   I'm having some difficulty figuring out why you are discussing as
   hypothetical things which already exist and have existed for some
   time!

Indeed, there have been a good number of QED-like efforts spread over
at least the last 27 years, both large scale and small.  (I hear
rumors that the Polish MIZAR effort may be the largest so far.)  But
one can ask the question whether any of the efforts now underway has
sufficient support to achieve coverage of the most commonly used sorts
of mathematics.  I would guess that despite at least 27 years of such
projects, what has been proof-checked so far is an insignificant
percentage (maybe 5%, if I may be permitted to take a blind, naive
shot in the dark, could be less than 1%) of what a typical math
graduate student must learn to pass qualifying exams.  I fear that QED
faces more difficult organizational problems (personal, national,
political, social, economic, etc.) than technical problems.  We not
only have *some* proof checking systems, we may have a Babel's worth
of them.  I doubt whether this plethora of really wonderful
alternative proof-checking systems is appealing to the various funding
agencies or to potential users.  People seemed to tire of inventing
new programming languages sometime around 1980 or so.  Maybe some day
the C and FORTRAN of proof checking systems will become clear.  (That
was a joke.)

Bob