Computers have been used for some time to both discover and check mathematical proofs. Today, automated reasoning is a vibrant field in its own right. The application of computers to the presentation and distribution of proofs has, however, been largely limited to advances in computer typesetting. Yet in some ways the presentation and distribution of a proof can be almost as important as its existence. In order for a result to be generally accepted it must not only be proved, but that proof must be effectively communicated to others.
There are two dimensions to the notion of proof. On one hand a proof is itself a mathematical object: a tree structure with the result at its root, inference rules as its branches, and axioms at its leaves. It is to this dimension of proof that computer support has traditionally been applied. However, a proof is also a social process that exists in the interaction which takes place between the author and reader via the printed page. If the author's argument does not convince the reader then in one respect it is not a proof, at least not for that reader. Increasing the readability of a proof then, in some ways makes it more of a proof. The technique of interactively browsing proofs described here is a potential application of computer support to this other dimension of proof.
The great majority of proofs presented today are still published on paper. For such proofs the structured calculational format described here may still be of some help with presentation, but interactive browsing is clearly impossible. However, the recent advent of electronic journals may help to change that. Mathesis Universalis (Marciszewski 1996), for example, already publishes papers as electronic documents that may be viewed on the world wide web. Journals like this could be used to publish browsable proofs using the system described in the section on proof browsing.