FMM - Formal Mathematics for Mathematicians

FMM is a workshop affiliated 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 verification of large computationally involved proofs such as those of the Kepler conjecture and the Four Color Theorem.

FMM's aims

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 field has been boosted by the development of systems for practical formalization of mathematics (proof assistants), a creation of large repositories of computer-verified 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 fields.

Points of interest include:

• formalization of challenging mathematical problems,
• interactive and automated theorem proving,
• development of proof assistants,
• design of proof languages and techniques,
• repositories of formalized mathematics,
• semantic representation of mathematical knowledge,
• formal tools in program verification,
• foundations and philosophy of mathematics,
• proof assistants in education.

Invited speaker(s)

Aleksy Schubert, University of Warsaw: On Differences in Proofs Between Intuitionistic and Classical Logic


The presentation will contrast the complexity results for proving assertions in classical and intuitionistic logic. The comparison will be built upon the known results for propositional logic and predicate one. The predicate case will be based upon the Mints hierarchy in intuitionistic logic which will be contrasted with its counterpart i.e. the prenex hierarchy in classical logic.
The differences in complexity will be illustrated with examples of particular proving mechanisms that are responsible for the divergence, which should facilitate the understanding of where the mathematics is done constructively.

Chad Brown, Czech Technical University: Developments, Libraries and Automated Theorem Provers

When formalizing a mathematical development with an interactive prover, it is helpful if the user can interface with a library (to avoid starting from scratch) and with automated provers (to avoid needing to give full details explicitly). We will consider an example of a development in Mizar, leading to some discussion of how one can interact with Mizar's library and how automated theorem provers can help construct Mizar proofs. With this example in mind, we discuss criteria for three aspects of formalization to work in harmony: formal mathematical developments, working with a global library of theorems and definitions and making use of automation.

Submissions

We welcome submission of extended abstracts and demonstration proposals presenting work related to the workshop's points of interest. Electronic submission is done through EasyChair. Extended abstracts and demonstration proposals should be no more than 4 pages formatted in LaTeX according to requirements of Springer's LNCS series (the corresponding style files can be downloaded from http://www.springer.de/comp/lncs/authors.html).

Deadline for submissions: June 20, 2016
Notification of acceptance: June 30, 2016

At least one author of each accepted extended abstract/demonstration proposal is expected to attend FMM and presents his/her extended abstract/demonstration. The extended abstracts will be made available online.

Programme Committee (TBC)

• Marco Caminati, University of St Andrews, UK
• Claudio Sacerdoti Coen, University of Bologna, Italy
• Adam Grabowski, University of Bialystok, Poland
• John Harrison, Intel, USA
• Cezary Kaliszyk, University of Innsbruck, Austria
• Artur Kornilowicz, University of Bialystok, Poland
• Krystyna Kuperberg, Auburn University, USA
• Adam Naumowicz, University of Bialystok, Poland (chair)
• Josef Urban, Czech Technical University in Prague, Czech Republic
• Freek Wiedijk, Radboud University, The Netherlands