In recent years wikis for formal mathematics have appeared. Formal mathematics presents a number of challenges for the wiki perspective. To enhance the quality of the data in these wikis from the perspective of information architecture, we propose some extensions of existing formal mathematics wikis to more properly handle metadata. Recent years have seen some attention paid to the problem of building wikis for formalized mathematical texts, and there are various proposals and even some live wiki or wiki-like systems for formal mathematics [9, 6]. Formal mathematics (or indeed any formally verified content) presents a number of challenges for the wiki perspective. In this paper we propose some extensions of existing formal mathematics wikis to more properly handle metadata. The aim, ultimately, is to better apply the tools of information architecture [7] for a formal mathematical wiki. We sketch some salient kinds of metadata for formal mathematics and their implementation. Our work is but a modest step toward the grand aim of a semantic web in the domain of mathematics, with a bias toward formal verification.
The efforts of Kohlhase and his collaborators (e.g., [
Some metadata about mizar texts are functions of the text—we can compute the metadata in question— and thus aren’t suitable for user editing. The length of a mizar article in bytes, for example, or the underlying XML representation of an article, are properties of the text that cannot (so far as we can see) be meaningfully modified.
Other properties of texts, however, can be profitably exposed. The following properties of mizar texts are candidates for user-editable properties:
Already there has been some informal efforts to annotate parts of the mizar Mathematical Library
by assigning tags to articles from the American Mathematical Society’s widely used Mathematical
Subject Classification (MSC) scheme [
Citations of relevant mathematical sources (e.g., books, papers, encyclopedia entries).
The mizar definition of cardinal numbers, for example, depends implicitly on the axiom of choice, but it is not clear how this can be detected from the dependency graph of the mizar Mathematical Library (if it is possible at all). It seems better to us to permit users of the mizar wiki to associate the mizar item that represents the definition of cardinal number with the mizar item that represents the axiom of choice. Such links could be represented through Atom link elements and served as See-Also HTTP headers.
Thus, a “named” theorem might have different variants or special cases. For example, the Jordan curve theorem can be understood in complete generality, or in the special case of polygons. A theorem might be started for arbitrary dimensions, but be of especial interest for dimension 2 or 3 (e.g., Euler’s polyhedron formula in full generality and the three-dimensional case). A theorem (or axiom, as the case may be) can even have different forms, such as Zermelo’s well-ordering principle (“every set can be well-ordered”) and a ‘vanilla’ rendering of the axiom of choice (“every non-empty set of non-empty sets has a choice function”) are equivalent to one another (in a suitable background theory, of course).
Some of these metadata categories are already handled outside the context of our wiki. When authors submit their mizar texts to SUM (the mizar User Group, charged with maintaining mizar and its library), they supply the text as well as author and title information, an abstract (in English), and citations to relevant sources (e.g., the source of the “informal” proofs that are formalized in the article). This information is used to automatically generate a TEX representation of an article, which is then published in the journal Formalized Mathematics1. The editors of Formalized Mathematics are charged with maintaining this information. The data is thus static, in the sense that one cannot edit the published title and abstract of a paper that has already been published in a journal.
A wiki that permits editing of metadata that already exists under the aegis of Formalized Mathematics is not intended to compete with that journal. The SUM and its efforts to professionalize the writing of formal mathematical texts (in mizar) complement the project proposed here. We use the the mass of metadata that has been accumulated throughout the construction of the MML to seed our wiki with an initial pool of trustworthy data. Our aim is to make the sea of (mizar-)formalized mathematical knowledge discoverable and improvable. Where possible, we provide links to the authoritative, original sources for mizar formalizations.
Metadata support in the mizar language itself is (almost) entirely lacking. One cannot use the language itself to indicate, for example, the author of a mizar text. The language supports only one metadatarelated construction, the section keyword, which takes no arguments and it intended to delimit different parts of an article.
In the context of a live wiki, however, curation-by-committee is not a viable option for eliciting and maintaining metadata. One must go beyond the mizar language and provide a means of attaching or editing metadata. Since one cannot directly add this information to mizar texts, in the context of a web interface, one must enter the information in a form.
The absence of metadata functionality from the mizar language (apart from the aforementioned section keyword) is, to some extent, an advantage, because it gives a clear separation of responsibility of the validity of the text from information about the text. Our wiki process for registering and maintaining metadata can complement the standard process for eliciting this data. With each new release of the mizar Mathematical Library, we receive another batch of “canonical” or official metadata for updated contents of the library. 4
We serve metadata in two ways: in the HTTP headers, and in the body of our article representations. We
adhere to RESTful principles [
We use the Atom Publishing Protocol and its extensible notion of link [
rel =" http :// wiki . example . org / rels / author " ...
1See http://fm.mizar.org.
2See http://linkeddata.org/
In this example, in addition to standard HTTP headers, we use the proposed Link HTTP header [
One challenge in the context of a wiki is to provide keep URIs “cool”, that is, essentially permanent
objects. The slogan here is “Cool URIs don’t change” [
Richer representations of formalized mathematical data and its metadata are available. Thus, one could serve RDFa or employ a suitable microdata framework. Richer representations of the mizar data itself as RDFa, or a documented, well-structured URI namespace for items, would be valuable. In the face of capable clients, one could even imagine performing non-trivial content negotiation; today, mizar text are served only as plain text or as (relatively thinly annotated) HTML.
Finally, it should be clear that although we focus on mizar, few parts of the project that directly depend on the mizar language, its tool set, or its library. The wiki principles developed here would apply to any other system as well. Indeed, a formal wiki for other systems, suitably equipped with the kind of metadata, would be a step toward setting up rich correspondences between various formal libraries and their web representations.