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

arXiv:2604.26311v1 Announce Type: new Abstract: We introduce DreamProver, an agentic framework that leverages a "wakesleep" program induction paradigm to discover reusable lemmas for formal theorem proving.