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. NatFoM 2021, following a ifrst edition in 2020, addressed various aspects of naturalness in formal mathematics.
The workshop was held on Saturday, July 31st 2021. At the center stood an invited talk by Jeremy Avigad on “The design of mathematical language”. The workshop accepted 5 out of 8 submissions. These were presented in 30-minute talks with discussions.