Formalized Mathematics

A pioneering, proof-checked mathematical journal in the field since 1990. It publishes original articles on mechanically checked, formalized mathematics.
The formalisation of mathematics using computer programs to verify mathematical proofs, effectively bridging the gap between human-readable mathematical arguments and machine-checkable logic. Long-term experience in publishing original articles of formalized, computer-checked mathematics, and various aspects of automated reasoning.

This is still a relatively new research area, situated at the intersection of MATHEMATICS, COMPUTER SCIENCE and AI. Notably, it was only recently given formal recognition in the Mathematical Subject Classification system (MSC2020) under the category
- "68V20: Formalization of mathematics in connection with theorem provers",
- "03B35: Mechanization of proofs and logical operations",
- "68V35: Digital mathematics libraries and repositories",
as defined by Mathematical Reviews and zbMATH.
The mathematical scope of the journal covers all areas of mathematics.

Our publications are significant academic contributions to the field of formalized mathematics. This field is closely tied to computer science, particularly logic and artificial intelligence, as it leverages computational power to enhance mathematical rigor and reliability.

New publishing technology: all papers are checked by the Mizar System and automatically translated into LaTeX code in English. Each published article has a link to the formal source.

They form the Repository of formally checked mathematics. The world's largest and most rapidly growing Repository of formalized mathematics. Repository can be used by artificial intelligence programs as a reasoning “engine” (symbolic processing) in AI chatbots (LLM) and for proving properties of computer programs.

Publication timeframe: Volume Open.
The official abbreviation of the Journal is: Formaliz. Math.
The main version of the Journal is the electronic version.

Archiving

Sciendo archives the contents of this journal in Portico - digital long-term preservation service of scholarly books, journals and collections.

Back Issues

fm.mizar.org/

Other Files

Addenda 2008
Formalized Mathematics Bibliography File.
Formalized Mathematics External Bibliography File.

In years 2023-2024: Formalized Mathematics was financed under
agreement RCN/SP/0479/2021/1
with the funds from the Polish Minister of Education and Science for the
development of scientific journals.

In years 2016-2017: Formalized Mathematics was financed under
agreement 548/P-DUN/2016
with the funds from the Polish Minister of Science and Higher Education
for the dissemination of science.

In years: 1995 - 1997 financed by Office of Naval Research Project (USA).