||The computer-support of the process of doing mathematics has significantly increased in the past few decades. And in the past few years it became clear that a next level of sophistication will be necessary and seems to be achievable that goes beyond the capabilities of current systems in a number of directions. In this thesis, we contribute to the one of such directions, the user-interfaces for such systems, i.e. we present various techniques that can contribute to making it easier and more attractive for the user of current and future mathematical software systems. The techniques that we propose in this thesis are:- the generation of natural language explanatory texts for theorem proving system,- tools for making it possible to generate spoken versions of mathematical formulae,- the technique of logicographic symbols, i.e. symbols that, at the same time, are completely formal and convey graphical intuition,- the communication of formal mathematical texts between various software systems.We implemented these various techniques in the frame of the Theorema system whose main goal is to provide a comprehensive frame for the entire process of doing mathematics.