Over the past two years, a group from Cornell, Cal Tech and the University of Wyoming have designed and built an experimental digital library of formal algorithmic mathematics. We call the system a formal digital library (FDL). We are now conducting studies and experiments with it about which I will report.

The project has two kinds of goals; one is to assemble content from several theorem provers, and the other is to provide services for using this content. We have collected content from HOL, Nuprl, MetaPRL, and PVS. We hope to add material from Coq, Isabelle, Minlog, Mizar and other systems as well. We have exported content to HELM and are working on a link to OMDoc.

Among the services we are working to provide is logical dependency tracking and Web presentation. We are also experimenting with hybrid proofs and with translations between logics and between different implementations of the same logic. Some of these services depend on theorems of Doug Howe relating type theory and set theory; we have extended them in ways that I will mention, including Moran's theorem about Aczel's CZF.