NFM 2020  Workshop on Natural Formal Mathematics
July XXX, 2020 (exact date tba)
In (pure) mathematics there has always existed a strong informal sense
of "naturality" of topics and methods. Generally "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 usage apparently have
to become more "natural". Or should mathematicians learn formal
languages like Lean so that they regard them as natural? This workshop
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 speaker: tba
Submissions
We welcome submission of extended abstracts and demonstration proposals
presenting work related to the workshop's topics of interest. Electronic
submission is done through EasyChair. Extended abstracts and
demonstration proposals should 1 page formatted in LaTeX using the style
onecolceurws (the corresponding style files can be downloaded from here).
 First round submission deadline: April 15 2020
 Notification of acceptance: May 01 2020
 Second round submission deadline: June 15 2020
 Notification of acceptance: July 01 2020
At least one author of each accepted extended abstract/demonstration
proposal is expected to attend NFM and presents his/her extended
abstract/demonstration. The extended abstracts will be made available
online.
Program Committee
 Florian Rabe, Erlangen (cochair)
 Peter Koepke, Bonn (cochair)
 Merlin Carl, Flensburg (tbc)
 Marcos Cramer, Dresden
 Adam Grabowski, Bialystok (tbc)
 Michael Junk, Konstanz (tbc)
 Cezary Kaliszyk, Innsbruck
 Andrea Kohlhase, NeuUlm
 Karol Pak, Bialystok (tbc)
 Aarne Ranta, Gothenburg (tbc)
 Josef Urban, Prague
