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

DreamProver, developed by Youyuan Zhang and colleagues, introduces a novel agentic framework for formal theorem proving that evolves reusable lemma libraries through a wake-sleep program induction paradigm. Unlike existing approaches that rely on fixed lemma libraries or generate theorem-specific lemmas, DreamProver iteratively discovers and refines transferable lemmas. In the wake stage, it attempts to prove theorems from a training set using the current library while proposing new candidate lemmas. In the sleep stage, it abstracts, refines, and consolidates these candidates to compress and optimize the library, progressively evolving a compact set of high-level lemmas.

Experimental results show DreamProver substantially improves proof success rates across diverse mathematical benchmarks, while also producing more concise proofs and reducing computational cost. This approach addresses a key limitation in automated theorem proving: the lack of generality in lemma libraries. By enabling lemmas to transfer across related domains, DreamProver could accelerate formal verification in software engineering, mathematics, and AI safety, where rigorous proofs are critical.