We want to avoid making systems which are difficult for mathematicians to use. This means we should try to keep the interface close to the familiar style of mathematics books. Perhaps even small changes in notation (e.g. '&' instead of '') could help a lot. Alternative styles of expression should be permitted ('for real x', 'for any x R' or 'for any real number x') and perhaps even a few redundant 'noise words'. For example, Mizar allows the word 'that' (e.g. 'suppose X' or 'suppose that X') but essentially ignores it. It should be possible to provide a degree of tailoring to suit individual tastes.³⁷ However we must avoid the error of making the interface too flexible and intelligent, for two reasons:

1. If there is an additional complicated layer of interpretation between the user and the underlying logic engine, then we are bringing back all the potential for vagueness and ambiguity that we are trying to banish. It will require substantial work for a new user to understand the relationship between what is seen at the user level and what exists inside the machine.

2. Making an intelligent flexible interface is probably just too hard; we're getting embroiled in a difficult AI project. The success of the Unix environment is partly because it is formal, simple, flexible, and makes no attempt to be clever! Anyway, opinions and fashions about what is best change quickly; remember the light pens in 60s visions of future computers.

It is not necessary to use a full-blown logical symbolism; one can quite well have stylized constructs of ordinary English. Mizar, for example, does not use special symbols for quantifiers and connectives. This is largely a matter of taste. Some writers like Halmos oppose the use of logical symbolism, but as far as we can see this is just a matter of personal taste, and no more in need of justification than the use of symbols for arithmetic operations. Current systems certainly leave a lot to be desired in the matter of user interaction. HOL tactic scripts are an arcane mix of higher order functions; some systems like IMPS, NQTHM and ONTIC use LISP syntax, which is even further from conventional notation. Mizar's proof scripts are undoubtedly the closest to familiar mathematical notation. This was after all one of the goals of the Mizar project; perhaps the developers were also less corrupted by the tendency to ready acceptance of machine-oriented syntax which tends to arise among computer scientists.

Even though the system itself may still be reasonably formal, there is plenty of potential for translating automatically or semi-automatically into something readable by any mathematician. Mizar's journal 'Formalized Mathematics' points the way here. The translation is by no means sophisticated, but works quite well (admittedly it is only the statements of theorems, not their proofs, at present). In line with the above remarks on alternative modes of expression, sometimes different alternatives are chosen using a random number generator, to give something like the 'elegant variation' discussed by [fowler]. ('Now we prove', 'The following hold', 'The following propositions are true', ...)

It's much easier to translate from a formal language to (possibly stilted and artificial but correct) natural language than vice versa. So mathematics expressed in a formal way is a valuable resource: it could be automatically translated into many different languages, avoiding some of the difficulties of communication among the world's mathematicians (most of whom are now forced to use English; a few decades ago German or French). It may even be that the formal language would itself become an accepted interlingua³⁸ for mathematical texts; though it would be rather spartan and colourless, the success of international chess publications like \uSakovski Informator, which are languageless, is worth noting.³⁹

Rendering proofs in HTML or using another hypertext format, to allow users to examine proofs at different levels of details, is a topic which has already attracted some attention. Conversely, one could imagine, in education, having different levels of automated theorem proving. Just as now, students are supposed to master arithmetic before being given calculators, it might be thought desirable for them to master constructing formal proofs before being given computer assistance. (To some extent, this depends on whether one is trying to teach logic or mathematics.) Several systems have already been used in education, notably Mizar, with interesting results as recounted by [szczerba-mizar]:

There occurred a substantial change in my role as a teacher. Earlier, when assigning homework tests, I was treated as an enemy who has to be forced to accept the solution, sometimes in not an exactly honest way. Now the enemy to be defeated was the computer and I was turned into an ally helping to fight this horrible device. This small fact has seriously influenced my contacts with the students. They were much more eager to approach me with their problems, to report on their difficulties, and ask for help.

John Harrison 96/2/22; HTML by 96/4/5