Skip to content

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

🕒 Published (v1): 2026-04-29 05:35 UTC · Source: Arxiv · link

Why this paper was selected

Wake-sleep program induction discovers reusable lemma libraries for theorem proving

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

DreamProver is a wake-sleep agentic framework that builds a persistent, transferable lemma library for formal theorem proving in Lean. The wake stage proves training theorems via recursive decomposition; the sleep stage clusters intermediate results, abstracts generalizable lemmas, and prunes the library. Against the prior best agentic system (Hilbert), DreamProver achieves a 61% average gain in solved theorems while reducing token usage by 48% and proof length by 50%.

Problem

Existing LLM-based theorem provers treat each problem in isolation: fixed libraries lack adaptability, while per-problem intermediate lemmas never generalize. Approaches like LEGO-Prover maintain growing libraries but show no measurable cross-problem lemma reuse under controlled compute budgets. This wastes both computation and available mathematical structure when problems share subdomains.

Method

DreamProver iterates two stages, initialized with an empty lemma library \(L\):

Wake stage. For each training theorem \(P\), the system: 1. Attempts direct proof using \(L\) via LLM prompting. Success marks \(P\) as a learnable theorem. 2. On failure, performs recursive subgoal decomposition: generates a Lean proof sketch, extracts unproved sub-theorems (annotated sorry), reassembles the full proof for validity checking, and recursively decomposes sub-theorems.

Sleep stage. Given the set of collected intermediate theorems: 1. Lemma abstraction: annotate each theorem with an LLM-generated natural-language description (subdomain, difficulty, related theorems); embed with a sentence transformer; cluster via K-Means (elbow method for \(k\)); for each cluster, prompt an LLM to propose candidate lemmas; retain only those whose structural similarity to cluster members—computed via first-order logic expression trees and tree alignment—exceeds a threshold. 2. Library update: (i) remove least-recently-used lemmas when capacity exceeds ~100; (ii) deduplicate via tree edit distance; (iii) formally verify each candidate by prompting the LLM to prove it.

Inference. First attempts direct prompting with \(L\); if it fails, falls back to sketch-and-prove using \(L\) throughout.

Key Contributions

  • A wake-sleep cycle that converts per-problem LLM-derived sub-theorems into a persistent, compact, domain-specific lemma library with principled forgetting (LRU).
  • Semantic clustering + structural similarity validation for lemma abstraction, preventing degenerate or redundant abstractions.
  • Demonstration that 58% of learned lemmas transfer to unseen test problems, covering 71% of all successfully proved theorems—falsifying the claimed non-reuse of prior library-learning work.
  • Inference efficiency gains: 48% fewer output tokens and 50% shorter proofs versus the agentic SOTA (Hilbert).

Results

  • Overall vs. Hilbert (prior SOTA agentic system): +20% on inequalities, +114% on number theory, +50% on combinatorics → +61% average across domains.
  • 567NEQ (92 problems): DreamProver (Gemini 3.1 Pro) 62.0% vs. Hilbert (Gemini 3.1 Pro) 55.4%.
  • ChenNEQ (42): 85.7% vs. 73.8%.
  • MO-INT (20): 85.0% vs. 65.0%.
  • PutnamBench (66, number theory): 28.8% vs. 12.1%.
  • ProverBench (40): 62.5% vs. 40.0%.
  • CombiBench (43): 62.8% vs. 39.5%.
  • Token usage vs. Hilbert: −42%, −50%, −53% across three inequality domains; −48% average.
  • Proof length vs. Hilbert: −48%, −51%, −51%; −50% average.
  • Ablation (inequality domains): removing iterative refinement drops from 104 → 76 solved; removing cluster-based evolution drops to 53 solved; no library gives 55 solved; LEGO-Prover–style retrieval gives 61 solved.
  • Library statistics: 93/37/23 total lemma uses per domain; 35/29/19 distinct lemmas reused; 41/75/39 test theorems covered.

Limitations

  • Lemma libraries are domain-specific; a fresh training run is required for each new mathematical domain.
  • Evaluation relies on a fixed compute budget (pass@32, max 3 error-correction rounds); performance under significantly tighter budgets is not characterized separately.
  • The paper is a preprint under review; results use very recent proprietary models (GPT-5.3-Codex, Gemini 3.1 Pro) that are not widely reproducible externally.
  • The text is truncated before reporting results on underrepresented-domain generalization (RQ4) and geometry experiments.
  • Library capacity capped at ~100 lemmas; the sensitivity of this hyperparameter is not fully analyzed.

Relevance to Harnesses / Meta-Harnesses

DreamProver is a textbook meta-harness: it wraps an LLM prover inside an iterative outer loop that controls compute budgets (max proof attempts, error-correction rounds, decomposition depth), manages a persistent knowledge artifact (the lemma library), and orchestrates a multi-phase pipeline—decompose → embed → cluster → abstract → verify → prune. The wake-sleep cycle is structurally identical to a meta-harness that alternates between an exploration agent and a consolidation/distillation agent, with formal verification as an exit gate. For harness researchers, this demonstrates how domain-specific persistent state (a curated lemma library) can substitute for raw sampling compute, and how LRU forgetting and deduplication solve the context-window bottleneck that plagues naive retrieval-augmented harnesses. The 61%/48% gains over a strong agentic baseline quantify the return on meta-harness investment beyond single-pass LLM calls.