DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915966154178560 |
|---|---|
| author | Zhang, Youyuan Sun, Jialiang Bi, Hangrui Geng, Chuqin Ma, Wenjie Li, Zhaoyu Si, Xujie |
| author_facet | Zhang, Youyuan Sun, Jialiang Bi, Hangrui Geng, Chuqin Ma, Wenjie Li, Zhaoyu Si, Xujie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_26311 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent Zhang, Youyuan Sun, Jialiang Bi, Hangrui Geng, Chuqin Ma, Wenjie Li, Zhaoyu Si, Xujie Artificial Intelligence 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. |
| title | DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2604.26311 |