0. Computers influence mathematics in many ways. This paper is devoted to one of these influences: the fact that we can explain mathematics to a computer. In this process we may learn about how to organize mathematics and how to teach some of its aspects.

At the Technological University Eindhoven (Eindhoven, the Netherlands) the project Automath was developed from 1967 onwards, with various kinds of activities at the interfaces of logic, mathematics, computer science, language and mathematical education. Right from the start, it was directed towards the presentation of formalized knowledge to a computer, in a very general language, with quite a strong emphasis on doing things the way humans do. One might say that the project is a modern version of “Leibniz's dream” of making a language for all scientific discussion in such a way that all reasoning can be represented by a kind of algebraic manipulation.

The basic idea of Automath is that the human being presents any kind of discourse, however long it may be, to a machine, and that the machine convinces itself that everything is sound. All this is intended to be effectively carried out on a large scale, and not just “in principle”.

This paper does not intend to describe the Automath system in any detail, but rather to explain a number of goals, achievements and characteristics that may have a bearing on the subject of the ICMI discussion on the influence of computers and informatics on mathematics and its teaching.