Retrieval-Augmented Language Models are Mimetic Theorem Provers (2025)

Abstract: Large language models have demonstrated considerable capabilities in various mathematical tasks, yet they often fall short in rigorous, proof-based reasoning essential for research-level mathematics. Retrieval-augmented generation presents a promising direction for enhancing these capabilities. This paper systematically explores RAG for natural language theorem proving, revealing that LLMs, when augmented with retrieved proofs rather than just theorems, can function as potent mimetic theorem provers: these models can effectively generalize proof techniques found in unstructured retrieved contexts to construct correct proofs for novel theorems. Building upon this finding, we introduce Dual RAG, a simple yet effective RAG framework. Dual RAG employs LLMs to identify underlying reasoning challenges within theorems, augmenting both queries and document contexts to improve retrieval performance. 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 for a practical mathematical copilot.

## problem statement in this paper, we study the task of natural language theorem proving with unstructured context. formally, given a target theorem foot_0 t , the goal is to generate a valid proof by leveraging a collection of potentially relevant documents @xmath0, d 2 , • • • , d n }, where each d i may be a theorem-related textbook or research paper. to construct the proof, the system must first retrieve a set of chunks c @xmath1, c 2 , ..., c n } from these documents, where each chunk c i ⊆ d j for some @xmath2. our setting differs from the classic premise selection task @xcite @xcite in important ways. while typical premise selection works with clean, pre-separated mathematical statements (usually from structured theorem libraries), we aim to handle raw documents where mathematical content appears alongside explanations, examples, and discussion. this better reflects how mathematicians actually work -they usually develop proofs by working with complete papers or books, instead of isolated formal statements. ## methodology to optimize retrieval performance in natural language theorem proving with unstructured data, we introduce dual rag, a simple yet effective rag framework. our method employs dual data augmentation to align target theorems with their relevant context in the embedding space. we meticulously develop a complete retrieval pipeline for our task, from chunking to reranking. we systematically introduce our framework in this section. ## experiments in this section, we conduct extensive experiments to study the task of natural language theorem proving with unstructured context. specifically, we aim to answer the following research questions: ## conclusion in this paper, we study the task of natural language theorem proving with unstructured context. this setting is both practical and important for building a mathematical copilot. we observe that advanced llms exhibit strong mimetic capabilities in such scenarios. this insight suggests that effective retrieval should involve both related theorems and relevant proof techniques for each target theorem. motivated by domain knowledge, we propose dual rag, a rag system that dually augments the target theorem and its context with llm-generated analyses. these analyses highlight the difficulties of the target theorem and suggest potential applications of the context, bringing semantically aligned query-context pairs closer and improving retrieval quality. this in turn leads to better proof generation on our graduate-level dataset, exercise100. we further integrate dual rag with the arxiv api to address research-level problems in theoretical machine learning. remarkably, we identify a case where an llm, given the right context, successfully solves an unpublished research problem. while current models remain limited in their ability to tackle novel theorems requiring fundamentally new techniques, our work represents a meaningful step toward building a practical mathematical copilot.