Mathematics Modulo Equivalence: Theorem Classes as Retrieval Supervision

The same theorem can be stated in very different mathematical language. Cayley–Hamilton, for instance, can be phrased through the annihilator ideal of an operator or as a linear recurrence along its orbits. Text embedders often fail to retrieve one such formulation from the other, and retrieval datasets rarely record which statements are equivalent, so contrastive training can push equivalent statements apart as negatives. We build Different but Equivalent (DBE), a dataset organized around reviewed theorem classes: 3,000 anchor theorems, 9,385 equivalent formulations in 18,770 wordings, and 62,514 search queries linked to their targets. Class membership tells the contrastive loss which other statements are also correct answers. For formal retrieval, we pair 235,930 Mathlib declarations with natural-language search queries, each written by a language model for its declaration, and link 1,447 DBE anchors to declarations. On Qwen3-Embedding-8B, one LoRA trained on DBE, Lean declaration lookup, and premise retrieval, with scores distilled from relation-specific specialists, reaches 57.15 macro nDCG@10 on 13 MIRB tasks, against 53.10 for the base model and 53.98 for MathLeap-Qwen-8B. Removing DBE from this recipe lowers MELD full MRR by 8.93 points but the MIRB average by only 0.18. Matched controls trained without teacher scores, at 8B and on Qwen3-Embedding-0.6B, come within 0.28 points of the distilled models on broad averages, so most of the broad gain comes from the multi-relation training data rather than from distillation.