Formalized Mathematics

Formalized Mathematics is issued yearly (Volume Open) and publishes articles contributed to the Repository "Mizar Mathematical Library".

The journal accepts submissions of research articles.
The journal archives the proof-checked source code of every submitted formal mathematics article.

Manuscript Submission

Manuscripts should be submitted to the address at the bottom of this page. Submission of a manuscript implies: that the work described has not been published before; that it is not under consideration for publication elsewhere else; and that its publication has been approved by all co-authors, if any, as well as by the responsible authorities – tacitly or explicitly – at the institute where the work has been carried out.

We do not have a specific LaTeX style because submitted articles are automatically translated into English in LaTeX. We require a bibliography in BibTeX style.

Instruction for Authors

Review Procedure:

Double blind: all papers are reviewed by at least two experts from the relevant field. The reviewers do not know the authors' names, and the authors does not know the reviewers' names. Each reviewer has three weeks to write a report, but this timeframe may be extended based on their situation.

The editor and reviewers can check the submitted code using the proof-checker system. Reviewers must verify that the authors correctly formulated their definitions and theorems and that the code does not contain hidden assumptions.
The following is very important:
- the presentation of the theory, the value of the originality,
- the quality of the formalization,
- the significance of the results for the Repository.
Reviewers can download the electronic Referee's Form from this link:

Every effort will be made to reach a decision within one month and to publish accepted papers within three months. Authors of the paper have usually 15 days to revise the paper by considering the suggestions given by the reviewer/editor. If authors need to spend more time, the scheduled time may be extended upon request from the corresponding author. If a revised paper is not resubmitted by the deadline, it will be rejected by the editor.

Rejection Rate: 45-55% of submitted articles.

Additionally you can see the reviewing process and the rejection percentage described in detail in the following paper: pp.239-240: dx.doi.org/10.1007/978-3-540-73086-6_20, (pdf file)
How to review formalized mathematics - more general guidelines by A.Bauer.

List of Reviewers

• Kenichi Arai, Tokyo University of Science, Japan
• Czeslaw Bylinski, Association of Mizar Users, Japan
• Marco Caminati, Lancaster University, UK
• Roland Coghetto, A.S.B.L. La Louviere, Belgium
• Adam Grabowski, University of Bialystok, Poland
• Ievgen Ivanov, Taras Shevchenko National University, Kyiv, Ukraine
• Peter Jaeger, Munich, Germany
• Artur Kornilowicz, University of Bialystok, Poland
• Roman Matuszewski, Association of Mizar Users, Japan
• Yatsuka Nakamura, Shinshu University, Japan
• Kazuhisa Nakasho, Iwate Prefectural University, Japan
• Adam Naumowicz, University of Bialystok, Poland
• Hiroyuki Okazaki, Shinshu University, Japan
• Karol Pąk, University of Bialystok, Poland
• Marco Riccardi, University of Pisa, Italy
• Josef Urban, Czech Institute of Informatics, Prague
• Katsumi Wasaki, Shinshu University, Japan
• Yasushige Watase, Rissho University, Tokyo, Japan
• Freek Wiedijk, Radboud University, the Netherlands.

Open Access Statement

This is an open access journal that provides free, immediate, and unrestricted online access to all its published content for readers around the world.

Articles are available under the Creative Commons Attribution-ShareAlike License (CC-BY-SA) version 4.0 Unported (https://creativecommons.org/licenses/by-sa/4.0/).
A detailed report on choosing the license: arxiv.org/abs/1107.3212.
Open Access Policy: this journal provides immediate open access to its content.

The journal does not have article processing charges (APCs) nor article submission charges.

Instruction for Authors

Articles should be submitted to:
Adam Grabowski,
Faculty of Comuter Science
University of Bialystok
ul. Ciolkowskiego 1 M
15-245 Bialystok, Poland
by e-mail: mml@mizar.uwb.edu.pl