## The Future

Only with more practical experience, ENOD^{51} in the words of *[kreisel-distractions]*, can we really decide
the best way to go. Perhaps nobody is farsighted enough to anticipate all the
problems that will arise, and we will only discover them by colliding heavily
with them. For example, there are still many questions over the formalization
of category theory, the role of types, the use of partial functions, and many
other things. We might find that some problem domains, e.g. those demanding a
lot of geometric intuition, are very hard to formalize, present new problems
and require new ideas. Accepting that geometrical insight, or even geometric
proof techniques (for the most 'algebraic' subjects often include commuting
diagrams!) are likely to be useful, the problem arises of fitting them into
existing formal calculi, or developing better calculi. The difficulty has been
noted by *[yamamoto-graphs]*:

Among many fields of mathematics and computer science, discrete mathematics is
one of the most difficult to formalize because we prove theorems using
intuitive inferences that have not been rigorously formalized yet.

Recently a proposal has been made to draw together the world's theorem proving
communities in a 'QED Project' *[anonymous-qed]* to formalize all
mathematics. Such an undertaking would demand a huge collaborative venture,
perhaps comparable to the Human Genome Project. We haven't spent so much of our
time here on advocacy, though some of the potential benefits of formalized
mathematics have been mentioned. Whatever one's opinion of these dreams, we
share the optimism of the QED proponents that formalization of mathematics is
both useful and practicable. What's more, given the disparate research
community and the wealth of experience collected piecemeal, its greater
development, for good or bad, seems to be inevitable.

John Harrison
96/8/13; HTML by 96/8/16