We want to avoid making systems that 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.^{48} However we
must avoid making the interface * too* flexible and intelligent, for two
reasons:

- 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.
- 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. 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^{49} 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.^{50}

Rendering proofs in HTML or another hypertext format, to allow users to examine
proofs at different levels of details, is a topic which has already attracted
some attention *[grundy-fais]*. Conversely, one could imagine, in education,
having different levels of automated theorem proving. Just as students are now
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.

We have said little so far about computer algebra systems such as REDUCE,
Maple, Mathematica and Axiom, which seem to provide a quite acceptable style of
user interaction. These are also aids to symbolic computation, and are
unquestionably much more popular among and useful to practising mathematicians
than theorem provers are. However, despite their use of symbolic languages,
they are typically not very rigorous. For example, one is often in doubt as to
whether an expression like x^{3} + x is supposed to be a member of **R**,
**R**[x], **C**(x) or something else. Such ambiguities are often
harmless, though by the same token unpleasantly insidious, since many formal
manipulations can be done regardless. Computer algebra systems also make
mistakes, often as a result not of bugs, but conscious decisions not to worry
about precise conditions and degenerate cases (zero denominators etc.) in the
determined quest for 'simplification'.

Given the complementary strengths and weakness of computer algebra systems and
theorem provers, it is natural to attempt to combine their best features. (We
need to worry, of course, whether a greater injection of rigour in computer
algebra will merely alienate their traditional users --- the same question may
be levelled at the project of formalization in general.) Our own use of Maple
as an oracle has already been mentioned as an illustration of the separation of
finding and checking. This approach, interesting and rigorous though it is, has
its limitations given the need for checkable certificates (albeit not
necessarily simply 'answers'). Another approach, which worries less about
correctness but effectively imports the power of Mathematica's simplifier into
theorem proving, is realized in Analytica *[clarke-zhao]*. This system can
prove some remarkably complicated theorems completely automatically.