  Mathematical text is written using a combination of words and mathematical
expressions. This combination, along with a specific way of structuring
sentences makes it challenging for state-of-art NLP tools to understand and
reason on top of mathematical discourse. In this work, we propose a new NLP
task, the natural premise selection, which is used to retrieve supporting
definitions and supporting propositions that are useful for generating an
informal mathematical proof for a particular statement. We also make available
a dataset, NL-PS, which can be used to evaluate different approaches for the
natural premise selection task. Using different baselines, we demonstrate the
underlying interpretation challenges associated with the task.

Computation and Language