Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics
For researchers developing AI assistants for mathematics, this benchmark provides a controlled diagnostic task to evaluate source-grounded theorem retrieval, revealing a critical gap between retrieval and proof-gap sufficiency.
The paper introduces Re$^2$Math, a benchmark for evaluating theorem retrieval from partial mathematical proofs. The best system achieves only 7.0% ToolAcc, showing that current models often retrieve valid statements but fail to verify their applicability to the proof context.
Large language models are increasingly capable at closed-world mathematical reasoning, but research assistance also requires source-grounded use of the literature. When a proof reaches a non-trivial step, a useful assistant should determine whether the needed tool (e.g., a lemma) already exists, identify a suitable scholarly source, and verify that its assumptions align with the current proof context. To rigorously evaluate such capabilities, we introduce Re$^2$Math, a benchmark for tool-grounded retrieval from partial mathematical proofs. Each instance is built from a candidate instrumental citation in the proof of a main theorem, with hierarchical context and an optional leakage-controlled anchor hint. We also make the task source-grounded yet citation-agnostic in that any admissible theorem sufficient for the proof transition is accepted. Evaluation uses a release-frozen retrieval artifact, ensuring reproducibility, while the benchmark itself supports automatic, continual expansion with newly constructed instances. On the current benchmark test set, the best fixed-judge ToolAcc reaches 7.0%, despite substantially higher rates of source grounding, indicating that current systems often retrieve valid statements but fail to establish their applicability to the local proof step. By decoupling citation recall, grounding, and proof-gap sufficiency, Re$^2$Math transforms literature-grounded mathematical tool use into a controlled diagnostic task.