# Learning to Match Mathematical Statements with Proofs

arXiv: https://arxiv.org/abs/2102.02110 · HTML: https://mlsanity.com/paper/2102.02110/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 38 references that are in the map.
- First posted on arXiv 3 Feb 2021.

## Builds on (most cited first, 3 of 3)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Mathematical Language Processing Project](https://mlsanity.com/paper/1407.0167/) (2014)
- [POS Tagging and its Applications for Mathematics](https://mlsanity.com/paper/1406.2880/) (2014)

## Built on by (most cited first, 2 of 2)

- [BERT is not The Count: Learning to Match Mathematical Statements with Proofs](https://mlsanity.com/paper/2302.09350/) (2023)
- [A Survey in Mathematical Language Processing](https://mlsanity.com/paper/2205.15231/) (2022)

## Abstract (arXiv)

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.