left up

The Future

Only with more practical experience, ENOD51 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.


left right up home John Harrison 96/8/13; HTML by 96/8/16