In high school algebra solutions to most problems can be checked by simple
computation; for instance,
one can easily verify by substitution and reduction that 17 is a root of
.
Those who are pleased with the certainty of such solutions may also
hope to find ways of checking solutions to more abstract problems
(such as showing that 
is irrational) computationally.
The idea that computers can check proofs is a step
toward achieving this ambition [McCarthy 62,deBruijn 80], and there are
several interesting implementations of this idea [Suppes 81,Weyhrauch 80,Constable, Johnson, & Eichenlaub 82,Gordon, Milner, & Wadsworth 79].
The computer system described here represents another approach to this problem.
Someone who has struggled for hours or perhaps days to untangle the details of a complex mathematical argument will understand the dream of building a computer system which helps fill in the details and keeps track of the proof obligations that must be met at the critical points of an argument. There are computer systems which do this, and it is possible in principle to solve problems in a system of this kind which are beyond the patience and capability of an unaided human being, as K. Mulmuley has already demonstrated in LCF [Mulmuley 84]. Nuprl uses some of the mechanisms of LCF which make this possible, namely the metalanguage ML in which the user writes programs to provide help with the details.
People who have spent hours or days getting a mathematical construction such as Gauss' construction of a regular 17--gon exactly right will know the desire to watch this mathematical construction ``come to life.''
was built to meet such aspirations. Every construction described in 's mathematics can, in principle, be executed mechanically. In particular, can execute functions and thus serve as a programming language in the usual sense.
Anyone who has tried to write a mathematical paper or system consisting of several interacting theorems and constructions will appreciate having a uniform notation for discourse and a facility for creating an encyclopedia of results in this notation. The Bourbaki effort [Bourbaki 68] manifests such aspirations on a grand scale, and
is a step toward realizing this goal. It supports a particular mathematical theory, constructive type theory, whose primitive concepts can serve as building blocks for nearly any mathematical concept. Thus provides a uniform language for expressing mathematics. This is a characteristic that distinguishes from most other proof--checking or theorem--generating systems.
Anyone who has written a heuristic procedure such as one for playing games or finding proofs and who has seen it do more than was expected will understand the dream of using a computer system which can provide unexpected help in proving theorems. It is easy to extrapolate to dreams of machines offering critical help in solving real problems. Substantial effort has been put into ``theorem--proving'' programs which attempt to provide just such help, usually in a specific domain of mathematics. While is not a theorem--proving program in the usual sense, it is a tool for exploring this kind of heuristic programming. Users may express a variety of procedures which search for proofs or attempt to fill in details of a proof. The system has already provided interesting experiences of unexpected behavior by finishing proofs ``on its own.''
People who have experienced the new electronic medium created by computers may imagine how mathematics will be conducted in it. We see electronic mail and electronic text editing. We see systems like the Cornell Program Synthesizer [Teitelbaum & Reps 81] that help users specify objects such as programs directly in terms of their structure, leaving the system to generate the textual description. We can imagine these ideas being applied to the creation of mathematical objects such as functions and proofs and their textual descriptions. In this case, because mathematical structure can be extremely complex, one can imagine the computer providing considerable assistance in producing objects as well as help in displaying the text and giving the reader access to the underlying structure in various ways.
offers such capabilities, the most striking among which are the help the system provides in writing formal text (see chapter 3) and in reading and generating highly structured objects such as proofs and function terms. As with all aspects of there is much to be done to achieve the goals that motivated the design, but in every case the system as it stands makes a contribution. We hope it will show the way to building better systems of this kind.