DreamProver：通过醒睡定理证明代理进化可迁移的引理库

本文提出 DreamProver，一种利用“醒 - 睡”程序归纳范式的智能体框架，旨在发现形式化定理证明中可复用的引理。现有方法要么依赖固定的引理库限制适应性，要么合成仅针对单个定理的特异性中间引理而缺乏通用性。DreamProver 通过迭代两阶段过程解决此问题：在“醒”阶段，利用当前引理库尝试证明训练集定理并提出新候选引理；在“睡”阶段，抽象、精炼并整合这些候选以压缩优化库。该交替循环使系统逐步进化出紧凑的高层可迁移引理集，显著提升数学基准测试的证明成功率，同时生成更简洁的证明并降低计算成本。