Abstract: Towards practical formalization of mathematcis

Andrzej Trybulec

In sixties the opinion that mathematics cannot be practically formalized was well established. So the main achievement of de Bruijn, among many others, is the decision that the problem must be reconsider and probably positively solved. And I believe that 1967 will be treated by future historians of mathematics as a turning point.

It is not easy to say precisely what we learnt in the meantime, if we learnt anything at all. I believe that the most important results are:

1. we need experiments with much more advanced mathematics than already done
2. a system for practical formalization of mathematics probably will not be a simple system based on small number of primitive notions
3. integration with a computer algebra systems may be necessary or at least a feasible system must have bigger computational power.

Still we should me more concerned with the original ideas of de Bruijn, the most important that eventually we have to be able to formalize new mathematical results, published in mathematical newspapers in this century.