# DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 33 of its 60 references that are in the map.
- First posted on arXiv 12 Oct 2025.

## Builds on (most cited first, 30 of 33)

- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Self-RAG: Learning to Retrieve, Generate, and Critique through Self-Reflection](https://mlsanity.com/paper/2310.11511/) (2023)
- [M3-Embedding: Multi-Linguality, Multi-Functionality, Multi-Granularity Text Embeddings Through Self-Knowledge Distillation](https://mlsanity.com/paper/2402.03216/) (2024)
- [Precise Zero-Shot Dense Retrieval without Relevance Labels](https://mlsanity.com/paper/2212.10496/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Large Language Models for Mathematical Reasoning: Progresses and Challenges](https://mlsanity.com/paper/2402.00157/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Query2doc: Query Expansion with Large Language Models](https://mlsanity.com/paper/2303.07678/) (2023)
- [RQ-RAG: Learning to Refine Queries for Retrieval Augmented Generation](https://mlsanity.com/paper/2404.00610/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [RL on Incorrect Synthetic Data Scales the Efficiency of LLM Math Reasoning by Eight-Fold](https://mlsanity.com/paper/2406.14532/) (2024)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [RichRAG: Crafting Rich Responses for Multi-faceted Queries in Retrieval-Augmented Generation](https://mlsanity.com/paper/2406.12566/) (2024)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [Theorem Prover as a Judge for Synthetic Data Generation](https://mlsanity.com/paper/2502.13137/) (2025)

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

- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees](https://mlsanity.com/paper/2604.19000/) (2026)
- [What are the Right Symmetries for Formal Theorem Proving?](https://mlsanity.com/paper/2605.22257/) (2026)
- [MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement](https://mlsanity.com/paper/2608.14221/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)

## Abstract (arXiv)

Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathematical knowledge and its corresponding formal representation in languages like Lean. Current retrieval-augmented autoformalization methods query external libraries using the informal statement directly, but overlook a fundamental limitation: informal statements lack direct mappings to mathematical theorems and lemmata, nor do those theorems translate trivially into the formal primitives of languages like Lean. To address this, we introduce DRIFT, a novel framework that enables LLMs to decompose informal mathematical statements into smaller, more tractable "sub-components". This facilitates targeted retrieval of premises from mathematical libraries such as Mathlib. Additionally, DRIFT retrieves illustrative theorems to help models use premises more effectively in formalization tasks. We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval, nearly doubling the F1 score compared to the DPR baseline on ProofNet. Notably, DRIFT demonstrates strong performance on the out-of-distribution ConNF benchmark, with BEq+@10 improvements of 42.25% and 37.14% using GPT-4.1 and DeepSeek-V3.1, respectively. Our analysis shows that retrieval effectiveness in mathematical autoformalization depends heavily on model-specific knowledge boundaries, highlighting the need for adaptive retrieval strategies aligned with each model's capabilities.