To submit an article to the Mizar Mathematical Library please 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 length of an article; usually it is between 1200 and 5000 lines, typical length is about 1700 lines - we strongly recommend submission of longer articles. Observe that the restriction of 80 characters in a line is given when submitting the article for inclusion in the MML.
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 ancient "8+3" 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" as it is reserved for some special encyclopaedic files). 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 technical pragmas ::$V, ::$P, ::$EOF and call Mizar verifier. Use most recent version of Mizar as possible.
7. Please make sure that your file is clean under all standard Mizar review programs available in your distribution: RELPREM, RELINFER, CHKLAB, INACC, TRIVDEMO and RELITERS. Also in your environment description unnecessary directives should be deleted (IRRVOC and IRRTHS programs will be useful).
8. 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. Please add at least one citation for an external (i.e. non-Mizar) article as given in the example bib-file.
9. 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 Informatics
   ul. Konstantego Ciolkowskiego 1M
   15-245 Bialystok
   Poland
   fax: +48 85-738-83-33
   PDF versions of the above files are available here (for one and more authors).
10. The files can be mailed to: mml AT mizar.uwb.edu.pl. Please compress your files with any of popular file compressors (ZIP is strongly preferred) and attach the zip-file to your mail. Please do not send any .miz files 'as is' in the message body. Such mails will be returned back to author.
11. On this page you can check how your article will be automatically LaTeXed if it will be accepted for publication in the Formalized Mathematics journal. The Library Committee strongly encourages authors to use the previewing process.