# DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 39 of its 75 references that are in the map.
- First posted on arXiv 29 Apr 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [MPNet: Masked and Permuted Pre-training for Language Understanding](https://mlsanity.com/paper/2004.09297/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [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)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [LOTUS: Continual Imitation Learning for Robot Manipulation Through Unsupervised Skill Discovery](https://mlsanity.com/paper/2311.02058/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Top-Down Synthesis for Library Learning](https://mlsanity.com/paper/2211.16605/) (2022)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [QueST: Self-Supervised Skill Abstractions for Learning Continuous Control](https://mlsanity.com/paper/2407.15840/) (2024)
- [LILO: Learning Interpretable Libraries by Compressing and Documenting Code](https://mlsanity.com/paper/2310.19791/) (2023)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers](https://mlsanity.com/paper/2509.06493/) (2025)
- [Proving Theorems Recursively](https://mlsanity.com/paper/2405.14414/) (2024)
- [Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically](https://mlsanity.com/paper/2411.01829/) (2024)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)

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

- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [Continual Learning in Transition](https://mlsanity.com/paper/2608.06216/) (2026)
- [ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving](https://mlsanity.com/paper/2608.26334/) (2026)
- [Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification](https://mlsanity.com/paper/2610.09681/) (2026)
- [Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify](https://mlsanity.com/paper/2610.13632/) (2026)

## Abstract (arXiv)

We introduce DreamProver, an agentic framework that leverages a "wake-sleep" program induction paradigm to discover reusable lemmas for formal theorem proving. Existing approaches either rely on fixed lemma libraries, which limit adaptability, or synthesize highly specific intermediate lemmas tailored to individual theorems, thereby lacking generality. DreamProver addresses this gap through an iterative two-stage process. In the wake stage, DreamProver attempts to prove theorems from a training set using the current lemma library while proposing new candidate lemmas. In the "sleep" stage, it abstracts, refines, and consolidates these candidates to compress and optimize the library. Through this alternating cycle, DreamProver progressively evolves a compact set of high-level, transferable lemmas that can be effectively used to prove unseen theorems in related domains. Experimental results demonstrate that DreamProver substantially improves proof success rates across a diverse set of mathematical benchmarks, while also producing more concise proofs and reducing computational cost.