Abstract

An integral piece of building a comprehensive library of formal mathematics is ensuring that the content is accessible. We want users to be able to easily find relevant Nuprl objects, through web search or improved library browsing, and help them understand the objects in which they are interested. To this end, we would like to attach annotations to formal objects. These annotations can take a variety of forms, from keywords and synopses, which we expect to collect from system users, to automatically generated information about the link structure of the library and references to supporting content for each object. We will discuss these annotations and the various methods we have been using to obtain them.