Author name: Youyuan Zhang, Jialiang Sun, Hangrui Bi, Chuqin Geng, Wenjie Ma, Zhaoyu Li, Xujie Si

arXiv:2604.26311v1 Announce Type: new
Abstract: 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 le…