# Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 19 references that are in the map.
- First posted on arXiv 22 Jun 2026.

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

- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [UMAP: Uniform Manifold Approximation and Projection for Dimension Reduction](https://mlsanity.com/paper/1802.03426/) (2018)
- [Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models](https://mlsanity.com/paper/2506.05176/) (2025)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Llama-Embed-Nemotron-8B: A Universal Text Embedding Model for Multilingual and Cross-Lingual Tasks](https://mlsanity.com/paper/2511.07025/) (2025)
- [KaLM-Embedding: Superior Training Data Brings A Stronger Embedding Model](https://mlsanity.com/paper/2501.01028/) (2025)
- [KaLM-Embedding-V2: Superior Training Techniques and Data Inspire A Versatile Embedding Model](https://mlsanity.com/paper/2506.20923/) (2025)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [MIRB: Mathematical Information Retrieval Benchmark](https://mlsanity.com/paper/2505.15585/) (2025)

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

- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [Recipe-Matching, Not Equivalence](https://mlsanity.com/paper/2609.31927/) (2026)
- [Objects Without Morphisms: What LLMs for Mathematics Do Not Represent](https://mlsanity.com/paper/2610.03551/) (2026)

## Abstract (arXiv)

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 new resources related to formalization has increased the need for tools that enable efficient and 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 Mathematically Equivalent but Lexically Different Pairs (MELD) Dataset, a collection of mathematically equivalent statements that are 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.