Formalized Mathematics (AutoMath)

The Nuprl Library is a repository for the definitions, theorems and proof procedures of formal mathematics. It is one of a handful of systems worldwide that is creating a new digital artifact of great significance. This section looks at the history of this aspect of our work. It is a view of the history of logic from a modern vantage point which recognizes that a new discipline has been created by the past efforts of logicians, applied logicians and computer scientists.

Frege, Hilbert and Post

The first truly formal mathematical text is Frege's Begriffsschrift (ideography), completed in 1879. As Martin Davis said about it:

Begriffsschrift is not only the direct ancestor of contemporary systems of mathematical logic, but also the ancestor of all formal languages including computer programming languages. (Citation.)

Frege's reason for creating this "ideography" or "concept script" is essentially the reason behind creating formal verification systems; that is, he wanted to leave no gaps in his reasoning. He said,

Its first purpose, therefore, is to provide us with the most reliable test of the validity of a chain of inferences and to point out every pre-supposition that tries to sneak in unnoticed, so that its origin can be investigated.

It is worth reading more of the introduction to Begriffsschrift to see how Frege was led to this revolutionary new idea, the idea underlying all the work we do on this project. (Citation.)

David Hilbert was led to the idea of a formal system for similar but distinct reasons. He developed this notion with increasing precision and clearer purpose in the 1920s, at the same time that Emil Post was coming to them in his 1920 PhD thesis in the United States. Hilbert understood the idea of removing the meaning from an axiom system from his work on the foundations of geometry.

Hilbert eventually (in the 1920s) based his famous "program" for "saving mathematics" from its foundational crisis on the idea of studying formal systems as mathematical objects using a highly constructive, even finitistic, mathematics which he called metamathematics. In this view, mathematics is considered to be a meaningless game, like chess. The only important property of the game is that it be free from contradiction. His bold idea for a program of salvation was to show, using finitary means, that the game was safe. Some of the results would be meaningful, at least the finitistic ones and perhaps the constructive ones if Brouwer had a say (See Constructive Mathematics); while other results were only "ideal." They lacked meaning in themselves, but could be used as shortcuts to deriving the meaningful ones in the game.

Hilbert's program was so bold and promising that it even won over Brouwer's disciple, Arend Heyting, who saw it as a way to reconcile classical and intuitionistic mathematics. But Gödel detected a flaw in this program. His incompleteness theorem essentially said that no formal system was strong enough to guarantee that the game would not allow results that were false or meaningless. That is, since there are true theorems that can not be proved in the game, it is possible to add false axioms and still have a safe (consistent) but meaningless system of mathematics. Here is what Gödel said at a small meeting on Foundations at Konigsberg in September, 1930.

On the contrary it would be, for example, entirely possible that one could prove with the transfinite methods of classical mathematics a sentence of the form Exists x F(x) where F is a finite property of the natural numbers ... and on the other hand recognize through conceptual considerations that all numbers have the property not F; and what I want to indicate is that this remains possible even if one had verified the consistency of the formal system of classical mathematics. (Citation.)

Gödel had already realized that "one cannot claim with certainty of any formal system that all conceptual considerations are representable in it." The questions motivating Gödel's theorem are still being asked about physical theories. For example, E. O. Wilson in Consilience asks whether there might be an interpretation of mathematical physics which is completely different from the physical world as we know it.


The idea to use computers in carrying out a massive formalization of mathematics is well articulated in Wang. But the first sustained project to do this was N. G. deBruijn's Automath Project. The copious work done by the Automath project is now collected in a 1024-page 1994 North-Holland publication, Selected Papers on Automath. (Citation.) The style and scope of the work can be seen in this quote from the first publication about the project in the book.

Technical Contributions

Our contributions can be understood by comparison to the pioneering and brilliant work of N. G. de Bruijn on Automath. It was this project along with Edinburgh LCF that directly inspired us, and in some ways we have not yet achieved the total breadth of the Automath conception, especially in regard to the structure of a "library" of formal on-line texts into a "tree of knowledge." But in some respects we have gone well beyond Automath, as we indicate.

First, the formal text we produce is directly readable as ordinary mathematics. Moreover, we can change the display of all the text with the trivial operation of changing the display form of an object. This powerful mechanism was introduced in PRL by Joe Bates and brought to the state-of-the-art by Stuart Allen and Richard Eaton.

Second, we can generate formal text from rigorous text at rates ten times faster than the Automath user.

Third, the expansion factor from rigorous text to Automath text was nearly 50 to 1 whereas for us it is more like 5 to 1. We have the tools to make the expansion close to 1 for completely rigorous proofs into formal proofs. We aim to create a situation where the normal display of formal argument is shorter than rigorous proof.

Fourth, we can incorporate proofs from other systems such as HOL. We can produce multiple logic arguments and keep track of the logical dependencies.

Fifth, we have tools to formally manipulate entire theories. So it is possible to generate a variant of a theory automatically as Chet Murthy showed by producing a constructive account of Higmann's Lemma from a classical one.

Sixth, our text is formal hypertext so that concepts are automatically linked. This makes our library into a semantic net. The naming convention for library objects is used to guide automatic search for content.

Seventh, our text can be automatically displayed on the Web.