From lusk Fri May 13 10:22:31 1994
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA03552 for <qed@mcs.anl.gov>; Fri, 13 May 1994 10:19:38 -0500
Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1)
	id AA08516; Fri, 13 May 94 10:19:05 CDT
From: boyer@cli.com (Robert S. Boyer)
Received: by rita (4.1) id AA16079; Fri, 13 May 94 10:19:04 CDT
Date: Fri, 13 May 94 10:19:04 CDT
Message-Id: <9405131519.AA16079@rita>
To: qed@mcs.anl.gov
Subject: More Motivations

It has been suggestied that the following motivations be added to the
QED manifesto:

   6.  The `noise level' of published mathematics is too high.  It has
   been estimated that something between 50 and 100 thousand
   mathematical papers are published per year.  Nobody knows for sure
   how many contain errors or how many are repetitions, but some
   pessimists claim the number of both is high.  QED can help to
   reduce the level of noise, both by helping to find errors and by
   helping to support computer searches for duplication.

   7.  QED can help to make mathematics more coherent.  There are
   similar techniques used in various fields of mathematics, a fact
   that category theory has exploited very well.  It is quite natural
   for formalizers to generalize definitions and propositions because
   it can make their work much easier.

   8.  By its insistence upon formalization, the QED project will add
   to the body of explicitly formulated mathematics.  There is
   mathematical knowledge that is neither taught in classes nor
   published in monographs.  It is below what mathematicians call
   "folklore," which is explicitly formulated.  Let us call this lower
   level of unformulated knowledge "mathlore".  In formalization
   efforts, we must formalize everything, and that includes mathlore
   lemmas.

   9.  The QED project will help improve the low level of
   self-consciousness in mathematics.  Good mathematicians understand
   trends and connections in their field.  The QED project will enable
   mathematicians to analyze, perhaps statistically, the whole
   structure of the mathematics, to discover new trends, to forecast
   developments and so on.