Since the inception of the first systems designed for developing mathematical proofs in a computer-based environment the research on automated theorem proving and proof checking has produced numerous proof-assistant tools. Their involvement in large-scale formalization projects revealed that practical formalization of whole theories, complete mathematical monographs or especially challenging proofs requires a substantial amount of dedicated work. It has become evident that for this sort of task accumulating and distributing previously formalized data is indispensable.

   In this spirit the Mizar community initiated in 1989 a long-term project of building a comprehensive library of formally interrelated mathematical data, the Mizar Mathematical Library (MML). As of today, MML contains over a thousand articles written by more than two hundred authors from 13 countries that comprise about 50000 theorems from a vast range of mathematical domains. Still, the library might be considered minute when compared to the huge body of mathematics developed throughout the past centuries. Admittedly, it has been estimated that building a formal library to cover only undergraduate mathematics would require about 140 man-years. Therefore it has been recognized that developing a library to base further formalizations on is equally essential as improving the capabilities of proof-assistance software.

   With this special issue we would like to disseminate research experiences with all proof-assistant systems that collect user contributions in an organized manner, attempt to build proof libraries and allow for new developments on top of previously accumulated mathematical knowledge. Expanding such libraries and at the same time making them coherent, well-organized and suitable for querying is a highly non-trivial enterprise. Therefore we also welcome new ideas advancing the field of formalizing mathematics, with special focus on reconstructing the existing body of mathematics in a computer environment.

   We solicit original papers addressing the issues mentioned above. Submitted works will be subject to a usual journal peer-review process. To facilitate typesetting, the submissions should be in PDF using the LNCS format (authors of accepted papers will be requested to provide the LaTeX source). Submissions and any inquiries about this issue should be sent to slgrsubmission@mizar.uwb.edu.pl.

Submission deadline: October 1, 2008
Notification of acceptance: November 1, 2008
Page limit (flexible): 20