=Paper=
{{Paper
|id=Vol-3377/fmm-preface
|storemode=property
|title=FMM Preface
|pdfUrl=https://ceur-ws.org/Vol-3377/fmm-preface.pdf
|volume=Vol-3377
|authors=Jasmin Blanchette,Adam Naumowicz
|dblpUrl=https://dblp.org/rec/conf/mkm/BlanchetteN21
}}
==FMM Preface==
<pdf width="1500px">https://ceur-ws.org/Vol-3377/fmm-preface.pdf</pdf>
<pre>
Formal Mathematics for Mathematicians (FMM 2021)
Jasmin Blanchette1 , Adam Naumowicz2
1
    Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
2
    Institute of Computer Science, University of Bialystok, Poland



   This volume contains the proceedings of the fifth workshop on Formal Mathematics for
Mathematicians, FMM 2021, affiliated with CICM 2021. The initial workshop in the series
was the AMS Special Session on Formal Mathematics for Mathematicians: Developing Large
Repositories of Advanced Mathematics held in New Orleans in 2011. The next FMM meetings
took place in Washington (with CICM 2015), Bialystok (CICM 2016), Hagenberg/Linz (CICM
2018), and Prague (CICM 2019).
   There were fifteen submissions to FMM 2021. All submissions were reviewed by at least two
reviewers, and the program committee decided to accept thirteen of them.
   The program featured two invited talks: one talk by Mario Carneiro (Carnegie Mellon
University) on porting Lean’s mathlib, and one talk by Manuel Eberl (Technical University of
Munich) about fighting the curse of De Bruijn.
   The contributed research presentations were split into four sessions spread over two days
(July 30-31, 2021). The presented works involved formalizations done with the proof assistants
Lean (7 works), Isabelle/HOL (3), Mizar (2), and Coq (1).
   Finally, we want to acknowledge and thank the rest of the program committee: Mauricio
Ayala Rincón (Brasilia University), Anthony Bordg (University of Cambridge), Johan Com-
melin (University of Freiburg), Sander Dahmen (Vrije Universiteit Amsterdam), and Karol Pąk
(University of Bialystok).




CICM 2021: 14th Conference on Intelligent Computer Mathematics, July 26–31, 2021, Timisoara, Romania
$ j.c.blanchette@vu.nl (J. Blanchette); adamn@mizar.org (A. Naumowicz)
 0000-0002-8367-0936 (J. Blanchette); 0000-0003-4224-9798 (A. Naumowicz)
                                       © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)

</pre>