<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>CICM</journal-title>
      </journal-title-group>
    </journal-meta>
    <article-meta>
      <title-group>
        <article-title>Formal Mathematics for Mathematicians (FMM 2021)</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Jasmin Blanchette</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Adam Naumowicz</string-name>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Department of Computer Science</institution>
          ,
          <addr-line>Vrije Universiteit Amsterdam</addr-line>
          ,
          <country country="NL">The Netherlands</country>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>Institute of Computer Science, University of Bialystok</institution>
          ,
          <country country="PL">Poland</country>
        </aff>
      </contrib-group>
      <pub-date>
        <year>2021</year>
      </pub-date>
      <volume>14</volume>
      <abstract>
        <p>This volume contains the proceedings of the fifth workshop on Formal Mathematics for Mathematicians, FMM 2021, afiliated 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 Commelin (University of Freiburg), Sander Dahmen (Vrije Universiteit Amsterdam), and Karol Pąk (University of Bialystok).</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>