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

1. Problem Statement

Automated theorem proving (ATP) has advanced significantly with Large Language Models (LLMs) and formal proof assistants like Lean. However, current state-of-the-art systems face two critical limitations:

• Lack of Generalization: Most approaches treat each theorem in isolation. While they may decompose problems into intermediate steps, these steps are often highly specific to the individual problem and do not generalize across different theorems.
• Inefficiency: Existing methods either rely on fixed, static lemma libraries (limiting adaptability) or synthesize new intermediate lemmas for every single problem instance. This leads to redundant computation, longer proof lengths, and higher token usage, as the system fails to accumulate and reuse "skills" (lemmas) learned from previous proofs.

The paper argues that current systems fail to mimic human mathematical practice, where mathematicians systematically accumulate, abstract, and reuse a core set of transferable lemmas to solve new problems efficiently.

2. Methodology: The DreamProver Framework

DreamProver is an agentic framework designed to learn and evolve a reusable library of lemmas through an iterative "Wake-Sleep" paradigm, inspired by cognitive learning theories and the DreamCoder algorithm. The system operates in alternating cycles:

A. The Wake Stage (Theorem Discovery & Decomposition)

In this phase, the agent attempts to prove theorems from a training set using the current lemma library.

• Learnable Theorem Identification: The system attempts to prove theorems directly using the library. If successful, the theorem is marked as "learnable," implying the library is sufficient for that domain.
• Intermediate Theorem Discovery: If a theorem cannot be proved directly, the system recursively decomposes it into simpler sub-problems (sub-theorems).
  • It generates a formal proof sketch.
  • It extracts unproven intermediate goals (marked by sorry) as standalone theorems.
  • It validates these extracted theorems by attempting to reassemble the full proof using the sketch and the new candidates.
• Outcome: The system accumulates a set of "learnable theorems" (intermediate results) derived from the training data.

B. The Sleep Stage (Lemma Abstraction & Library Optimization)

In this phase, the system processes the accumulated experiences to evolve the lemma library.

• Semantic Clustering: The system annotates the collected intermediate theorems with natural language descriptions (sub-domain, difficulty, relevant concepts). It then embeds these descriptions and clusters them using K-Means based on semantic similarity.
• Lemma Abstraction: For each cluster, an LLM is prompted to generate a candidate lemma that generalizes the specific theorems in that cluster.
• Structural Validation: To ensure the abstracted lemmas are applicable, the system computes the structural similarity (using tree edit distance on first-order logic expression trees) between the candidate lemma and the theorems in the cluster. Lemmas exceeding a similarity threshold are retained.
• Library Update (Forgetting & Deduplication):
  • Deduplication: New lemmas are compared against the existing library using tree edit distance; highly similar (duplicate) lemmas are discarded.
  • Forgetting: To maintain a compact library, the system employs a "Least Recently Used" (LRU) strategy. Lemmas that have not been used frequently in recent wake stages are pruned once the library reaches capacity.
  • Verification: Remaining candidate lemmas are formally verified to ensure they are provable.

C. Inference

During inference on unseen test problems, DreamProver utilizes the evolved library. It first attempts direct proof generation. If that fails, it employs a "Sketch-and-Prove" workflow, using the library to guide the generation of proof sketches and the solving of sub-goals.

3. Key Contributions

1. Wake-Sleep Paradigm for ATP: The first application of a continuous, iterative wake-sleep cycle specifically for evolving transferable lemma libraries in formal theorem proving.
2. Transferable Lemma Learning: Unlike previous works (e.g., LEGO-Prover) that struggled to demonstrate effective reuse, DreamProver explicitly clusters and abstracts intermediate results into general lemmas, creating a persistent, high-quality knowledge base.
3. Efficiency Mechanisms: The introduction of a "forgetting" mechanism (LRU pruning) and structural deduplication ensures the library remains compact (<100 lemmas), preventing context window overflow and maintaining high retrieval relevance.
4. Domain Generalization: The framework is designed to work across diverse mathematical domains, including those underrepresented in LLM training data.

4. Experimental Results

The authors evaluated DreamProver across five mathematical domains: Inequalities, Number Theory, Combinatorics, Plane Geometry, and Machine Learning Theory.

• Performance Gains:

  • DreamProver improved proof success rates by an average of 61% compared to prior state-of-the-art (SOTA) systems like Hilbert and Goedel-Prover-V2.
  • In specific domains, improvements were drastic: 114% in Number Theory and 50% in Combinatorics.
  • In underrepresented domains (Plane Geometry, ML Theory), DreamProver solved significantly more instances than proprietary LLMs (e.g., solving 14-16 Olympiad-level geometry problems where baseline LLMs solved 0-3).

• Efficiency and Quality:

  • Token Reduction: DreamProver reduced output token usage by 48% on average compared to SOTA agentic systems.
  • Proof Conciseness: Generated proofs were 50% shorter on average, indicating higher quality and better structure.
  • Lemma Reuse: Analysis showed that 58% of the lemmas generated during training were reused in test sets, contributing to 71% of all successfully proved theorems.

• Ablation Studies:

  • Removing the iterative wake-sleep refinement (single-pass evolution) dropped success rates significantly (from 104 to 76 solved problems).
  • Removing semantic clustering resulted in an oversized, unmanageable library, reducing performance even below a baseline without a library.

5. Significance

DreamProver represents a shift from "one-shot" or "static-library" theorem proving to continual, self-improving learning.

• Bridging the Gap: It effectively bridges the gap between the raw reasoning power of LLMs and the structured, reusable knowledge required for complex mathematical reasoning.
• Scalability: By learning a compact, transferable library, the system reduces the computational cost of proving new theorems, making high-level formal verification more accessible.
• Human-Like Learning: The framework mimics human cognitive processes (acquiring experience, abstracting principles, and forgetting irrelevant details), suggesting a viable path toward more robust and generalizable AI reasoning systems.

In conclusion, DreamProver demonstrates that explicitly learning and refining a library of reusable lemmas is a critical factor in achieving state-of-the-art performance in automated theorem proving, particularly in complex and data-scarce mathematical domains.