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.