  We introduce a novel task consisting in assigning a proof to a given
mathematical statement. The task is designed to improve the processing of
research-level mathematical texts. Applying Natural Language Processing (NLP)
tools to research level mathematical articles is both challenging, since it is
a highly specialized domain which mixes natural language and mathematical
formulae. It is also an important requirement for developing tools for
mathematical information retrieval and computer-assisted theorem proving. We
release a dataset for the task, consisting of over 180k statement-proof pairs
extracted from mathematical research articles. We carry out preliminary
experiments to assess the difficulty of the task. We first experiment with two
bag-of-words baselines. We show that considering the assignment problem
globally and using weighted bipartite matching algorithms helps a lot in
tackling the task. Finally, we introduce a self-attention-based model that can
be trained either locally or globally and outperforms baselines by a wide
margin.
