FMM 2018 - Third workshop on Formal Mathematics for Mathematicians

August 13, 2018

The FMM workshop series allows mathematicians interested in computer assistance and researchers in formal and computer-understandable mathematics to meet and exchange ideas. The meeting provides a platform for discussion of suitable forms of computer assistance between the formal community and interested mathematicians and other researchers.

The main points of interest include:

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

Invited speaker(s)

ALEXANDRIA is a new ERC project at the University of Cambridge led by Lawrence Paulson aiming at the creation of a proof development environment for working mathematicians through a collaboration of mathematicians and computer scientists. This will be achieved by formalizing mathematical proofs with the proof assistant Isabelle. The focus of the project is the management and use of large-scale mathematical knowledge, both as theorems and as algorithms. In this talk we will briefly discuss some of our objectives and methods. See: Alexandia

Programme

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 using the style onecolceurws (the corresponding style files can be downloaded from here).

Deadline for submissions: June 10, 2018June 17, 2018
Notification of acceptance: June 30, 2018

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

• Yves Bertot, Inria
• Marco Caminati, University of St Andrews
• Cezary Kaliszyk, University of Innsbruck (co-chair)
• Michael Kohlhase, FAU Erlangen-Nürnberg
• Adam Naumowicz, University of Białystok (co-chair)
• Aleksy Schubert, University of Warsaw
• Josef Urban, Czech Technical University in Prague