Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants

Present day computer algebra systems (CASs) and proof assistants (PAs) are specialized programs that help humans with mathematical computations and de ductions. Although several such systems are impressive, they all have certa in limitations. In most CASs side conditions that are essential for the tru th of an equality are not formulated; moreover there are bugs. The PAs have a limited power for computing and hence also for assistance with proofs. A lmost all examples of both categories are stand alone special purpose: syst ems and therefore they cannot communicate with each other, We will argue that the present state of the art in logic is such that there is a natural formal language, independent of the special purpose applicati on in question, by which these systems can communicate mathematical stateme nts. In this way their individual power will be enhanced. Statements received at one particular location from other sites fall into t wo categories: with or without the qualification;"evidently impeccable", a notion that is methodologically precise and sound. For statements having th is quality assessment the evidence may come from the other site or from the local site itself, but in both cases it is verified locally. In cases wher e there is no evidence of impeccability one has to rely on cross checking. There is a trade-off between these two kinds of statements: for impeccabili ty one has to pay the price of obtaining less power. Some examples of communication forms are given that show how the participan ts benefit, (C) 2001 Academic Press.