You must enable JavaScript to use this site
  • FMM 2021 – Fifth Workshop on Formal Mathematics for Mathematicians

    30–31 July 2021

    The FMM workshop series enables 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

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

    Invited speakers:

    Manuel Eberl, TU Munich, Germany

    Title: TBA

    Mario Carneiro, Carnegie Mellon University, USA

    Title: TBA

    List of accepted papers

    Sebastien Gouezel. Formalizing the Gromov-Hausdorff space
    Muhammad Harun Ali Khan. Formalizing Fibonacci Squares
    Alexander Bentkamp and Jeremy Avigad. Verified Optimization (work in progress)
    Anthony Bordg and Nicolo Cavalleri. Elements of Differential Geometry in Lean: A Report for Mathematicians
    Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho and Katsumi Wasaki. A Web Platform for Hosting the Mizar Mathematical Library
    Alexander Best. Automatically Generalizing Theorems Using Typeclasses
    Zibo Yang. Formalization of Gambler’s Ruin Problem
    Eric Wieser. Scalar actions in Lean's mathlib
    Karol Pąk. Formalization of Prime Representing Polynomial in Mizar
    Yury Kudryashov. Formalizing rotation number and its properties in Lean
    Flavio L. C. de Moura and Leandro O. Rezende. A Formalization of the (Compositional) Z Property
    Stepan Holub. Computing the Border Array in Isabelle/HOL
    Martin Raška and Štěpán Starosta. Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL


    See FMM sessions in the CICM programme on Friday, July 30 and Saturday, July 31.


    Electronic submission is continuous and done via EasyChair: select the author role, select the "new submission" tab, and choose FMM. We welcome submission of short papers presenting research related to the workshop's points of interest. Submitted papers should be 4–6 pages long and formatted in LaTeX using the style onecolceurws (the corresponding style files can be downloaded from here).

    • Submission is continuous until 14 July 2021 (AoE).
    • Reviews sent back no later than 21 July 2021.
    • Final revised papers due by 25 July 2021.

    At least one author of each accepted paper is expected to attend FMM and present the work online.

    We plan to publish electronic proceedings in the CEUR Workshop Proceedings series.

    Organizers and Programme Committee

    • Mauricio Ayala Rincón, Brasilia University, Brasil
    • Jasmin Blanchette, Vrije Universiteit Amsterdam, the Netherlands (co-chair)
    • Anthony Bordg, Cambridge University, UK
    • Johan Commelin, Universität Freiburg, Germany
    • Sander Dahmen, Vrije Universiteit Amsterdam, the Netherlands
    • Adam Naumowicz, University of Bialystok, Poland (co-chair)
    • Karol Pąk, University of Bialystok, Poland
  • News

    • Proceedings available online until 27 July at this link
    • Preliminary programme published
    • Cfp third round
    • Deadlines extended
    • Cfp second round
    • Springer LNAI proceedings confirmed
    • Cfp first round
    • Dates online
    • Calls online
    • Invited speakers
    • PC online
    • Initial website online
Privacy policy and legal information
Last modified: July 26 2021 08:19:46 CEST