NatFoM 2025: Workshop on Natural Formal Mathematics

In (pure) mathematics there has always been a strong informal sense of “naturality” of topics and methods. Generally, “natural” theories, notions, properties, or proofs are preferred over technical, convoluted, or counterintuitive approaches. If formal mathematics is to become part of mainstream mathematics, its formalizations and usage have to become more “natural”, and thus closer to informal mathematics.

This workshop broadly addresses the issue of naturality in formal mathematics. It will take place in the context of the CICM conference, tentatively on Monday, Oct. 6, 2025 (to be confirmed). We plan to hold open discussions on naturalness in formal mathematics.

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

• The notion of naturality in mathematics generally
• Natural mathematical language
• Translations between informal and formal mathematics using statistical or symbolic techniques
• Natural input and output languages for formal mathematics systems
• Controlled natural languages (CNL) for mathematics
• Making formal mathematics documents readable
• Naturality of foundational theories (type theory, set theory, HOL, etc.)
• Naturality of proof methods
• Natural proof structures and granularities
• Natural structurings of formalized mathematical texts and libraries
• Mathematical typesetting (LaTeX) and formal mathematics
• Natural formalizations

Previous instances of the workshop: 2020 | 2021 | 2023

Call for abstracts

We invite you to submit extended abstracts or demonstration proposals (up to 500 words).

At least one author of each accepted extended abstract or demonstration proposal is expected to attend NatFoM and present their submission in person. Accepted abstracts will be made available online. Accepted abstracts can optionally be extended to a full paper (5–15 pages) after the workshop. We are considering publication on CEUR-WS, so please use their LaTeX format.

Please send your abstract/demonstration proposal as a PDF via email to both Frederik (jan.frederik.schaefer@fau.de) and Marcel (marcel.schuetz@fau.de).

Rolling submission until September 7 (earlier submissions will receive earlier notifications).

Program Committee:

• Adrian De Lon, Bonn, Germany (co-chair)
• Peter Koepke, Bonn, Germany (co-chair)
• Marcel Schütz, Erlangen, Germany (co-chair)
• Jan Frederik Schaefer, Erlangen, Germany (co-chair)
• TBD