To submit an article to the Mizar Mathematical Library follow these steps:

1. We claim that an author of a Mizar article is satisfied with the content of his article. None of special restrictions are given for the lenght of an article; usually it is from 1000 to 5000 lines, typical length is about 1700 lines. However the article may be rejected if it will be too short.
2. Check if your article uses the local data base. If so, empty local "prel" subdirectory (transfer preliminaries to your article if needed)
3. Check your private vocabulary if you use any: call "checkvoc ". If it contains extended ASCII characters or one-letter symbols, correct the formats. White space in a symbol is not allowed also. Checkvoc compares your private symbols with the ones from the MML and returns error if any repeat.
4. The name of your article had to be built according to the DOS principles with the obligatory extension ".miz". File name must contain only letters, digits and symbol "_". The first character must be a letter (excluding "x"). The length of the name should be between 5 and 8. File name had to be unique, that is it must differ from article names yet submitted to the MML. The correspondence of a name with the title of article as well as 8-chars identifiers are preferred.
5. The vocabulary name should be the same as the article name, but the obligatory extension is ".voc". Make sure that the vocabulary file does not contain unused symbols. For details concerning vocabulary building, check Vocabulary section on WWW.
6. Make sure that your article is without errors: remove the @proof's and call Mizar verifier. Use most recent version of PC Mizar as possible.
7. Use example.bib file (in "doc" directory of your Mizar distribution) to make bibliography note for your article. The name of this file has to be same as the name of your Mizar article file name. Note that English language should be used.
8. Complete submission form (mmldecl.txt in case of one author or mmldecls.txt if more) you may find in Mizar distribution package and send it by snail mail or by fax to the following address:
   Association of Mizar Users
   University of Bialystok
   Institute of Mathematics
   ul. Akademicka 2
   15-267 Bialystok
   Poland
   The fax number: 0-85-745-75-45
   Postscript versions of the above files are available here (for one and more authors).
9. For the above address you can also send MS DOS formatted diskette with your Mizar article and bibliography file (vocabulary if needed). However the easiest way is to e-mail the files to: mml@mizar.uwb.edu.pl. You can use any method to do it: the preferred one is to compress your files with any of popular file compressors (like ZIP, PKZIP, ARJ, RAR, TAR with GZIP, ...) and attach the file to your mail. Please do not send any .miz files 'as is' in the message body.
10. On this page you can check how your article will be automatically TeXed if it will be accepted for publication in the Journal of Formalized Mathematics. The Library Committee strongly encourages the previewing process.