FMM is a workshop a liated with CICM 2016 intended to gather together mathematicians interested in computer assistance and researchers in formal and computer-understandable mathematics.
The mathematical community today seeks various ways to support their work by accessing digital libraries and repositories, applying Internet search techniques to better explore and classify the vast mathematical knowledge, and to combine computer calculations with informal mathematics. Related methods have been developed a lot recently by the formal community, allowing the building of very large formal mathematical libraries and full formal veri cation of large computationally involved proofs such as those of the Kepler conjecture and the Four Color Theorem.
It is very important to establish a platform for both communities to interact. The successful development of computerized formal mathematics and its general availability very much depends on the feedback that the formalized mathematics developers can obtain from the community of working mathematicians. This workshop's main objective is to explore ways of building synergy between the two communities.
Over the last decades, we witnessed a number of successful instances of computer-assisted formalization of mathematical problems. Research in this eld has been boosted by the development of systems for practical formalization of mathematics (proof assistants), a creation of large repositories of computerveri ed formal mathematics, and integration of interactive and automated methods of theorem proving. Proof assistants provide a very useful teaching tool suitable for undergraduate instruction, in particular for training beginning students in writing rigorous proofs. An expected wider outcome of this workshop is therefore setting up of an annual series of meetings between working mathematicians and researchers in formal mathematics as well as graduate students with strong background in these elds.