left up

User interaction

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 'and') could help a lot. Alternative styles of expression should be permitted ('for real x', 'for any x memberof 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:

  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. 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 interlingua49 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 x3 + 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.

left right up home John Harrison 96/8/13; HTML by 96/8/16