Automated theorem proving offers a natural foundation for recursive self‑improvement in scientific discovery. Existing neural provers, however, fail to fully preserve this recursive structure—learning should become self‑enhancing over time. Current approaches either embed proof experience into model parameters via costly weight updates or keep verified intermediate deductions only within the current problem. Moreover, they heavily rely on sparse whole‑proof feedback, even when unsuccessful partial attempts contain useful insights.
To close this gap, we introduce ProofEvolve, a neuro‑symbolic framework that evolves explicit, formally verified symbolic proof structures, thereby decisively expanding the knowledge boundary. In the framework, a neural model proposes variation operators, including decompositions, repairs, and schema recombinations. Every proof transition is verified by the Lean kernel.
During evolution loops, ProofEvolve computes a verified closure over the resulting proof directed acyclic graphs (DAGs). For each problem, the system evolves partial AND‑OR proof DAGs in a behavior‑indexed archive; across problems, kernel‑checked schema extraction adds newly proved sub‑DAGs to a persistent schema library. Proof DAGs inherit solved results through typed schema recombination, while every residual premise is exposed as a new subgoal. This evolutionary process preserves verified results from incomplete attempts and makes them available for later proofs without weakening formal soundness.
Across three competition‑level Lean benchmarks, ProofEvolve achieves the highest average solve rate among the evaluated proof systems.
Blogger's Review: ProofEvolve cleverly combines the exploratory power of neural networks with Lean's formal guarantees, offering a sustainable way to accumulate proof knowledge. Its DAG‑driven evolution is especially promising for long‑term self‑improving scientific AI, and merits further exploration.