There has already been considerable experience of formalized mathematics in widely differing theorem proving systems. It's important to absorb the lessons which this teaches about the process in general and the strengths and weaknesses of particular formal systems and proof methodologies. Most of the following is based on personal experience, but I know that much of it will be echoed by other practitioners.

Formalizing mathematics is sometimes quite difficult. It's not uncommon to make a definition, set about proving some consequences of it, fail, and then realize that the definition was faulty. Usually this is because some trivial degenerate case was ignored, sometimes because of a more substantive misunderstanding. This can be tedious, but at other times it is clarifying, and forces one to think precisely.

It's an interesting question whether modest changes to normal mathematical style can render it completely formal, or whether it will always be an unbearably tedious load (some say that 'rigour means rigor mortis'). It certainly doesn't seem too much trouble always to explicitly say that p is a prime, that n is a natural number, that when we talk about the poset X we are talking about the partial order _X, or to distinguish between a function and its value. But it may be that the accumulation of such details renders mathematics too inelegant. Only experience can tell.

Unsurprisingly, formal proofs are long and tedious, and tend to look quite unreadable compared to their textbook models. However we believe several existing systems such as Mizar show that one can still provide fairly readable proof texts, and the main difficulty in practice is automating just the right parts of the reasoning. In principle, there seems no reason why they cannot be brought down to something close to the length of textbook proofs; even less perhaps. Of course, for a few exceptionally explicit and precise textbooks, this may already be the case.

In any case (though this comment might seem to smack of desperation) there are advantages in the fact that proofs are more difficult. One tends to think more carefully beforehand about just what is the best and most elegant proof. One sees common patterns that can be exploited. All this is valuable. Compare the greater care one would take when writing a book or essay in the days before word processors!

In practice formalized mathematics is quite addictive (at least, for a certain kind of personality). This may be similar to the usual forms of computer addiction, but we believe there is another important factor at work. Since one can usually see one's way intuitively to the end of the proof, one has a continual mirage before one's eyes, an impression of being almost there! This must account for the times people stay up till the small hours of the morning trying to finish 'just one last proof'.

Many of the problems are not connected with the profound and interesting difficulties of formalizing and proving theorems, but with the prosaic matter of organizing the resulting database of theorems. Since one will often need to refer back to previous theorems, possibly proved by other people, it's useful to have a good lookup technique. In mathematics texts, readers can only remember a few 'big names' like the Heine-Borel theorem, the Nullstellensatz, and the rather ironic relic of 'Hilbert's Theorem 90' which in retrospect needed a name!. For run of the mill theorems, it's better to number them: although the numeration scheme may be without significance, it does at least facilitate relatively easy lookup (though some books unhelpfully adopt distinct numbering streams for theorems, lemmas, corollaries and definitions). Mizar numbers its theorems, though inside textual units which are named. But this policy seems to us less suitable for a computer theorem prover because it's more common to want to pass from a (fancied) theorem to its identifier, rather than vice versa. Admittedly in the long term we want people to read formal proofs, but at present the main emphasis on constructing them.

With a computer system, textual lookup is at least as easy as numeric lookup, and names can have a mnemonic value, so using names throughout seems a better choice. It also makes it easier to insert or rearrange theorems without destroying any logic in the sequence of numbers. HOL names all theorems, but some theories do not have a consistent naming convention, notably natural number arithmetic which used to include the aptly-named TOTALLY_AD_HOC_LEMMA. A computer can offer the new possibility of looking up a theorem according to its structure, e.g. find a theorem that will match a given term, or contains a certain combination of constants. HOL and IMPS have such facilities. (In a computer system, there is a tendency to have the writer's own convenience at heart rather than that of a later reader or user. Perhaps therein lies the mistake.)

Then there are the social problems: when different people work at formalizing mathematics, they will choose slightly different conventions, and perhaps reinvent the same concepts with different names. For example, one may take < as the basic notion of ordering, one may take (or !). Perhaps there needs to be some kind of central authority (like the Mizar 'library committee') which establishes certain canons, but this is rife with potential for disagreement and petty politicking. We should reiterate our earlier remarks here: there are real advantages in only allowing users one way to do things!

And in practice, a given arrangement is not set in stone; people may want to add more theorems to existing libraries, perhaps slightly modify the theorems on which other libraries depend. It can be very difficult to write machine proofs which are insensitive even to trifling changes in the assumptions. This problem has been studied by [curzon-changes] with respect to large hardware verification proofs. How much worse if we want to change the foundational system more radically (e.g. constructists might like to excise the use of nonconstructive principles in proofs). It seems one should try to write proofs which avoid too many unnecessary parochial assumptions (e.g. the assumption that there are von Neumann ordinals floating around). This is comparable to avoiding machine dependencies in programming.

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