Only with more practical experience, ENOD⁴⁰ 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 (even algebraic subjects often include commuting diagrams!) 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 to draw together the world's theorem proving communities in a 'QED Project' [anonymous-qed] to formalize all mathematics has been proposed. 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 grandiose 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/2/22; HTML by 96/4/5