Summary (Overview)

• ProofEvolve is a neuro-symbolic evolutionary framework for formal automated theorem proving in Lean 4, where neural models propose structural variations (decomposition, repair, schema recombination) and the Lean kernel verifies every proof transition.
• The framework introduces verified closure ($\rho$) as a kernel-grounded fitness measurement that ranks partial proofs by their verified progress, enabling graded selection rather than binary pass/fail feedback.
• Typed schema recombination enables verified sub-proofs to be extracted from one problem and reused across targets via a persistent, kernel-checked schema library, enabling recursive self-improvement.
• ProofEvolve achieves the highest average solve rate (57.8%) across three competition-level benchmarks (PutnamBench, IMO-LeanProofBench, CombiBench), outperforming LEAP (50.5%) and Hilbert (45.9%).
• On 744 unseen Lean Workbook theorems, the prover's own verified proofs add ~4 points over zero-shot, while random retrieval from the same library gives no improvement, demonstrating the value of verified knowledge inheritance.

---

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses a central limitation in automated theorem proving: existing neural provers do not fully preserve the recursive, self-improving structure of mathematical discovery. Key observations:

• Training-based systems (e.g., AlphaProof) store experience mainly in model parameters, requiring expensive retraining cycles before new results affect later problems.
• Agentic systems (e.g., LEAP, Hilbert) reuse information mainly within the current problem, with memory tied to the current target.
• Current systems focus primarily on whether the root theorem is solved, discarding useful structures from partial and unsuccessful attempts.

The authors draw an analogy to mathematical history: unsuccessful attempts (e.g., proving Euclid's parallel postulate) can lead to important discoveries (non-Euclidean geometry), and failed attempts at Hilbert's Entscheidungsproblem led to foundational results in theoretical computer science.

Theoretical Foundation

The work builds on three theoretical pillars:

1. Formal verification in Lean 4: Every accepted proof step is rigorously verified by the kernel, providing a reliable setting for cumulative evolution.

2. AND-OR proof DAGs: Proof attempts are represented as directed acyclic graphs where nodes are tactic states and hyperedges are proof constructors.

3. Quality-Diversity search (MAP-Elites): A behaviorally indexed archive preserves structurally diverse candidates while selection pressure is applied through fitness.

The paper positions ProofEvolve under Kautz's taxonomy as a Neuro[Symbolic] system, where the Lean kernel and verified closure operator are embedded in the neural generation process.

---

Methodology

Core Symbolic Structures

Lean verification: For a tactic state $s = (\Gamma \vdash g)$, the checked witnesses form:

$$\operatorname{Prf} _ {\mathcal{E}} (s) = \{p \mid \mathcal{E}; \Gamma \vdash_ {\mathcal{K}} p: g \}.\tag{1}$$

Proof DAGs: A proof attempt is a finite acyclic AND-OR proof DAG $D = (V, E, r)$ where each node is a tactic state. An accepted hyperedge $e = (s; s_1, \ldots, s_k)$ is a checked realizer:

$$F _ {e}: \prod_ {i = 1} ^ {k} \operatorname{Prf} _ {\mathcal{E}} (s _ {i}) \longrightarrow \operatorname{Prf} _ {\mathcal{E}} (s).\tag{2}$$

Closure and frontier: Closure is defined recursively:

$$\operatorname{Closed} _ {D} (s) \Longleftrightarrow \exists e \in \operatorname{out} _ {D} (s) \forall s ^ {\prime} \in \operatorname{ch} (e), \operatorname{Closed} _ {D} (s ^ {\prime}).\tag{3}$$

The open search boundary (frontier) is:

$$\operatorname{frontier} (D) = \{s \in V: \neg \operatorname{Closed} _ {D} (s), \operatorname{out} _ {D} (s) = \varnothing \}.\tag{4}$$

Neural Proof Proposal

The policy $\pi$ proposes edits to frontier states, and the kernel decides survival via the trusted transition operator:

$$\operatorname{step} _ {\mathcal{K}} (D, \delta) = \left\{ \begin{array}{l l} D ^ {\prime}, & \text{if Lean accepts the induced edge and} \\ & D ^ {\prime} \text{ is an acyclic extension of } D \\ \bot, & \text{otherwise.} \end{array} \right.\tag{7}$$

Three variation operators:

• Decomposition: Breaking a goal into smaller subgoals
• Repair: Fixing failed steps using Lean error messages
• Schema recombination: Applying library schemas to close goals

Verified Closure as Fitness

The fitness functional $\rho$ is defined by well-founded recursion over the acyclic DAG:

For a non-closing edge:

$$\rho_ {D} (e) = \sum_ {s ^ {\prime} \in \mathrm{ch} (e)} w _ {e} (s ^ {\prime}) \rho_ {D} (s ^ {\prime}).\tag{8}$$

For a state $s$:

$$\rho_ {D} (s) = \left\{ \begin{array}{l l} 1, & \text{Closed} _ {D} (s), \\ 0, & \text{out} _ {D} (s) = \varnothing, \\ \max _ {e \in \text{out} _ {D} (s)} \rho_ {D} (e), & \text{otherwise}, \end{array} \right.\tag{9}$$

Key property:

$$\rho(D) = 1 \Longleftrightarrow \operatorname{Closed} _ {D} (r).\tag{10}$$

Schema Extraction and Recombination

Schema extraction: Closed sub-DAGs are abstracted into reusable theorem schemas:

$$\ell : \forall \mathbf{x}, A _ {1} \rightarrow \dots \rightarrow A _ {m} \rightarrow C, \qquad \mathcal{E} \vdash_ {\mathcal{K}} \pi_ {\ell}: \ell .\tag{14}$$

Schema application: At an open state, a schema is applicable when a typed substitution makes its conclusion definitionally equal to the goal:

$$\mathsf {A p p} _ {\mathcal{L}} (s) = \{(\ell , \sigma): \operatorname{concl} (\ell) \sigma \equiv_ {\mathcal{E}} g \wedge \operatorname{Adm} _ {\Gamma} (\sigma) \}.\tag{16}$$

Theoretical Guarantees

Theorem 1 (Invariance of kernel-grounded state): Every finite execution preserves:

• (I1) Every accepted edge has a checked realizer
• (I2) Every closed node has a valid proof assembly
• (I3) Every library schema is kernel-verified

Corollary 1 (Validity of returned proofs): If ProofEvolve returns a proof, it type-checks against the standard axioms by construction.

---

Empirical Validation / Results

Main Results (Table 1)

Key Findings

1. Largest margin on IMO-LeanProofBench (53.3% vs. 36.7% for LEAP): Problems requiring proofs assembled from several lemmas benefit most from graded selection and schema reuse.

2. Verified closure dynamics: $\rho$ increases step-by-step as subgoals are verified, with solved runs reaching 1 and failed runs plateauing below.

3. Ablation study (60 IMO problems): Full system solves 32/60 on average; removing decomposition → 11, removing recombination → 14, removing repair → 9. All operators contribute more on the harder Advanced split.

4. Test-time budget scaling: 7 of 8 open-weight model configurations produce more kernel-verified transitions as budget grows, with monotonic increases in distinct targets solved.

5. Controlled compositional families: Growing library solves 19.8% vs. 7.3% with reset library (2.7× improvement).

6. Unseen Lean Workbook theorems: At K=8, the library raises solve rate from 49.5% to 53.4% (+3.9 points), while random retrieval reaches only 49.6%. In 91.7% of cases, accepted proofs do not reproduce any shown proof verbatim, confirming structural reuse rather than answer memorization.

---

Theoretical and Practical Implications

Theoretical Implications

1. Recursive self-improvement: ProofEvolve demonstrates a concrete mechanism for agents to accumulate formal knowledge over time without model retraining, addressing a fundamental challenge in AI-driven scientific discovery.

2. Graded feedback from binary verification: The verified closure functional $\rho$ shows how to extract meaningful, graded selection signals from the binary verdict of a formal kernel, enabling evolutionary search where verification is all-or-nothing.

3. Sound knowledge inheritance: The framework shows that verified partial structures can be safely transferred across problems while maintaining formal soundness, with Theorem 1 providing formal guarantees.

Practical Implications

1. Computational efficiency: By storing verified results as explicit schemas rather than model parameters, ProofEvolve avoids expensive retraining cycles and enables immediate reuse of proven results.

2. Scalability: The framework works with frozen base models (both proprietary and open-weight), making it deployable with frontier LLMs without fine-tuning.

3. Scientific discovery potential: The ability to accumulate verified knowledge across problems could accelerate discovery in mathematics and potentially extend to other scientific domains (theoretical physics, chemistry) where formal verification is applicable.

---

Conclusion

ProofEvolve introduces a neuro-symbolic evolutionary framework for formal automated theorem proving that achieves state-of-the-art results through three key innovations:

1. Verified closure as a kernel-grounded fitness measurement that enables graded selection on partial proofs
2. Typed schema recombination for cross-problem knowledge inheritance with formal soundness guarantees
3. Behaviorally indexed archives that preserve structural diversity during evolutionary search

The framework achieves the highest average solve rate (57.8%) across three competition-level Lean benchmarks and demonstrates that a library of the prover's own verified proofs adds ~4 points over zero-shot on unseen theorems, with random retrieval adding nothing.

Future directions include:

• Extending the framework to other scientific domains (theoretical physics, chemistry)
• Continual learning for AI-driven scientific discovery
• Scaling schema libraries and improving retrieval mechanisms
• Exploring the recursive self-improvement potential of verified knowledge accumulation

The work represents a concrete step toward recursively self-improving agents that accumulate formal knowledge over time, with formal guarantees of correctness maintained throughout the evolutionary process.