How to submit an article to the MML
To submit an article to the Mizar Mathematical Library please follow these steps:
Submissions which do not meet the abovementioned criteria will be returned
their authors without review.
If you have any questions or comments concerning submissions to the MML,
mus AT mizar.uwb.edu.pl (Mizar User Service) or
mml AT mizar.uwb.edu.pl.
- 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
Observe that the restriction of 80 characters in a line is given
when submitting the article for inclusion in the MML.
- Check if your article uses the local data base. If so, empty local
subdirectory (transfer preliminaries to your article if needed)
- 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.
- 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
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.
- 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.
- Make sure that your article is without errors: remove the
::$V, ::$P, ::$EOF and call Mizar verifier.
version of Mizar as possible.
- 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).
- Use example.bib file (in "doc" directory of your Mizar
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.
- 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
fax: +48 85-738-83-33
PDF versions of the above files are available here (for
one and more
The files can be mailed to:
mml AT mizar.uwb.edu.pl.
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.
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.
Last modified: February 25, 2015