Does My Embedding Reflect That \(A = B\)? Evaluating Mathematical Equivalence in Embedding Models

Because mathematics is highly abstract, a single statement can take very different forms depending on what subfield it is framed in. There are many examples where breakthroughs occurred after researchers discovered that a question had already been answered in a different field. At the same time, the growth of resources related to formalization has increased the need for tools that enable efficient, reliable navigation between mathematical `languages’ (e.g., from Lean to natural language). In this paper, we investigate whether current embedding models capture mathematical equivalence. To do this, we introduce the \emph{Mathematically Equivalent but Lexically Different Pairs (MELD) Dataset}, a collection of mathematically equivalent statements expressed in very different language. We show that current state-of-the-art embedding models tend to group statements by the terminology used to make them instead of the underlying math. Motivated by this, we propose a contrastive approach to learning embeddings of mathematical text that focuses on aligning informal statements with different formalizations. Our experiments demonstrate that this leads to improvements not only on informal-formal retrieval tasks but also on MELD, which only contains natural language statements.