# ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving

> ProofEvolve achieves 57.8% average solve rate on competition benchmarks by using kernel-verified closure as graded fitness and reusing proven proof schemas across problems.

- **Source:** [arXiv](https://arxiv.org/abs/2608.26334)
- **Published:** 2026-09-05
- **Permalink:** https://picx.dev/p/ZTwuSe
- **Whiteboard:** https://picx.dev/p/ZTwuSe/image

## Summary

## 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)

| Method | Putnam (%) | IMO-Lean (%) | Combi (%) | Avg. (%) |
|--------|-----------|--------------|-----------|----------|
| **Inference-only models** | | | | |
| Claude Haiku 4.5 | 0.0 | 0.0 | 3.3 | 1.1 |
| Claude Sonnet 4.6 | 0.0 | 0.0 | 6.7 | 2.2 |
| Claude Opus 4.8 | 0.0 | 0.0 | 10.0 | 3.3 |
| Gemini 3.1 Pro | 0.0 | 3.3 | 10.0 | 4.4 |
| DeepSeek-Prover-V2-671B | 7.0 | 0.0 | 10.0 | 5.7 |
| Goedel-Prover-V2-32B | 12.8 | 5.0 | 0.0 | 5.9 |
| GPT-5.5 | 10.0 | 5.0 | 13.0 | 9.3 |
| **Agentic systems** | | | | |
| ReAct (Claude Opus 4.8) | 35.0 | 15.0 | 27.0 | 25.7 |
| Aristotle (Claude Opus 4.8) | 45.0 | 13.3 | 40.0 | 32.8 |
| AxProver (Claude Opus 4.8) | 54.3 | 10.0 | 47.0 | 37.1 |
| Hilbert (Claude Opus 4.8) | 55.5 | 33.3 | 49.0 | 45.9 |
| LEAP (Claude Opus 4.8) | 64.7 | 36.7 | 50.0 | 50.5 |
| **Our work** | | | | |
| **ProofEvolve (Claude Opus 4.8)** | **71.2** | **53.3** | 49.0 | **57.8** |

### 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.

---

_Markdown view of https://picx.dev/p/ZTwuSe, served by PicX — AI-generated visual whiteboard summaries of research papers._