In our description of the Mathematical Bus up to now, we have regarded objects shared between packages as ephemeral---objects are translated to the common mathematical language and then back again as packages inter-operate. But once the data types and definitions are in place for some subset of interesting mathematical objects, it becomes possible to make objects permanent.
The permanent objects are not just the ``data'' but also the ``definitions'' and ``theorems'' themselves. This is because the formal system we envision treats data, definitions, theorems, and so on with a uniform notation. Nuprl is an example of such a system.
Indeed, a major component of our envisioned collaborative mathematics environment will be a database of definition, display forms, facts, algorithms, theorems, explanations, transformations, system-level (meta) functions, and methods. We expect these to be linked by a user interface that will provide natural ways to browse, as with Mosaic on the Nuprl library browser. Moreover, there will be system-level functions to automatically access data and use it. A model for this is the Weyl transformation and Nuprl tactics.
When one thinks of mathematical repositories, one usually thinks of software libraries like Netlib [35] or GAMS [15]. These libraries are enormously successful, having made a large body of numerical software widely available twenty-four hours a day. However, when software synthesis becomes more widely accepted the structure of these libraries will change and new problems will arise.
As a simple example of such a library, consider the problem of selecting elements (shape functions) to use as a basis in a finite element method. A typical finite element package such as ANSYS offers the user dozens of elements, documented by many pages of the ANSYS manual. In our imagined library, these shape functions could be stored together with all their attributes such as order, degree of continuity, and nodal coordinates. This information could then be used in synthesis of a numerical method, with pre- and post- conditions automatically checked. This kind of database entry is considerably different from the traditional subroutine-library approach, because most of the useful information about a shape function takes the form of specification rather than executable code.