This session aims to connect a constellation of topics related to processing
corpora of mathematical texts. NLP on informal mathematical documents
presents many interesting challenges, and can be18.md aided by the presence of
corresponding formal documents (interpreted broadly). Creating and maintaining
these corpora presents even more challenges. We hope to bring together
researchers thinking about the retrieval, curation, and interpretation
of formal and informal mathematical texts, as well as the underlying languages used in these projects and the connections between them. There are many exciting projects underway in all of these areas, and a combined session will spur fruitful discussions and help to align the work of different groups.