You must enable JavaScript to use this site
  • NatFoM 2021 - Workshop on Natural Formal Mathematics

    The workshop will take place virtually using the same login details as the CICM conference.

    In mathematics there has always existed a strong informal sense of "naturality". Natural theories, notions, properties, or proofs are prefered over technical, convoluted, or counterintuitive approaches. If formal mathematics is to become part of mainstream mathematics, its formalizations and user experience have to become more natural. This workshop, following a first edition in 2020, broadly addresses the issue of naturality in formal mathematics.

    Topics of interest include (but are not limited to):

    • The notion of naturality in mathematics generally
    • Natural input and output languages for formal mathematics systems
    • Parsing natural mathematical language
    • Controlled natural languages (CNL) for mathematics
    • Making formal mathematics documents readable
    • Naturality of foundational theories (types, sets, HOL, ...)
    • Naturality of proof methods
    • Natural proof structures and granularities
    • Natural structurings of formalized mathematical texts and libraries
    • Mathematical type setting (LaTeX) and formal mathematics
    • Examples of natural formalizations

    Invited Talks

    Jeremy Avigad


    We call for submissions of extended abstracts (1 page) and demonstration proposals presenting work related to the workshop's topics of interest. Accepted abstracts can optionally be expanded to full papers (4 to 15 pages) to be published in proceedings on To promote Natural Formal Mathematics, unfinished or exploratory work will also be welcome.

    Electronic submission is done through EasyChair (select the author role, select the "new submission" tab, and choose "NatFom"). Extended abstracts and papers should be formatted in LaTeX using the style onecolceurws.

    • Submission is continuous (early submit -> early notify).
    • July 1. 2021: Final revised papers due
    • July 26 - 31. 2021: Workshop (half day; date to be announced)
    Accepted abstracts and demonstrations should be presented online and live, to allow for questions and discussions.

    Program Committee

    • Peter Koepke, Bonn (co-chair)
    • Dennis Müller, Erlangen (co-chair)
    • Merlin Carl, Flensburg
    • Marcos Cramer, Dresden
    • Michael Junk, Konstanz
    • Cezary Kaliszyk, Innsbruck
    • Andrea Kohlhase, Neu-Ulm
    • Aarne Ranta, Gothenburg
    • Josef Urban, Prague
  • 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: May 17 2021 17:34:01 CEST