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

DreamProver：通过“唤醒-睡眠”定理证明智能体演化可迁移引理库

---

We introduce DreamProver, an agentic framework that leverages a “wake-sleep” program induction paradigm to discover reusable lemmas for formal theorem proving.

我们介绍了 DreamProver，这是一个利用“唤醒-睡眠”（wake-sleep）程序归纳范式来发现可重用引理，以进行形式化定理证明的智能体框架。

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.

DreamProver 通过一个迭代的两阶段过程解决了这一差距。在“唤醒”阶段，DreamProver 尝试使用当前的引理库证明训练集中的定理，同时提出新的候选引理。

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.

通过这种交替循环，DreamProver 逐步演化出一套紧凑的高级、可迁移引理，这些引理可以有效地用于证明相关领域中未见过的定理。

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.

实验结果表明，DreamProver 在多种数学基准测试中显著提高了证明成功率，同时生成了更简洁的证明并降低了计算成本。