<div dir="ltr"><div><div>Hello all,<br><br></div>Although the implementation is still in progress, I've completed a writeup of the algorithm for converting OT article files into valid Metamath proofs, to be published in the Journal of Formalized Reasoning. You can find the preprint on arXiv, <a href="http://arxiv.org/abs/1412.8091">http://arxiv.org/abs/1412.8091</a> .<br><br></div><div>I've also been thinking about the reverse conversion process, but before I get into the details I'd like to establish what are the usual conventions are for producing good output, since so far I've only looked at the article level and haven't even touched any theory files. In particular, how should I structure the theory division process, and what OT base definitions should I import?<br><br></div><div>For context, a Metamath file is a list of theorems, where each theorem has a derivation that refers to textually previous theorems or axioms. The entire metamath database is one (rather large) file, and there are section headers, but they are just comments (although they are machine-readable for presentation purposes). I expect that the different theorems correspond well to "thm" exports, and perhaps the section headers correspond to theory files (although there are quite a few, perhaps a few thousand section headers). The sections come in three levels, from the 14 major "parts" to the "chapters" and then "sections", each of which might have from 1 or 2 to a couple hundred theorems each. (see: <a href="http://us2.metamath.org:88/mpegif/mmtheorems.html">http://us2.metamath.org:88/mpegif/mmtheorems.html</a>)<br><br></div><div>Also, Metamath is built on ZFC foundations, although we also have the Tarski-Grothendieck axiom defined. However, Metamath tracks axiom usage, and there is a conscious effort to limit unnecessary axiom usage (most other systems don't seem to do this, i.e. using the axiom of choice to prove the law of excluded middle is rather overkill), so it is possible that some of the weaker subsystems fit in vanilla HOL. However, it is well-known that ZFC is stronger than HOL, and so the general approach I was intending is to add some kind of universe axiom to say that "ind" is a really big set, big enough for some construction of an epsilon-relation to satisfy the axioms of ZFC. Does anyone know of research and/or existing definitions along these lines?<br></div><div><br></div>Mario Carneiro<br></div>