Retrieval-Augmented Language Models are Mimetic Theorem Provers

Abstract

Large language models have shown impressive capabilities in various mathematical tasks, yet they often struggle with rigorous, proof-based reasoning required for research-level mathematics. Retrieval-augmented generation presents a promising path to address this limitation. This paper systematically explores RAG for natural language theorem proving. We reveal that LLMs, when augmented with retrieved proofs, can function as powerful mimetic theorem provers: models can effectively generalize proof techniques from unstructured retrieved contexts to construct correct proofs for novel theorems. Building upon this insight, we introduce Dual RAG, a simple yet effective RAG framework that retrieves both relevant theorems and proof techniques. Dual RAG uses LLMs to identify the underlying reasoning challenges posed by theorems, enhancing both queries and document contexts to improve retrieval quality. Our experiments show that Dual RAG achieves substantial improvements in retrieval performance, with gains of up to 34.19%. Expert evaluations further confirm that these retrieval enhancements directly translate into higher quality proof generation. Notably, when integrated with the arXiv API, Dual RAG demonstrates the ability to prove research-level theorems in theoretical machine learning, highlighting its strong potential as a foundational element of a practical mathematical copilot.

Introduction

While recent large language models (LLMs) like OpenAI-o1 and DeepSeek-R1 have demonstrated strong performance on standard mathematical benchmarks, their capabilities in rigorous, proof-based reasoning remain limited. Proving a new theorem often requires specific "tricks" or techniques—such as the "subsequence trick" in probability—that are not explicitly stated in the theorem itself. Standard Retrieval-Augmented Generation (RAG) often fails in this domain because two theorems might be semantically similar in wording but require vastly different proof strategies.

This paper identifies a key property of LLMs: they are "mimetic theorem provers." When provided with a document showing a specific technique, these models can adapt the logical flow to solve a different problem. To leverage this, we propose Dual RAG, a framework designed to bridge the semantic gap between a theorem statement and the techniques required for its proof.

The Dual RAG Framework

Dual RAG improves upon standard retrieval systems through three core innovations:

1. LLM-Based Chunking: Rather than using arbitrary text splits, an LLM segments source material into logically coherent units, ensuring theorems, proofs, and remarks remain together.
2. Dual Augmentation: This process aligns the challenges of a query with the solutions in the context. An LLM analyzes the target theorem to generate a preliminary proof sketch (Query Augmentation), while the document database is pre-processed to extract key proof techniques and potential applications (Context Augmentation).
3. Zero-Shot Reranking: A high-capacity LLM ranks the top retrieved candidates based on their specific utility for the proof at hand.

Expand

Source, p. 4

Experimental Results

To evaluate Dual RAG, we introduced Exercise100, a benchmark consisting of 100 theorem-proving problems from graduate-level textbooks in Probability (PT), High-Dimensional Probability (HDP), Real Analysis (RA), and Topology (TP).

Retrieval Performance

Dual RAG significantly outperforms standard RAG baselines. As shown in the results table, it achieves retrieval coverage improvements ($\Delta_r$) of up to 34.19% over vanilla methods. By focusing on the "how" (techniques) rather than just the "what" (statements), Dual RAG successfully retrieves the necessary "gold contexts" required for complex proofs.

Expand

Source, p. 6

Generation and Research Utility

Expert evaluations confirm that improved retrieval leads to higher-quality proofs. For instance, on the Real Analysis subset, DeepSeek-R1's score improved from 80% to 90% when using Dual RAG. Furthermore, when integrated with the arXiv API, the system successfully generated a correct proof for a recently proposed open problem in theoretical machine learning regarding regret bounds in contextual bandits.

Conclusion

Dual RAG demonstrates that LLMs can effectively mimic and adapt complex mathematical reasoning when provided with the right context. While the system currently struggles with fundamentally new techniques not present in its library or extremely deep multi-layer dependencies, it represents a significant step toward practical mathematical copilots. Future work will explore tighter integration with formal verification tools like Lean or Coq to ensure absolute logical correctness.