ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving

# ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
Source: [https://arxiv.org/html/2608.26334](https://arxiv.org/html/2608.26334)
Ziwei GuanAffiliation:Meta AICore contributorsEric XieAffiliation:University of VirginiaBohan LiuAffiliation:University of VirginiaShivani ModiAffiliation:Meta AIBuyun ZhangAffiliation:Meta AIEllie Dingqiao WenAffiliation:Meta AIHenry KautzAffiliation:University of VirginiaAidong ZhangAffiliation:University of Virginia

###### Abstract

Automated theorem proving offers a natural foundation for recursive self\-improvement in scientific discovery\. However, existing neural provers do not fully preserve this recursive structure, where the learning process should be self\-improving over time\. Existing methods either embed proof experience into model parameters through expensive weight updates, or keep verified intermediate deductions only within the current problem\. In addition, these methods also heavily rely on sparse whole\-proof feedback, even when unsuccessful partial attempts contain useful discoveries\. To close the gap, we proposeProofEvolve, aneuro\-symbolicframework that evolves explicit, formally verifiedsymbolicproof structures withneuralmodels to decisively expand the knowledge boundary\. In this framework, the neural model proposes variation operators, including decompositions, repairs, and schema recombinations\. The symbolic Lean kernel verifies every proof transition\. Over the evolution loops, ProofEvolve computes verified closure over the resulting proof directed acyclic graphs \(DAGs\)\. Within each problem, ProofEvolve evolves partial AND\-OR proof DAGs in a behaviorally indexed archive\. Across problems, kernel\-checked schema extraction adds newly proved sub\-DAGs to a persistent schema library\. Proof DAGs inherit the solved results through typed schema recombination, with every residual premise 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\.

††date:August 10, 2026††correspondence:Wenqian Ye and Aidong Zhang at[\{wenqian, aidong\}@virginia\.edu](mailto:[email protected],[email protected])## 1Introduction

Theorem proving paves the way for scientific reasoning to discover new knowledge with formal guarantee of correctness\. A proof often contributes more than its stated conclusion\. It can produce reusable lemmas, reveal hidden structures, and expose new hypotheses\. Even unsuccessful proof programs can push forward important advances\. For centuries, mathematicians attempted to deriveEuclid’s parallel postulatefrom his remaining axioms\. Examining geometries in which the postulate does not hold instead led to the development of non\-Euclidean geometry\([Bonola, 1955](https://arxiv.org/html/2608.26334#bib.bib6)\)\. A similar pattern is in theoretical computer science \(TCS\)\. Hilbert’sEntscheidungsproblemasked whether a general procedure could determine the validity of any statement in first\-order logic\([Hilbert and Ackermann, 1928](https://arxiv.org/html/2608.26334#bib.bib16)\)\. Following the unsolved problem, Church and Turing proved that no such general procedure exists\([Church, 1936](https://arxiv.org/html/2608.26334#bib.bib9);[Turing, 1937](https://arxiv.org/html/2608.26334#bib.bib46)\)\. Turing’s analysis also introduced a formal model of computation that later became the foundation of TCS\. Therefore, proofs fundamentally convert individual results into reusable knowledge that supports later discoveries\.

Figure 1:Overview of ProofEvolve\.Within a target, a proof DAG archive preserves structurally diverse candidates and ranks them by verified closureρ\\rho, computed from kernel\-accepted subgoals\. Across targets, checked extraction adds newly proved results to a persistent schema library, and typed recombination instantiates them in later DAGs while exposing all residual premises as subgoals\.Recently, AI systems have begun to automate parts of scientific discovery\. Trained neural models with automatic evaluation have produced new algorithms, mathematical constructions, and structural patterns\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib39);[Novikov et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib31);[Davies et al\., 2021](https://arxiv.org/html/2608.26334#bib.bib10)\)\. Evolutionary search is also promising as it can improve candidates over time through repeated generation, evaluation, and selection\. However, current linguistic\-based neural theorem provers still heavily use a small part of the verified structure\. Training\-based systems store experience mainly in model parameters, so new results affect later problems only after another training cycle\([Hubert et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib17);[Ren et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib38);[Lin et al\., 2025b](https://arxiv.org/html/2608.26334#bib.bib25)\)\. Agentic systems leverage multi\-agent collaboration to work on problems with subgoals during inference\([Jiang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib19);[Varambally et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib47)\)\. One latest work, LEAP\([Kung et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib22)\), also shares intermediate lemmas across branches of a proof DAG, but this memory remains tied to the current target\. Thus, current systems still focus mainly on whether the root theorem is solved\.

Formal theorem proving in Lean 4\([de Moura and Ullrich, 2021](https://arxiv.org/html/2608.26334#bib.bib11)\)provides a reliable setting for cumulative evolution because every accepted proof step is rigorously verified\. However, current neural theorem provers do not fully preserve verified progress\. Training based methods store experience mainly in model parameters\([Hubert et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib17);[Ren et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib38);[Lin et al\., 2025b](https://arxiv.org/html/2608.26334#bib.bib25)\), while agentic methods reuse information mainly within the current problem\([Jiang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib19);[Varambally et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib47);[Kung et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib22)\)\. As a result, useful structures from partial and completed proofs are rarely inherited across searches\. This is a central limitation for evolutionary search, which requires useful structures to survive unsuccessful candidates and pass to later generations\. A small textual mutation may invalidate a complete proof even when much of its verified argument remains correct\([Nagashima, 2019](https://arxiv.org/html/2608.26334#bib.bib30)\)\. A self\-improving prover should therefore evolve verified partial structures rather than complete proof texts alone and preserve them for recombination across problems\.

To address these shortcomings, we proposeProofEvolve, a neuro\-symbolic evolutionary framework in which improvement grows in an explicit body of verified symbolic structures with neural proposals\. As shown in Figure[1](https://arxiv.org/html/2608.26334#S1.F1), ProofEvolve grows a proof DAG for each theorem through kernel\-verified transitions\. At each step the language model proposes a decomposition, repair, or schema recombination, and Lean 4 kernel accepts or rejects it\. A behaviorally indexed archive\([Mouret and Clune, 2015](https://arxiv.org/html/2608.26334#bib.bib29)\)keeps structurally diverse partial proofs and ranks them by*verified closure*, a kernel\-grounded score that aggregates proved subgoals through the AND\-OR structure, so selection acts on graded progress rather than a single pass\-or\-fail verdict\. Across problems, ProofEvolve extracts closed sub\-DAGs as theorem schemas\. Typed recombination later instantiates a schema at a matching goal, exposes any remaining premises as new subgoals, and re\-checks the result with the kernel\. Verified results from earlier problems therefore enlarge the reachable search space of later ones\.

To show the effectiveness, we evaluate our framework on three competition\-level benchmarks, PutnamBench, IMO\-LeanProofBench, and CombiBench, with a frontier LLM \(Claude Opus 4\.8\) as the base model under matched per\-target budgets, and on a disjoint Lean Workbook split with the frontier open\-weight model Qwen3\.5\-397B\-A17B\-FP8\. ProofEvolve achieves an average solve rate of57\.8%57\.8\\%, compared with50\.5%50\.5\\%for LEAP and45\.9%45\.9\\%for Hilbert\. Ablation and test\-time scaling studies further analyze the method’s components and its behavior as the per\-target budget grows\. A separate evaluation isolates the library itself: on744744Lean Workbook theorems disjoint from the9,9689\{,\}968\-theorem source stream,5,5465\{,\}546of the prover’s own kernel\-checked proofs improve the solve rate by about four points over zero\-shot, whereas random retrieval from the same library gives no improvement\.

In summary, our main contributions are as follows:

- ∙\\bulletWe formulate theorem proving as an evolution process over structured symbolic knowledge with persistent inheritance through a Lean\-verified theorem schema library, where the neural models propose new directions to extend the knowledge boundary\.
- ∙\\bulletWe introduce verified closure as a kernel\-grounded fitness measurement and typed schema recombination as a mechanism to enable verified subproofs across targets\.
- ∙\\bulletExtensive experiments on ProofEvolve against state\-of\-the\-art neural models and agentic baselines on three competition\-level Lean benchmarks show the significant effectiveness of the proposed framework, and on744744Lean Workbook theorems disjoint from its library the prover’s own verified proofs add about four points over zero\-shot, while random retrieval from the same library adds nothing\.

## 2Related Work

### 2\.1Neural theorem provers

Neural theorem provers train an LLM policy to propose tactics or complete proofs in a formal language\. GPT\-f\([Polu and Sutskever, 2020](https://arxiv.org/html/2608.26334#bib.bib35)\)and PACT\([Han et al\., 2021](https://arxiv.org/html/2608.26334#bib.bib15)\)established language\-model policies for tactic generation\. Other works\([Yang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib52);[Lample et al\., 2022](https://arxiv.org/html/2608.26334#bib.bib23);[Xin et al\., 2025a](https://arxiv.org/html/2608.26334#bib.bib50);[Xin et al\., 2025b](https://arxiv.org/html/2608.26334#bib.bib51)\)combine learned proposals with retrieval or tree search\. Recent systems obtain stronger policies from synthetic proofs, supervised fine\-tuning, and reinforcement learning\([Ren et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib38);[Lin et al\., 2025b](https://arxiv.org/html/2608.26334#bib.bib25);[Wang et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib49);[ByteDance Seed, 2025](https://arxiv.org/html/2608.26334#bib.bib8);[Ji et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib18)\)\. AlphaProof\([Hubert et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib17)\)trains at scale on kernel\-checked self\-generated experience and performs test\-time adaptation on difficult targets\. Retrieval\-augmented provers reuse existing library lemmas at inference time\([Shen et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib40)\), while self\-play systems learn from both successful and failed proof trees\([Poesia et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib34)\)\. ProofEvolve instead keeps the model fixed and stores newly proved results as explicit, verified schemas\.

### 2\.2Agentic theorem provers

Agentic systems use multiple language models to structure proof search through decomposition, retrieval, and verifier feedback\. Draft\-Sketch\-Prove\([Jiang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib19)\)turns informal arguments into formal sketches\. COPRA\([Thakur et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib41)\)constructs proofs through repeated tactic execution\. Hilbert\([Varambally et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib47)\)recursively decomposes difficult goals and repairs failed proofs, while LEAP\([Kung et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib22)\)uses an AND\-OR proof DAG to share intermediate lemmas across branches\. AlphaProof Nexus\([Tsoukalas et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib45)\)applies compiler\-guided agents to research problems, while AlphaGeometry\([Trinh et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib43)\)combines neural proposals with symbolic deduction in geometry\. These methods strengthen search within a target\. In contrast, ProofEvolve additionally extracts verified sub\-DAGs for reuse across targets, which enables the framework the ability to recursively evolve\.

### 2\.3Symbolic knowledge evolution

Evolutionary program search, including FunSearch\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib39)\)and AlphaEvolve\([Novikov et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib31)\), alternates language model generation with automatic evaluation and selection, while MAP\-Elites preserves diverse high quality candidates across behavioral niches\([Mouret and Clune, 2015](https://arxiv.org/html/2608.26334#bib.bib29)\)\. LEGO\-Prover expands a lemma library\([Wang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib48)\), although storage alone does not guarantee reuse\([Berlot\-Attwell et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib5)\)\. DreamProver is closest to our setting because it keeps the model fixed and builds a transferable Lean library through wake sleep abstraction\([Zhang et al\., 2026](https://arxiv.org/html/2608.26334#bib.bib57);[Ellis et al\., 2021](https://arxiv.org/html/2608.26334#bib.bib12)\)\. Other methods retrain a retriever\([Kumarappan et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib21)\), distill proof strategies\([Fang et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib13)\), or modify agent code using empirical fitness\([Zhang et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib56)\)\. Formal proof evolution is difficult because verification is binary and small edits can invalidate useful candidates\([Nagashima, 2019](https://arxiv.org/html/2608.26334#bib.bib30)\)\. ProofEvolve instead combines verified closure and typed schema recombination in a single inference time process\. Partial proof DAGs are selected through kernel accepted subgoals, while newly closed sub\-DAGs become schemas reused in later candidates without modifying the model\. Under Kautz’s taxonomy on Neural Symbolic AI\([Kautz, 2022](https://arxiv.org/html/2608.26334#bib.bib20)\), ProofEvolve is aNeuro\[Symbolic\]system where the Lean kernel and verified closure operator are embedded in the neural generation process to recursively improve over time\.

## 3Preliminaries

We first define the symbolic structures on which ProofEvolve operates\. Every state is a Lean 4 artifact, and the search retains each partial result rather than discarding it\. A closed fragment of an attempt is a valid, reusable result even before the attempt closes its root goal \(Eq\. \([5](https://arxiv.org/html/2608.26334#S3.E5)\)\)\. This property is what later lets the search accumulate and transfer verified work \(Section[4](https://arxiv.org/html/2608.26334#S4)\)\.

#### Lean verification\.

We work in a fixed Lean 4 environmentℰ\\mathcal\{E\}that imports a matched Mathlib version\([The mathlib Community, 2020](https://arxiv.org/html/2608.26334#bib.bib42)\)\. We writeℰ;Γ⊢𝒦p:g\\mathcal\{E\};\\Gamma\\vdash\_\{\\mathcal\{K\}\}p:gwhen the termppelaborates under local contextΓ\\Gamma\. It contains no unresolved metavariables or placeholders, and is accepted at typeggby Lean’s kernel𝒦\\mathcal\{K\}\. A tactic state iss=\(Γ⊢g\)s=\(\\Gamma\\vdash g\)\([Polu and Sutskever, 2020](https://arxiv.org/html/2608.26334#bib.bib35);[Yang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib52)\), and its checked witnesses form

𝖯𝗋𝖿ℰ\(s\)=\{p∣ℰ;Γ⊢𝒦p:g\}\.\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\)=\\\{p\\mid\\mathcal\{E\};\\Gamma\\vdash\_\{\\mathcal\{K\}\}p:g\\\}\.\(1\)We writeu≡ℰvu\\equiv\_\{\\mathcal\{E\}\}vfor definitional equality inℰ\\mathcal\{E\}, let𝖳𝗁𝗆⁡\(ℰ\)\\mathsf\{Thm\}\(\\mathcal\{E\}\)denote the theorem declarations imported intoℰ\\mathcal\{E\}, and call a targetTT*well\-formed*whenℰ;∅⊢𝒦T:𝖯𝗋𝗈𝗉\\mathcal\{E\};\\varnothing\\vdash\_\{\\mathcal\{K\}\}T:\\mathsf\{Prop\}\.

#### Reusable proof structures\.

For awell\-formedtargetTT, a proof attempt is a finite acyclic AND\-OR proof DAGD=\(V,E,r\)D=\(V,E,r\)with rootr=\(Γ0⊢T\)r=\(\\Gamma\_\{0\}\\vdash T\), where each node is a tactic state\. An accepted hyperedgee=\(s,s1,…,sk\)e=\(s;s\_\{1\},\\ldots,s\_\{k\}\)is one Lean\-elaborated proof constructor from the child obligations to the source obligation, i\.e\., a checked realizer

Fe:∏i=1k𝖯𝗋𝖿ℰ​\(si\)⟶𝖯𝗋𝖿ℰ​\(s\)\.F\_\{e\}:\\prod\_\{i=1\}^\{k\}\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\_\{i\}\)\\longrightarrow\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\)\.\(2\)Fork=0k=0, the empty product is the singleton\{⋆\}\\\{\\star\\\}andFe​\(⋆\)∈𝖯𝗋𝖿ℰ​\(s\)F\_\{e\}\(\\star\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\)is a checked closing witness\. Multiple edges leavingssare alternative proof steps, whereas the children of a single edge must all be discharged\. For DAGs sharing a root, we writeD⪯D′D\\preceq D^\{\\prime\}whenV⁡\(D\)⊆V⁡\(D′\)V\(D\)\\subseteq V\(D^\{\\prime\}\),E⁡\(D\)⊆E⁡\(D′\)E\(D\)\\subseteq E\(D^\{\\prime\}\), and all existing node labels and edge realizers are preserved, and we callD′D^\{\\prime\}an*extension*ofDD\.

LetoutD​\(s\)\\mathrm\{out\}\_\{D\}\(s\)be the accepted edges leavingssandch⁡\(e\)\\mathrm\{ch\}\(e\)be their children\. SinceDDis acyclic, closure is well defined by

ClosedD​\(s\)⟺∃e∈outD​\(s\)​∀s′∈ch⁡\(e\),ClosedD​\(s′\)\.\\mathrm\{Closed\}\_\{D\}\(s\)\\Longleftrightarrow\\exists e\\in\\mathrm\{out\}\_\{D\}\(s\)\\;\\forall s^\{\\prime\}\\in\\mathrm\{ch\}\(e\),\\ \\mathrm\{Closed\}\_\{D\}\(s^\{\\prime\}\)\.\(3\)The universal condition is vacuous for a checked closing edge\. For each closedss, we fix one witnessing edgewinD​\(s\)\\mathrm\{win\}\_\{D\}\(s\), and the constructions below hold for any such choice\. The open search boundary is

frontier\(D\)=\{s∈V:¬ClosedD\(s\),outD\(s\)=∅\}\.\\mathrm\{frontier\}\(D\)=\\\{s\\in V:\\neg\\mathrm\{Closed\}\_\{D\}\(s\),\\ \\mathrm\{out\}\_\{D\}\(s\)=\\varnothing\\\}\.\(4\)WritingwinD​\(s\)=\(s,s1,…,sk\)\\mathrm\{win\}\_\{D\}\(s\)=\(s;s\_\{1\},\\ldots,s\_\{k\}\)and taking the empty tuple to be⋆\\star, proof assembly is the recursion

AsmD​\(s\)=FwinD​\(s\)​\(\(AsmD​\(si\)\)i=1k\)\.\\mathrm\{Asm\}\_\{D\}\(s\)=F\_\{\\mathrm\{win\}\_\{D\}\(s\)\}\\left\(\(\\mathrm\{Asm\}\_\{D\}\(s\_\{i\}\)\)\_\{i=1\}^\{k\}\\right\)\.\(5\)Acyclicity makes this recursion well founded, and Eq\. \([2](https://arxiv.org/html/2608.26334#S3.E2)\) givesAsmD​\(s\)∈𝖯𝗋𝖿ℰ​\(s\)\\mathrm\{Asm\}\_\{D\}\(s\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\): a closed internal sub\-DAG is a typed result, reusable while its root remains open\.

## 4Neuro\-Symbolic Evolution for Formal Automated Theorem Proving

### 4\.1Overview

Figure[1](https://arxiv.org/html/2608.26334#S1.F1)shows the ProofEvolve pipeline\. A neural language model proposes structural variations, the Lean kernel checks every proof transition and schema application, and the search keeps the checked structures that make the most verified progress\.*Verified closure*\(Sec\.[4\.2](https://arxiv.org/html/2608.26334#S4.SS2.SSS0.Px1)\) turns the kernel’s binary verdict into a graded fitness read off the proof DAG, so two unfinished attempts can still be ranked\.*Schema recombination*\(Sec\.[4\.3](https://arxiv.org/html/2608.26334#S4.SS3)\) carries a verified result from one proof into another as a single kernel\-checked step\. Within one target, a*proof DAG archive*stores candidate proofs; across targets, a*schema library*stores proved results\. Schema extraction adds results to the library, and schema recombination applies them in later DAGs\.

ProofEvolve separates neural proposal from symbolic state transition\. The policyπ\\piproposes edits and the semantic retriever supplies premises and schemas, but every change to the proof state passes through the symbolic operators defined below\. At evolutionary iterationtt, let𝒬t\\mathcal\{Q\}\_\{t\}be the target queue,ℳT,t\\mathcal\{M\}\_\{T,t\}the proof DAG archive for targetTT,ℒt\\mathcal\{L\}\_\{t\}the verified theorem schema library, andℋt\\mathcal\{H\}\_\{t\}the store of rejected proposals and Lean errors keyed by\(T,D,s\)\(T,D,s\)\. The operational state is

𝒮t=\(𝒬t,\{ℳT,t\}T∈𝒬t,ℒt,ℋt\)\.\\mathcal\{S\}\_\{t\}=\\left\(\\mathcal\{Q\}\_\{t\},\\\{\\mathcal\{M\}\_\{T,t\}\\\}\_\{T\\in\\mathcal\{Q\}\_\{t\}\},\\mathcal\{L\}\_\{t\},\\mathcal\{H\}\_\{t\}\\right\)\.\(6\)EachℳT,t\\mathcal\{M\}\_\{T,t\}is local to one target, whereasℒt\\mathcal\{L\}\_\{t\}persists across targets\. The trusted projection isΣt=\(\{ℳT,t\}T,ℒt\)\\Sigma\_\{t\}=\(\\\{\\mathcal\{M\}\_\{T,t\}\\\}\_\{T\},\\mathcal\{L\}\_\{t\}\), and only kernel\-verified DAG transitions, archive updates with accepted DAGs, and kernel\-checked schema insertions may modify it\.

### 4\.2Neural Proof Proposal

At each step the policyπ\\piproposes an editδ\\deltato one frontier states∈frontier⁡\(D\)s\\in\\mathrm\{frontier\}\(D\), and the kernel decides whether it survives\. The trusted transition operator is

step𝒦​\(D,δ\)=\{D′,if Lean accepts the induced edge andD′is an acyclic extension ofD,⊥,otherwise\.\\mathrm\{step\}\_\{\\mathcal\{K\}\}\(D,\\delta\)=\\begin\{cases\}D^\{\\prime\},&\\begin\{subarray\}\{c\}\\text\{if Lean accepts the induced edge and\}\\\\ \\text\{$D^\{\\prime\}$ is an acyclic extension of $D$\}\\end\{subarray\},\\\\ \\bot,&\\text\{otherwise\}\.\\end\{cases\}\(7\)An acceptedD′D^\{\\prime\}extendsDDby a typed edge carrying the realizer of Eq\. \([2](https://arxiv.org/html/2608.26334#S3.E2)\) and stays finite and acyclic, whereas a rejected proposal leaves the proof DAG archive and schema library unchanged\. A proposal takes one of three forms\. In*decomposition*, the model proposes either a checked closing term or a proof constructor with typed intermediate obligations, and any proposal\-time hole must become an explicit child state before acceptance\([Jiang et al\., 2023](https://arxiv.org/html/2608.26334#bib.bib19);[Varambally et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib47)\)\. In*schema recombination*, the model applies a library schema, whose mechanics we defer to Section[4\.3](https://arxiv.org/html/2608.26334#S4.SS3)\. In*repair*, available only for a previously rejected proposal at the same state, the model receives the proposal, retrieval context, and Lean error, and the corrected edge must pass the samestep𝒦\\mathrm\{step\}\_\{\\mathcal\{K\}\}check\([Varambally et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib47)\)\.

#### Kernel\-grounded selection\.

Root verification is binary, but an accepted DAG records which internal obligations are already proved, and we turn this structure into a kernel\-grounded fitness functional\. For every nonempty child set, letwe​\(s′\)\>0w\_\{e\}\(s^\{\\prime\}\)\>0with∑s′∈ch⁡\(e\)we​\(s′\)=1\\sum\_\{s^\{\\prime\}\\in\\mathrm\{ch\}\(e\)\}w\_\{e\}\(s^\{\\prime\}\)=1\. Edge and state values are defined together by well\-founded recursion over the acyclic DAG, evaluated from leaves to root in reverse topological order\. For a non\-closing edge,

ρD​\(e\)=∑s′∈ch⁡\(e\)we​\(s′\)​ρD​\(s′\)\.\\rho\_\{D\}\(e\)=\\sum\_\{s^\{\\prime\}\\in\\mathrm\{ch\}\(e\)\}w\_\{e\}\(s^\{\\prime\}\)\\rho\_\{D\}\(s^\{\\prime\}\)\.\(8\)For a statess,

ρD​\(s\)=\{1,ClosedD​\(s\),0,outD​\(s\)=∅,maxe∈outD​\(s\)⁡ρD​\(e\),otherwise,\\rho\_\{D\}\(s\)=\\begin\{cases\}1,&\\mathrm\{Closed\}\_\{D\}\(s\),\\\\ 0,&\\mathrm\{out\}\_\{D\}\(s\)=\\varnothing,\\\\ \\displaystyle\\max\_\{e\\in\\mathrm\{out\}\_\{D\}\(s\)\}\\rho\_\{D\}\(e\),&\\text\{otherwise\},\\end\{cases\}\(9\)We use uniform weights and writeρ​\(D\)=ρD​\(r\)\\rho\(D\)=\\rho\_\{D\}\(r\)\. The maximum encodes alternative edges at anornode, and the weighted sum encodes the conjunctive obligations along anandedge\. Reverse topological induction givesρ⁡\(D\)∈\[0,1\]\\rho\(D\)\\in\[0,1\]\. Ifrris closed, the first case of Eq\. \([9](https://arxiv.org/html/2608.26334#S4.E9)\) givesρ⁡\(D\)=1\\rho\(D\)=1\. Conversely, if an open state has value one, some outgoing edge has weighted average one, and positivity of the weights forces every child to have value one\. Induction then closes every child and hence the source, a contradiction\. Therefore

ρ⁡\(D\)=1⟺ClosedD​\(r\)\.\\rho\(D\)=1\\Longleftrightarrow\\mathrm\{Closed\}\_\{D\}\(r\)\.\(10\)Finally, ifD⪯D′D\\preceq D^\{\\prime\}, every earlier alternative remains available and closed nodes stay closed, soρ⁡\(D′\)≥ρ⁡\(D\)\\rho\(D^\{\\prime\}\)\\geq\\rho\(D\): verified closure is monotone under extension and computed entirely from kernel\-accepted proof DAGs\.

#### Structural diversity\.

To preserve distinct proof strategies, letℬ\\mathcal\{B\}be a fixed descriptor space and letb⁡\(D\)∈ℬb\(D\)\\in\\mathcal\{B\}record binned depth, dominant tactic family, and the region of the schema index used byDD\. The archiveℳT\\mathcal\{M\}\_\{T\}\([Mouret and Clune, 2015](https://arxiv.org/html/2608.26334#bib.bib29)\)stores at most one DAG per descriptor, and an accepted challengerD′D^\{\\prime\}updates its cell by

ℳT​\[b⁡\(D′\)\]←\{D′,b⁡\(D′\)∉dom⁡\(ℳT\),D′,ρ⁡\(D′\)\>ρ⁡\(ℳT​\[b⁡\(D′\)\]\),ℳT​\[b⁡\(D′\)\],otherwise,\\mathcal\{M\}\_\{T\}\[b\(D^\{\\prime\}\)\]\\leftarrow\\begin\{cases\}D^\{\\prime\},&b\(D^\{\\prime\}\)\\notin\\mathrm\{dom\}\(\\mathcal\{M\}\_\{T\}\),\\\\ D^\{\\prime\},&\\rho\(D^\{\\prime\}\)\>\\rho\(\\mathcal\{M\}\_\{T\}\[b\(D^\{\\prime\}\)\]\),\\\\ \\mathcal\{M\}\_\{T\}\[b\(D^\{\\prime\}\)\],&\\text\{otherwise\},\\end\{cases\}\(11\)so the incumbent wins ties\. For a temperatureτ\>0\\tau\>0, parents are sampled from occupied cells by

P⁡\(D∣ℳT\)=exp⁡\(ρ⁡\(D\)/τ\)∑D′′∈range⁡\(ℳT\)exp⁡\(ρ⁡\(D′′\)/τ\)\.P\(D\\mid\\mathcal\{M\}\_\{T\}\)=\\frac\{\\exp\(\\rho\(D\)/\\tau\)\}\{\\sum\_\{D^\{\\prime\\prime\}\\in\\mathrm\{range\}\(\\mathcal\{M\}\_\{T\}\)\}\\exp\(\\rho\(D^\{\\prime\\prime\}\)/\\tau\)\}\.\(12\)The archive therefore retains structural diversity while verified closure supplies selection pressure\.

#### Frontier scheduling\.

Algorithm[1](https://arxiv.org/html/2608.26334#alg1)\(Appendix[A](https://arxiv.org/html/2608.26334#A1)\) gives one iteration of ProofEvolve, with parent selection following Eq\. \([12](https://arxiv.org/html/2608.26334#S4.E12)\)\. Fors∈frontier⁡\(D\)s\\in\\mathrm\{frontier\}\(D\), letρD\[s↦1\]\\rho\_\{D\}^\{\[s\\mapsto 1\]\}denote the recursion of Eqs\. \([8](https://arxiv.org/html/2608.26334#S4.E8)\)–\([9](https://arxiv.org/html/2608.26334#S4.E9)\) with the value atsscounterfactually fixed to one\. Frontier scheduling then uses

ΔD\(s\)=ρD\[s↦1\]\(r\)−ρD\(r\),\\Delta\_\{D\}\(s\)=\\rho\_\{D\}^\{\[s\\mapsto 1\]\}\(r\)\-\\rho\_\{D\}\(r\),\(13\)which prioritizes the frontier state whose closure would yield the largest structural gain\.

### 4\.3Symbolic Knowledge Inheritance

Recombination is the operator that carries verified work across targets\. A closed state may depend on variables and assumptions from its local context, and kernel\-checked schema extraction turns that local result into a reusable pair\(ℓ,πℓ\)\(\\ell,\\pi\_\{\\ell\}\): the schemaℓ\\ellquantifies the free local variables𝐱\\mathbf\{x\}, makes each used hypothesisAiA\_\{i\}an explicit premise, and has conclusionCC, whileπℓ\\pi\_\{\\ell\}is its proof term:

ℓ:∀𝐱,A1→⋯→Am→C,ℰ⊢𝒦πℓ:ℓ\.\\ell:\\forall\\mathbf\{x\},\\ A\_\{1\}\\rightarrow\\cdots\\rightarrow A\_\{m\}\\rightarrow C,\\qquad\\mathcal\{E\}\\vdash\_\{\\mathcal\{K\}\}\\pi\_\{\\ell\}:\\ell\.\(14\)For this prenex schema,concl⁡\(ℓ\)=C\\mathrm\{concl\}\(\\ell\)=C\. WritingCl⁡\(D\)=\{s∈V⁡\(D\):ClosedD​\(s\)\}\\mathrm\{Cl\}\(D\)=\\\{s\\in V\(D\):\\mathrm\{Closed\}\_\{D\}\(s\)\\\}, the states newly closed by an extensionD⪯D′D\\preceq D^\{\\prime\}are

NewClose⁡\(D,D′\)=Cl⁡\(D′\)∖Cl⁡\(D\)\.\\mathrm\{NewClose\}\(D,D^\{\\prime\}\)=\\mathrm\{Cl\}\(D^\{\\prime\}\)\\setminus\\mathrm\{Cl\}\(D\)\.\(15\)For eachs∈NewClose⁡\(D,D′\)s\\in\\mathrm\{NewClose\}\(D,D^\{\\prime\}\), the extraction map followswinD′\\mathrm\{win\}\_\{D^\{\\prime\}\}and abstracts, in dependency order, exactly the free local constants and hypotheses occurring inAsmD′​\(s\)\\mathrm\{Asm\}\_\{D^\{\\prime\}\}\(s\)\. It returns no schema if this generalization or the displayed kernel judgment fails\. We writeExtract𝒦​\(D,D′\)\\mathrm\{Extract\}\_\{\\mathcal\{K\}\}\(D,D^\{\\prime\}\)for the checked schemas obtained from this set\.

At an open states=\(Γ⊢g\)s=\(\\Gamma\\vdash g\), a schema is applicable when a typed substitution makes its conclusion definitionally equal to the goal\. A substitutionσ\\sigmamaps the binder telescope𝐱\\mathbf\{x\}to Lean terms inΓ\\Gamma, and we writeAdmΓ​\(σ\)\\mathrm\{Adm\}\_\{\\Gamma\}\(\\sigma\)when every instantiated binder elaborates inΓ\\Gammawithout unresolved metavariables\. Then

𝖠𝗉𝗉ℒ\(s\)=\{\(ℓ,σ\):concl\(ℓ\)σ≡ℰg∧AdmΓ\(σ\)\}\.\\mathsf\{App\}\_\{\\mathcal\{L\}\}\(s\)=\\\{\(\\ell,\\sigma\):\\mathrm\{concl\}\(\\ell\)\\sigma\\equiv\_\{\\mathcal\{E\}\}g\\land\\mathrm\{Adm\}\_\{\\Gamma\}\(\\sigma\)\\\}\.\(16\)For\(ℓ,σ\)∈𝖠𝗉𝗉ℒ​\(s\)\(\\ell,\\sigma\)\\in\\mathsf\{App\}\_\{\\mathcal\{L\}\}\(s\), Lean first attempts local witnessespi∈𝖯𝗋𝖿ℰ​\(Γ⊢Ai​σ\)p\_\{i\}\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(\\Gamma\\vdash A\_\{i\}\\sigma\)\. Each premise without such a witness becomes a child state\(Γ⊢Ai​σ\)\(\\Gamma\\vdash A\_\{i\}\\sigma\), and the instantiated schema application is elaborated as a complete hyperedge realizer before acceptance\. The semantic retriever returns a Mathlib premise shortlist and a library\-schema shortlist,

ℛM​\(s\)⊆𝖳𝗁𝗆⁡\(ℰ\),ℛℒ​\(s\)⊆\{ℓ∣\(ℓ,πℓ\)∈ℒ\},\\mathcal\{R\}\_\{M\}\(s\)\\subseteq\\mathsf\{Thm\}\(\\mathcal\{E\}\),\\qquad\\mathcal\{R\}\_\{\\mathcal\{L\}\}\(s\)\\subseteq\\\{\\ell\\mid\(\\ell,\\pi\_\{\\ell\}\)\\in\\mathcal\{L\}\\\},\(17\)and the candidates presented to the policy are

𝒞ℒ​\(s\)=\{\(ℓ,σ\)∈𝖠𝗉𝗉ℒ​\(s\):ℓ∈ℛℒ​\(s\)\}\.\\mathcal\{C\}\_\{\\mathcal\{L\}\}\(s\)=\\\{\(\\ell,\\sigma\)\\in\\mathsf\{App\}\_\{\\mathcal\{L\}\}\(s\):\\ell\\in\\mathcal\{R\}\_\{\\mathcal\{L\}\}\(s\)\\\}\.\(18\)To recombine, the model selects\(ℓ,σ\)∈𝒞ℒ​\(s\)\(\\ell,\\sigma\)\\in\\mathcal\{C\}\_\{\\mathcal\{L\}\}\(s\), and Lean accepts the result after checking the instantiated schema, all local witnesses, and all residual child obligations as one realizer\. Mathlib retrieval separately supplies premises to the proposal context\. A persistent schema therefore enters a later proof only as a kernel\-checked transformation of its state\.

### 4\.4Theoretical analysis

We formalize the soundness of ProofEvolve by showing that every proof object accepted into the proof DAG archive or schema library is validated by the Lean kernel\. The result below states that this property is preserved as the search extends proof DAGs and grows the library\. Let𝔇0\\mathfrak\{D\}\_\{0\}contain the initial DAGs\. Fort\>0t\>0,𝔇t\\mathfrak\{D\}\_\{t\}also contains every challenger accepted during transitions0,…,t−10,\\ldots,t\-1, including challengers later discarded by archive comparison\.

###### Theorem 1\(Invariance of kernel\-grounded state\)\.

Under the formal assumptions in Appendix[B](https://arxiv.org/html/2608.26334#A2), every finite execution𝒮0→⋯→𝒮n\\mathcal\{S\}\_\{0\}\\rightarrow\\cdots\\rightarrow\\mathcal\{S\}\_\{n\}of Algorithm[1](https://arxiv.org/html/2608.26334#alg1)satisfies, for each0≤t≤n0\\leq t\\leq n:

- \(I1\)every accepted edge in everyD∈𝔇tD\\in\\mathfrak\{D\}\_\{t\}has a checked realizer of the form in Eq\. \([2](https://arxiv.org/html/2608.26334#S3.E2)\);
- \(I2\)every closed nodessin everyD∈𝔇tD\\in\\mathfrak\{D\}\_\{t\}satisfiesAsmD​\(s\)∈𝖯𝗋𝖿ℰ​\(s\)\\mathrm\{Asm\}\_\{D\}\(s\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\); and
- \(I3\)every\(ℓ,πℓ\)∈ℒt\(\\ell,\\pi\_\{\\ell\}\)\\in\\mathcal\{L\}\_\{t\}satisfiesℰ⊢𝒦πℓ:ℓ\\mathcal\{E\}\\vdash\_\{\\mathcal\{K\}\}\\pi\_\{\\ell\}:\\ell\.

For every0≤t<n0\\leq t<n,ℒt⊆ℒt\+1\\mathcal\{L\}\_\{t\}\\subseteq\\mathcal\{L\}\_\{t\+1\}\. If transitionttrejects its proposal, thenΣt\+1=Σt\\Sigma\_\{t\+1\}=\\Sigma\_\{t\}\.

Building on Theorem[1](https://arxiv.org/html/2608.26334#Thmtheorem1), we obtain the validity of the proofs ProofEvolve returns\.

###### Corollary 1\(Validity of returned proofs\)\.

Under the assumptions of Theorem[1](https://arxiv.org/html/2608.26334#Thmtheorem1), if ProofEvolve returnsppfromD′∈𝔇nD^\{\\prime\}\\in\\mathfrak\{D\}\_\{n\}for a targetTTwith rootr=\(Γ0⊢T\)r=\(\\Gamma\_\{0\}\\vdash T\), thenℰ;Γ0⊢𝒦p:T\\mathcal\{E\};\\Gamma\_\{0\}\\vdash\_\{\\mathcal\{K\}\}p:T\.

The neural models decide only which variations to attempt, whereas the kernel decides whether an accepted one is valid\. Every proof ProofEvolve returns therefore type\-checks against the standard axioms by construction\. The assumptions and full proofs of Theorem[1](https://arxiv.org/html/2608.26334#Thmtheorem1)and Corollary[1](https://arxiv.org/html/2608.26334#Thmcorollary1)are deferred to Appendix[B](https://arxiv.org/html/2608.26334#A2)\.

Table 1:Main comparison\.Mean solve rate \(%\) over three independent runs on PutnamBench\([Tsoukalas et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib44)\), IMO\-LeanProofBench\([Luong et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib27)\), and CombiBench\([Liu et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib26)\)\.

## 5Experiments

### 5\.1Experimental setup

#### Implementation\.

In our experiments, the parameters of all base LLMs remain frozen throughout search and across targets\. For all agentic baselines, we use Claude Opus 4\.8 as base model to ensure fair comparison\. Lean 4 with Mathlib provides tactic states, elaboration errors, and kernel verification\. Each target receives a budget of parallel attempts together with a bounded kernel\-guided repair loop, and ProofEvolve draws its attempts from this budget\. All experiments use Lean 4 with the same Mathlib version\. For proprietary models, we use API calls\. For open\-sourced model hosting, we use NVIDIA B200 GPU clusters with 192 GB of memory per GPU\. Each node contains 8 GPUs, and our largest runs use up to 28 nodes, corresponding to 224 GPUs operating concurrently\.

#### Benchmarks and baselines\.

We evaluate on three competition\-level benchmarks\. PutnamBench\([Tsoukalas et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib44)\)formalizes problems from the William Lowell Putnam Mathematical Competition\. We use its pure\-proof subset, which excludes problems whose theorem statements already contain a fixed answer value\. IMO\-LeanProofBench\([Luong et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib27)\)contains Lean formalizations of International Mathematical Olympiad\-level proof problems\. CombiBench\([Liu et al\., 2025](https://arxiv.org/html/2608.26334#bib.bib26)\)covers competition\-level combinatorial mathematics, where a proof usually rests on an explicit construction or count\. We compare against pass@1616sampling from the LLMs and five agentic systems: LEAP, Hilbert, AxProver, Aristotle, and ReAct\. Our reproduction of each agentic system uses the same base LLM, retains its search strategy, and runs under a matched budget\.

#### Evaluation metrics\.

Our primary metric is the solve rate, the fraction of a benchmark whose theorems are proved and pass the Lean 4 kernel verification\. A theorem is evaluated as solved only when its final proof matches the benchmark ground truth, contains no unresolved metavariables or placeholders, and passes the Lean kernel\. We exclude proofs that rely onnative\_decide, because its code\-generation path introduces an axiom outside the standard proof kernel\. We apply the same verification to every solution in our evaluation\. Every reported solve is independently re\-verified against the matched Lean kernel with a restricted\#print axiomscheck\. Across more than400400re\-verifications, we found00false positives\.

### 5\.2Main results

Table[1](https://arxiv.org/html/2608.26334#S4.T1)reports solve rates on the three benchmarks\. Under pass@1616sampling, Claude Opus 4\.8 without agentic search solves0\.0%0\.0\\%of PutnamBench and IMO\-LeanProofBench\. The agentic systems use the same base model Claude Opus 4\.8, providing the closest matched comparison of their search methods\. ProofEvolve has the highest average solve rate at57\.8%57\.8\\%, ahead of LEAP \(50\.5%50\.5\\%\) and Hilbert \(45\.9%45\.9\\%\)\. It leads PutnamBench at71\.2%71\.2\\%,6\.56\.5points above LEAP, and widens the margin on IMO\-LeanProofBench, reaching53\.3%53\.3\\%against36\.7%36\.7\\%for LEAP\. On CombiBench the strongest systems are within one point, LEAP at50\.0%50\.0\\%and ProofEvolve at49\.0%49\.0\\%\. The largest margin appears on IMO\-LeanProofBench, whose problems often require proofs assembled from several lemmas\. This pattern is consistent with the intended role of graded selection and schema reuse on decomposable problems\.

### 5\.3Dynamics of verified closureρ\\rho

We study how verified closureρ\\rhochanges during proof search\. ProofEvolve usesρ\\rhoin Eq\. \([9](https://arxiv.org/html/2608.26334#S4.E9)\) as a fitness value computed from kernel\-accepted edges\. Unlike a binary root verdict, it records partial progress once Lean certifies intermediate subgoals\. Since Eq\. \([10](https://arxiv.org/html/2608.26334#S4.E10)\) guarantees that solved runs reachρ=1\\rho=1, we focus on the search trajectory before completion\. Figure[4](https://arxiv.org/html/2608.26334#S5.F4)shows thatρ\\rhoincreases step by step as subgoals are verified, while failed runs plateau below one\. Figure[4](https://arxiv.org/html/2608.26334#S5.F4)shows one solved run in which several lemmas are certified before the root is finally closed\. These results show thatρ\\rhocaptures verified intermediate progress that binary feedback cannot represent\.

\{subfigure\}\[b\]0\.372\{subfigure\}\[b\]0\.598

Figure 2:Closure trajectoriesFigure 3:One solved proof DAGFigure 4:Verified closureρ\\rhoduring search\.\(a\)ρ\\rhoagainst evolutionary iterations: solved runs \(green\) reach11, failed runs \(red\) plateau below, and the binary pass/fail signal \(dashed\) stays at00\(medians with interquartile bands\)\.\(b\)An accepted proof DAG whose lemma nodes are certified by the kernel at iterations5,7,10,115,7,10,11, soρ\\rhorises step by step to11\.Figure 5:Per\-difficulty ablation:every variation operator contributes more on the harder Advanced split than on the Basic split\. Error bars show the run\-to\-run standard deviation across independent reruns\.
### 5\.4Ablation study

We conduct ablation study on how each of the three variation operators affects ProofEvolve\. Decomposition breaks a goal into smaller subgoals\. Repair fixes a failed step using the error message from Lean 4\. Recombination reuses an already proved result to close a new goal\. We remove one operator at a time on the6060IMO\-LeanProofBench problems\. The base model and the compute budget stay the same, and we repeat each run with five random seeds to ensure statistical stability\. As shown in Figure[5](https://arxiv.org/html/2608.26334#S5.F5), the full system on average solves3232of the6060problems, with2222of3030on the Basic split and1010of3030on the Advanced split\. Without decomposition it on average solves1111\(99Basic,22Advanced\), without recombination1414\(1111Basic,33Advanced\), and without repair99\(77Basic,22Advanced\)\. The drop is larger on the harder Advanced split than on the Basic split\. These results show that all three variation operators contribute to the performance of ProofEvolve, with larger effects on the Advanced split\.

Figure 6:Test\-time budget scaling\(a\) Kernel\-verified transitions per target across seeds; \(b\) Union of distinct targets solved across seeds and configuration\.*In \(a\)*:![Refer to caption](https://arxiv.org/html/2608.26334v1/Figures/qwen_mark.png)Qwen3\.5think∘\\circ/instant□\\square;![Refer to caption](https://arxiv.org/html/2608.26334v1/Figures/qwen_mark.png)Qwen3\.6instant◇\\Diamond/think△\\triangle;![Refer to caption](https://arxiv.org/html/2608.26334v1/Figures/glm_mark.png)GLM\-5\.1\+\+;![Refer to caption](https://arxiv.org/html/2608.26334v1/Figures/moonshot_mark.png)Kimi\-K2\.6×\\times;![Refer to caption](https://arxiv.org/html/2608.26334v1/Figures/openai_mark.png)gpt\-ossmed▽\\triangledown/low×\\times\.
### 5\.5Test\-time budget scaling

We next test ProofEvolve with open\-weight models as the per\-target budget grows\. The models are Qwen3\.5\-397B\([Qwen Team, 2026a](https://arxiv.org/html/2608.26334#bib.bib36)\), Qwen3\.6\-35B\([Qwen Team, 2026b](https://arxiv.org/html/2608.26334#bib.bib37)\), Kimi\-K2\.6\([Moonshot AI, 2026](https://arxiv.org/html/2608.26334#bib.bib28)\), GLM\-5\.1\([Z\.ai, 2026](https://arxiv.org/html/2608.26334#bib.bib55)\), and gpt\-oss\-120b\([OpenAI, 2025](https://arxiv.org/html/2608.26334#bib.bib32)\), each run in the inference modes it supports, for eight configurations\. A per\-target budget caps the model calls, Lean\-kernel calls, tokens, and wall\-clock time each target may use\. Appendix[C](https://arxiv.org/html/2608.26334#A3)gives the models, decoding, and the full budget table\. Seven of the eight configurations produce more kernel\-verified transitions per target as the budget grows \(Figure[6](https://arxiv.org/html/2608.26334#S5.F6)a, per\-seed values in Appendix[D](https://arxiv.org/html/2608.26334#A4)\)\. The one exception, gpt\-oss\-120b at low reasoning effort, is flat across budgets, confirming that the trend is not merely a by\-product of issuing more calls\. The final results in Figure[6](https://arxiv.org/html/2608.26334#S5.F6)b shows that the number of distinct targets solved increases monotonically\. Appendix[D](https://arxiv.org/html/2608.26334#A4)reports the exact per\-budget counts\. We also provide the solutions found by the models in Appendix[E](https://arxiv.org/html/2608.26334#A5)\.

\{subfigure\}

\[t\]0\.4850022k44kfull00224466Library size \(verified self\-solutions\)Lift over zero\-shot \(pp\)

Figure 7:Library size, atK=8K\{=\}8\{subfigure\}

\[t\]0\.485008816163232646400224466Retrieved examplesKKLift over zero\-shot \(pp\)

Figure 8:Retrieval depth, full libraryFigure 9:Reusing the prover’s own verified proofs\.Solve\-rate lift over zero\-shot, in percentage points, on the744744screened evaluation theorems \(three\-run mean\)\.∙\\bulletrelevant retrieval;– –zero\-shot;▲\\blacktrianglerandom retrieval from the same library\. The band is±1\\pm 1run\-to\-run standard deviation*of the lift*, which is not the standard deviation of the solve rate reported in Table[7](https://arxiv.org/html/2608.26334#A6.T7)\. The lift is00at an empty library and atK=0K\{=\}0, where both conditions reduce to zero\-shot\.
### 5\.6Old Proofs, New Theorems: Verified Reuse Across Problems

A library that grows during evaluation should make later targets easier to prove\. We test this at two scales\. The controlled study below isolates accumulation in a setting where the dependency structure is known by construction\.

#### Controlled compositional families\.

To isolate the effect of a library that grows during evaluation, we run a controlled study on synthetic compositional lemma families, where each later target is built from lemmas that earlier targets establish\. ProofEvolve solves19\.8%19\.8\\%of the targets when the library grows across targets and7\.3%7\.3\\%when the library is reset before each target\. The growing library therefore solves2\.7×2\.7\\timesas many targets, with every other component held fixed\. The study isolates the inheritance mechanism in this controlled setting, separate from the benchmark evaluation\. Recombination stays sound throughout, because a typed schema discharges a subgoal only when Lean accepts its instantiation, so a mismatched retrieval fails without changing the trusted proof state\.

#### Unseen Lean Workbook theorems\.

The compositional families are synthetic\. We next evaluate cross\-problem reuse on real competition\-style theorems, using a library built entirely from the prover’s own work\. We start from Lean Workbook\([Ying et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib54)\)statements with the machine\-generated proofs released by Goedel\-Prover\([Lin et al\., 2025a](https://arxiv.org/html/2608.26334#bib.bib24)\)\. Re\-verification under the same kernel and axiom checks retains20,55420\{,\}554statement and proof pairs, and deduplication leaves10,96810\{,\}968distinct theorems\. We hold out1,0001\{,\}000for evaluation and use the remaining9,9689\{,\}968as a source stream\. The base model, Qwen3\.5\-397B\-A17B\-FP8\([Qwen Team, 2026a](https://arxiv.org/html/2608.26334#bib.bib36)\), attempts every buildable source theorem once; its5,5465\{,\}546kernel\-accepted proofs form the library\. Five independent language\-model judges screen the evaluation theorems against their retrieved neighbors, leaving the744744theorems that fewer than two judges flag\. For each evaluation theorem the semantic retriever selects the top\-KKschemas, and their statements and Lean\-accepted proof bodies enter the proposal context\.*Zero\-shot*omits that context, and*random retrieval*suppliesKKschemas drawn uniformly from the same library\. All conditions share one prompt template, one Lean environment and one decoding profile\. We report the mean over three runs, with condition contrasts computed as paired differences across matched runs\.

AtK=8K\{=\}8the library raises the solve rate from49\.5%49\.5\\%to53\.4%53\.4\\%, a gain of3\.93\.9points, while random retrieval from the same library reaches49\.6%49\.6\\%: the improvement comes from selecting useful verified work, not from adding examples to the prompt\. The gain appears at every library size and retrieval depth we measure\. A library of only1,0001\{,\}000proofs already adds3\.33\.3points, and the gain reaches5\.35\.3points atK=64K\{=\}64\. Figure[9](https://arxiv.org/html/2608.26334#S5.F9)shows both scaling axes and Table[7](https://arxiv.org/html/2608.26334#A6.T7)lists every condition\. Across the three runs atK=8K\{=\}8, relevant retrieval closes351351theorem instances that zero\-shot leaves open, and in322322of them, or91\.7%91\.7\\%, the accepted proof does not reproduce any shown proof verbatim\. The library supplies reusable proof structure rather than a catalog of answers\.

This study isolates one mechanism\. Each condition gives a single whole\-proof attempt with no repair and no second sample, so retrieved schemas act as in\-context exemplars rather than as typed instantiations composed into a realizer \(Eqs\. \([16](https://arxiv.org/html/2608.26334#S4.E16)\)–\([18](https://arxiv.org/html/2608.26334#S4.E18)\)\); the DAG archive, decomposition, repair, and verified closure as a selection signal are all switched off\. Holding the search fixed is what makes the library’s own contribution measurable\. Appendix[F](https://arxiv.org/html/2608.26334#A6)records the full setup and Appendix[G](https://arxiv.org/html/2608.26334#A7)shows two retrieval\-to\-proof traces\.

## 6Conclusion

We introduced ProofEvolve, a neuro\-symbolic evolutionary framework that improves through explicit, formally verified proof structures\. It represents partial proofs as AND\-OR DAGs, ranks them using kernel\-grounded verified closure, preserves structurally diverse candidates, and extracts closed sub\-DAGs as reusable theorem schemas\. The symbolic Lean 4 kernel faithfully checks every proposed variation before it can evolve the internal structured knowledge\. Empirically, ProofEvolve achieves the highest average solve rate among the state\-of\-the\-art baselines on three challenging competition\-level Lean benchmarks, and on Lean Workbook theorems disjoint from its library a library of the prover’s own verified proofs adds about four points over zero\-shot, with random retrieval from the same library adding nothing\. More broadly, this work paves a concrete step toward recursively self\-improving agents that accumulate formal knowledge over time\. This insight could shed light on scientific discovery in other scientific domains, such as theoretical physics and chemistry\. We hope this work can inspire future research on the field of continual learning for AI\-driven scientific discovery\.

## References

- Achim et al\. \(2025\)Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern\-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu\.Aristotle: Imo\-level automated theorem proving, 2025\.[https://arxiv\.org/abs/2510\.01346](https://arxiv.org/abs/2510.01346)\.
- Anthropic \(2025\)Anthropic\.Claude Haiku 4\.5 System Card\.[https://www\.anthropic\.com/claude\-haiku\-4\-5\-system\-card](https://www.anthropic.com/claude-haiku-4-5-system-card), October 2025\.Model ID:claude\-haiku\-4\-5\-20251001\.
- Anthropic \(2026a\)Anthropic\.Claude Opus 4\.8 System Card\.[https://www\.anthropic\.com/claude\-opus\-4\-8\-system\-card](https://www.anthropic.com/claude-opus-4-8-system-card), May 2026a\.Model ID:claude\-opus\-4\-8\.
- Anthropic \(2026b\)Anthropic\.Claude Sonnet 4\.6 System Card\.[https://www\.anthropic\.com/claude\-sonnet\-4\-6\-system\-card](https://www.anthropic.com/claude-sonnet-4-6-system-card), February 2026b\.Model ID:claude\-sonnet\-4\-6\.
- Berlot\-Attwell et al\. \(2025\)Ian Berlot\-Attwell, Frank Rudzicz, and Xujie Si\.Llm library learning fails: A lego\-prover case study, 2025\.[https://arxiv\.org/abs/2504\.03048](https://arxiv.org/abs/2504.03048)\.
- Bonola \(1955\)Roberto Bonola\.*Non\-Euclidean Geometry: A Critical and Historical Study of Its Development*\.Dover Publications, New York, 1955\.
- Breen et al\. \(2025\)Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M\. Taylor, Frank H\. L\. Koppens, and Dirk Englund\.Ax\-prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics, 2025\.[https://arxiv\.org/abs/2510\.12787](https://arxiv.org/abs/2510.12787)\.
- ByteDance Seed \(2025\)ByteDance Seed\.Seed\-prover: Deep and broad reasoning for automated theorem proving, 2025\.[https://arxiv\.org/abs/2507\.23726](https://arxiv.org/abs/2507.23726)\.
- Church \(1936\)Alonzo Church\.An unsolvable problem of elementary number theory\.*American Journal of Mathematics*, 58\(2\):345–363, 1936\.[10\.2307/2371045](https://doi.org/10.2307/2371045)\.
- Davies et al\. \(2021\)Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev, Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie Williamson, Demis Hassabis, and Pushmeet Kohli\.Advancing mathematics by guiding human intuition with ai\.*Nature*, 600:70–74, 2021\.[https://www\.nature\.com/articles/s41586\-021\-04086\-x](https://www.nature.com/articles/s41586-021-04086-x)\.
- de Moura and Ullrich \(2021\)Leonardo de Moura and Sebastian Ullrich\.The Lean 4 theorem prover and programming language\.In*International Conference on Automated Deduction \(CADE\)*, 2021\.
- Ellis et al\. \(2021\)Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sable\-Meyer, Luc Cary, Lucas Morales, Luke Hewitt, Armando Solar\-Lezama, and Joshua B\. Tenenbaum\.Dreamcoder: Bootstrapping inductive program synthesis with wake\-sleep library learning, 2021\.[https://arxiv\.org/abs/2006\.08381](https://arxiv.org/abs/2006.08381)\.PLDI 2021\.
- Fang et al\. \(2025\)Jian Fang, Yican Sun, and Yingfei Xiong\.Proof strategy extraction from LLMs for enhancing symbolic provers, 2025\.[https://arxiv\.org/abs/2510\.10131](https://arxiv.org/abs/2510.10131)\.
- Google DeepMind \(2026\)Google DeepMind\.Gemini 3\.1 Pro Model Card\.[https://deepmind\.google/models/model\-cards/gemini\-3\-1\-pro/](https://deepmind.google/models/model-cards/gemini-3-1-pro/), February 2026\.API model ID:gemini\-3\.1\-pro\-preview\.
- Han et al\. \(2021\)Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W\. Ayers, and Stanislas Polu\.Proof artifact co\-training for theorem proving with language models, 2021\.[https://arxiv\.org/abs/2102\.06203](https://arxiv.org/abs/2102.06203)\.ICLR 2022\.
- Hilbert and Ackermann \(1928\)David Hilbert and Wilhelm Ackermann\.*Grundzüge der theoretischen Logik*\.Julius Springer, Berlin, 1928\.
- Hubert et al\. \(2026\)Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z\. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salvatore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Velingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli, and David Silver\.Olympiad\-level formal mathematical reasoning with reinforcement learning\.*Nature*, 651, 2026\.[10\.1038/s41586\-025\-09833\-y](https://doi.org/10.1038/s41586-025-09833-y)\.[https://www\.nature\.com/articles/s41586\-025\-09833\-y](https://www.nature.com/articles/s41586-025-09833-y)\.
- Ji et al\. \(2025\)Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai\.Leanabell\-Prover\-V2: Verifier\-integrated reasoning for formal theorem proving via reinforcement learning, 2025\.[https://arxiv\.org/abs/2507\.08649](https://arxiv.org/abs/2507.08649)\.
- Jiang et al\. \(2023\)Albert Q\. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample\.Draft, sketch, and prove: Guiding formal theorem provers with informal proofs, 2023\.[https://arxiv\.org/abs/2210\.12283](https://arxiv.org/abs/2210.12283)\.ICLR 2023\.
- Kautz \(2022\)Henry Kautz\.The third AI summer: AAAI robert s\. engelmore memorial lecture\.*AI Magazine*, 43\(1\):105–125, 2022\.
- Kumarappan et al\. \(2024\)Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anandkumar\.LeanAgent: Lifelong learning for formal theorem proving, 2024\.[https://arxiv\.org/abs/2410\.06209](https://arxiv.org/abs/2410.06209)\.
- Kung et al\. \(2026\)Po\-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun\-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart, Quoc V\. Le, Burak Gokturk, Thang Luong, Tomas Pfister, and Nanyun Peng\.LEAP: Supercharging LLMs for formal mathematics with agentic frameworks, 2026\.[https://arxiv\.org/abs/2606\.03303](https://arxiv.org/abs/2606.03303)\.
- Lample et al\. \(2022\)Guillaume Lample, Marie\-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurelien Rodriguez, and Timothee Lacroix\.Hypertree proof search for neural theorem proving, 2022\.[https://arxiv\.org/abs/2205\.11491](https://arxiv.org/abs/2205.11491)\.NeurIPS 2022\.
- Lin et al\. \(2025a\)Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin\.Goedel\-prover: A frontier model for open\-source automated theorem proving, 2025a\.[https://arxiv\.org/abs/2502\.07640](https://arxiv.org/abs/2502.07640)\.
- Lin et al\. \(2025b\)Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui\-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin\.Goedel\-prover\-v2: Scaling formal theorem proving with scaffolded data synthesis and self\-correction, 2025b\.[https://arxiv\.org/abs/2508\.03613](https://arxiv.org/abs/2508.03613)\.
- Liu et al\. \(2025\)Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, Zhengfeng Yang, Jujian Zhang, Lihong Zhi, Jia Li, and Zhengying Liu\.Combibench: Benchmarking llm capability for combinatorial mathematics, 2025\.[https://arxiv\.org/abs/2505\.03171](https://arxiv.org/abs/2505.03171)\.
- Luong et al\. \(2025\)Thang Luong, Dawsen Hwang, Hoang H\. Nguyen, Golnaz Ghiasi, Yuri Chervonyi, Insuk Seo, Junsu Kim, Garrett Bingham, Jonathan Lee, Swaroop Mishra, Alex Zhai, Clara Huiyi Hu, Henryk Michalewski, Jimin Kim, Jeonghyun Ahn, Junhwi Bae, Xingyou Song, Trieu H\. Trinh, Quoc V\. Le, and Junehyuk Jung\.Towards robust mathematical reasoning\.In*Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing \(EMNLP\)*, 2025\.[https://aclanthology\.org/2025\.emnlp\-main\.1794/](https://aclanthology.org/2025.emnlp-main.1794/)\.
- Moonshot AI \(2026\)Moonshot AI\.Kimi\-K2\.6\.Hugging Face model card, 2026\.[https://huggingface\.co/moonshotai/Kimi\-K2\.6](https://huggingface.co/moonshotai/Kimi-K2.6)\.Revision 2755962d\.
- Mouret and Clune \(2015\)Jean\-Baptiste Mouret and Jeff Clune\.Illuminating search spaces by mapping elites, 2015\.[https://arxiv\.org/abs/1504\.04909](https://arxiv.org/abs/1504.04909)\.
- Nagashima \(2019\)Yutaka Nagashima\.Towards evolutionary theorem proving for isabelle/hol, 2019\.[https://arxiv\.org/abs/1904\.08468](https://arxiv.org/abs/1904.08468)\.
- Novikov et al\. \(2025\)Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po\-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J\. R\. Ruiz, Abbas Mehrabian, M\. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog\.Alphaevolve: A coding agent for scientific and algorithmic discovery, 2025\.[https://arxiv\.org/abs/2506\.13131](https://arxiv.org/abs/2506.13131)\.
- OpenAI \(2025\)OpenAI\.gpt\-oss\-120b\.Hugging Face model card, 2025\.[https://huggingface\.co/openai/gpt\-oss\-120b](https://huggingface.co/openai/gpt-oss-120b)\.Revision b5c939de\.
- OpenAI \(2026\)OpenAI\.GPT\-5\.5 System Card\.[https://openai\.com/index/gpt\-5\-5\-system\-card/](https://openai.com/index/gpt-5-5-system-card/), April 2026\.Model ID:gpt\-5\.5\.
- Poesia et al\. \(2024\)Gabriel Poesia, David Broman, Nick Haber, and Noah D\. Goodman\.Learning formal mathematics from intrinsic motivation, 2024\.[https://arxiv\.org/abs/2407\.00695](https://arxiv.org/abs/2407.00695)\.NeurIPS 2024\.
- Polu and Sutskever \(2020\)Stanislas Polu and Ilya Sutskever\.Generative language modeling for automated theorem proving, 2020\.[https://arxiv\.org/abs/2009\.03393](https://arxiv.org/abs/2009.03393)\.
- Qwen Team \(2026a\)Qwen Team\.Qwen3\.5\-397B\-A17B\-FP8\.Hugging Face model card, 2026a\.[https://huggingface\.co/Qwen/Qwen3\.5\-397B\-A17B\-FP8](https://huggingface.co/Qwen/Qwen3.5-397B-A17B-FP8)\.Revision 9f1f3de9\.
- Qwen Team \(2026b\)Qwen Team\.Qwen3\.6\-35B\-A3B\.Hugging Face model card, 2026b\.[https://huggingface\.co/Qwen/Qwen3\.6\-35B\-A3B](https://huggingface.co/Qwen/Qwen3.6-35B-A3B)\.Revision 53c43178\.
- Ren et al\. \(2025\)Z\. Z\. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z\. F\. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan\.Deepseek\-prover\-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025\.[https://arxiv\.org/abs/2504\.21801](https://arxiv.org/abs/2504.21801)\.
- Romera\-Paredes et al\. \(2024\)Bernardino Romera\-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M\. Pawan Kumar, Emilien Dupont, Francisco J\. R\. Ruiz, Jordan S\. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi\.Mathematical discoveries from program search with large language models\.*Nature*, 625:468–475, 2024\.[https://www\.nature\.com/articles/s41586\-023\-06924\-6](https://www.nature.com/articles/s41586-023-06924-6)\.
- Shen et al\. \(2025\)Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai, and Bin Dong\.REAL\-Prover: Retrieval augmented Lean prover for mathematical reasoning, 2025\.[https://arxiv\.org/abs/2505\.20613](https://arxiv.org/abs/2505.20613)\.
- Thakur et al\. \(2024\)Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri\.An in\-context learning agent for formal theorem\-proving, 2024\.[https://arxiv\.org/abs/2310\.04353](https://arxiv.org/abs/2310.04353)\.COLM 2024\.
- The mathlib Community \(2020\)The mathlib Community\.The Lean mathematical library\.In*ACM SIGPLAN International Conference on Certified Programs and Proofs \(CPP\)*, 2020\.
- Trinh et al\. \(2024\)Trieu H\. Trinh, Yuhuai Wu, Quoc V\. Le, He He, and Thang Luong\.Solving olympiad geometry without human demonstrations\.*Nature*, 625:476–482, 2024\.[https://www\.nature\.com/articles/s41586\-023\-06747\-5](https://www.nature.com/articles/s41586-023-06747-5)\.
- Tsoukalas et al\. \(2024\)George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri\.Putnambench: Evaluating neural theorem\-provers on the putnam mathematical competition, 2024\.[https://arxiv\.org/abs/2407\.11214](https://arxiv.org/abs/2407.11214)\.NeurIPS 2024 Datasets and Benchmarks\.
- Tsoukalas et al\. \(2026\)George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J\. R\. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z\. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, and Swarat Chaudhuri\.Advancing mathematics research with ai\-driven formal proof search, 2026\.[https://arxiv\.org/abs/2605\.22763](https://arxiv.org/abs/2605.22763)\.
- Turing \(1937\)Alan M\. Turing\.On computable numbers, with an application to the entscheidungsproblem\.*Proceedings of the London Mathematical Society*, 42\(1\):230–265, 1937\.[10\.1112/plms/s2\-42\.1\.230](https://doi.org/10.1112/plms/s2-42.1.230)\.
- Varambally et al\. \(2025\)Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, and Rose Yu\.Hilbert: Recursively building formal proofs with informal reasoning, 2025\.[https://arxiv\.org/abs/2509\.22819](https://arxiv.org/abs/2509.22819)\.
- Wang et al\. \(2023\)Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang\.Lego\-prover: Neural theorem proving with growing libraries, 2023\.[https://arxiv\.org/abs/2310\.00656](https://arxiv.org/abs/2310.00656)\.ICLR 2024\.
- Wang et al\. \(2025\)Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus\-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen\-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li\.Kimina\-prover preview: Towards large formal reasoning models with reinforcement learning, 2025\.[https://arxiv\.org/abs/2504\.11354](https://arxiv.org/abs/2504.11354)\.
- Xin et al\. \(2025a\)Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen\.Bfs\-prover: Scalable best\-first tree search for llm\-based automatic theorem proving, 2025a\.[https://arxiv\.org/abs/2502\.03438](https://arxiv.org/abs/2502.03438)\.
- Xin et al\. \(2025b\)Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, and Xia Xiao\.Scaling up multi\-turn off\-policy RL and multi\-agent tree search for LLM step\-provers, 2025b\.[https://arxiv\.org/abs/2509\.06493](https://arxiv.org/abs/2509.06493)\.
- Yang et al\. \(2023\)Kaiyu Yang, Aidan M\. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar\.Leandojo: Theorem proving with retrieval\-augmented language models, 2023\.[https://arxiv\.org/abs/2306\.15626](https://arxiv.org/abs/2306.15626)\.NeurIPS 2023 Datasets and Benchmarks\.
- Yao et al\. \(2023\)Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao\.ReAct: Synergizing reasoning and acting in language models\.In*International Conference on Learning Representations \(ICLR\)*, 2023\.[https://arxiv\.org/abs/2210\.03629](https://arxiv.org/abs/2210.03629)\.
- Ying et al\. \(2024\)Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen\.Lean workbook: A large\-scale lean problem set formalized from natural language math problems, 2024\.[https://arxiv\.org/abs/2406\.03847](https://arxiv.org/abs/2406.03847)\.
- Z\.ai \(2026\)Z\.ai\.GLM\-5\.1\-FP8\.Hugging Face model card, 2026\.[https://huggingface\.co/zai\-org/GLM\-5\.1\-FP8](https://huggingface.co/zai-org/GLM-5.1-FP8)\.Revision f396cf80\.
- Zhang et al\. \(2025\)Jenny Zhang, Shengran Hu, Cong Lu, Robert Lange, and Jeff Clune\.Darwin Gödel machine: Open\-ended evolution of self\-improving agents, 2025\.[https://arxiv\.org/abs/2505\.22954](https://arxiv.org/abs/2505.22954)\.
- Zhang et al\. \(2026\)Youyuan Zhang, Jialiang Sun, Hangrui Bi, Chuqin Geng, Wenjie Ma, Zhaoyu Li, and Xujie Si\.DreamProver: Evolving transferable lemma libraries via a wake\-sleep theorem\-proving agent, 2026\.[https://arxiv\.org/abs/2604\.26311](https://arxiv.org/abs/2604.26311)\.

## Appendix

## Appendix AAlgorithm

The full evolutionary iteration summarized in Section[4\.2](https://arxiv.org/html/2608.26334#S4.SS2.SSS0.Px3)is given below\.

Algorithm 1One evolutionary iteration in ProofEvolveInput: target queue𝒬\\mathcal\{Q\}; policyπ\\pi; kernel𝒦\\mathcal\{K\}; archives\{ℳT\}\\\{\\mathcal\{M\}\_\{T\}\\\}; schema libraryℒ\\mathcal\{L\}; error storeℋ\\mathcal\{H\}

1:Select

T∈𝒬T\\in\\mathcal\{Q\}\. If

ℳT\\mathcal\{M\}\_\{T\}is empty, insert the singleton root DAG\.

2:Sample parent

DDfrom

ℳT\\mathcal\{M\}\_\{T\}using Eq\. \([12](https://arxiv.org/html/2608.26334#S4.E12)\)\.

3:Select

s∈frontier⁡\(D\)s\\in\\mathrm\{frontier\}\(D\)maximizing

ΔD​\(s\)\\Delta\_\{D\}\(s\)\.

4:Retrieve Mathlib premises

ℛM​\(s\)\\mathcal\{R\}\_\{M\}\(s\)and schemas

ℛℒ​\(s\)\\mathcal\{R\}\_\{\\mathcal\{L\}\}\(s\); form

𝒞ℒ​\(s\)\\mathcal\{C\}\_\{\\mathcal\{L\}\}\(s\)\.

5:if

ℋ⁡\(T,D,s\)\\mathcal\{H\}\(T,D,s\)contains a rejected edit and error

ϵ\\epsilonthen

6:Sample

δ∼π⁡\(repair∣s,D,ℛM​\(s\),𝒞ℒ​\(s\),ϵ\)\\delta\\sim\\pi\(\\textsc\{repair\}\\mid s,D,\\mathcal\{R\}\_\{M\}\(s\),\\mathcal\{C\}\_\{\\mathcal\{L\}\}\(s\),\\epsilon\)\.

7:else

8:Choose an applicable

o∈\{decompose,recombine\}o\\in\\\{\\textsc\{decompose\},\\textsc\{recombine\}\\\}\.

9:Sample

δ∼π⁡\(o∣s,D,ℛM​\(s\),𝒞ℒ​\(s\)\)\\delta\\sim\\pi\(o\\mid s,D,\\mathcal\{R\}\_\{M\}\(s\),\\mathcal\{C\}\_\{\\mathcal\{L\}\}\(s\)\)\.

10:endif

11:Compute

D′←step𝒦​\(D,δ\)D^\{\\prime\}\\leftarrow\\mathrm\{step\}\_\{\\mathcal\{K\}\}\(D,\\delta\)\.

12:if

D′=⊥D^\{\\prime\}=\\botthen

13:Store the rejected edit and Lean error in

ℋ⁡\(T,D,s\)\\mathcal\{H\}\(T,D,s\);returnwith

Σ\\Sigmaunchanged\.

14:endif

15:

ℒ←ℒ∪Extract𝒦​\(D,D′\)\\mathcal\{L\}\\leftarrow\\mathcal\{L\}\\cup\\mathrm\{Extract\}\_\{\\mathcal\{K\}\}\(D,D^\{\\prime\}\)\.

16:Update

ℳT​\[b⁡\(D′\)\]\\mathcal\{M\}\_\{T\}\[b\(D^\{\\prime\}\)\]using Eq\. \([11](https://arxiv.org/html/2608.26334#S4.E11)\)\.

17:if

ρ⁡\(D′\)=1\\rho\(D^\{\\prime\}\)=1and

ℰ;Γ0⊢𝒦AsmD′\(r\):T\\mathcal\{E\};\\Gamma\_\{0\}\\vdash\_\{\\mathcal\{K\}\}\\mathrm\{Asm\}\_\{D^\{\\prime\}\}\(r\):Tthen

18:return

AsmD′​\(r\)\\mathrm\{Asm\}\_\{D^\{\\prime\}\}\(r\)\.

19:endif

## Appendix BProofs of Theoretical Results

This appendix states the execution assumptions and derives the invariant and returned\-proof results used in Section[4\.4](https://arxiv.org/html/2608.26334#S4.SS4)\.

### B\.1Assumptions

Theorem[1](https://arxiv.org/html/2608.26334#Thmtheorem1)uses the following assumptions\.

- \(A1\)The environmentℰ\\mathcal\{E\}and kernel𝒦\\mathcal\{K\}are fixed throughout the execution\. Every target that occurs in the execution is well formed inℰ\\mathcal\{E\}\. Every initial DAG is finite, acyclic, rooted at\(Γ0⊢T\)\(\\Gamma\_\{0\}\\vdash T\), and each accepted edge satisfies Eq\. \([2](https://arxiv.org/html/2608.26334#S3.E2)\)\.
- \(A2\)Every initial library entry\(ℓ,πℓ\)∈ℒ0\(\\ell,\\pi\_\{\\ell\}\)\\in\\mathcal\{L\}\_\{0\}satisfiesℰ⊢𝒦πℓ:ℓ\\mathcal\{E\}\\vdash\_\{\\mathcal\{K\}\}\\pi\_\{\\ell\}:\\ell\.
- \(A3\)Every later DAG is produced bystep𝒦\\mathrm\{step\}\_\{\\mathcal\{K\}\}in Eq\. \([7](https://arxiv.org/html/2608.26334#S4.E7)\)\. Every later library entry is produced byExtract𝒦\\mathrm\{Extract\}\_\{\\mathcal\{K\}\}, which returns a pair\(ℓ,πℓ\)\(\\ell,\\pi\_\{\\ell\}\)only if Lean elaborates the resulting declaration without unresolved metavariables and verifiesℰ⊢𝒦πℓ:ℓ\\mathcal\{E\}\\vdash\_\{\\mathcal\{K\}\}\\pi\_\{\\ell\}:\\ell\. If abstraction, elaboration, or kernel verification fails, no schema is returned\. Archive and library updates follow Algorithm[1](https://arxiv.org/html/2608.26334#alg1)\.

### B\.2Kernel\-grounded invariance

Let𝔇0\\mathfrak\{D\}\_\{0\}contain the initial DAGs; fort\>0t\>0,𝔇t\\mathfrak\{D\}\_\{t\}also contains every challenger accepted during transitions0,…,t−10,\\ldots,t\-1, including challengers later discarded by archive comparison\. See[1](https://arxiv.org/html/2608.26334#Thmtheorem1)

###### Proof\.

We use induction on the transition indextt\. Assumption \(A1\) establishes \(I1\) att=0t=0, and \(A2\) establishes \(I3\)\.

To derive \(I2\), fixD∈𝔇0D\\in\\mathfrak\{D\}\_\{0\}and a closed nodess\. WritewinD​\(s\)=\(s,s1,…,sk\)\\mathrm\{win\}\_\{D\}\(s\)=\(s;s\_\{1\},\\ldots,s\_\{k\}\)and define

hD​\(s\)=\{0,k=0,1\+max1≤i≤k⁡hD​\(si\),k\>0\.h\_\{D\}\(s\)=\\begin\{cases\}0,&k=0,\\\\ 1\+\\displaystyle\\max\_\{1\\leq i\\leq k\}h\_\{D\}\(s\_\{i\}\),&k\>0\.\\end\{cases\}\(19\)Acyclicity makeshD​\(s\)h\_\{D\}\(s\)finite\. IfhD​\(s\)=0h\_\{D\}\(s\)=0, then \(I1\) gives

AsmD​\(s\)=FwinD​\(s\)​\(⋆\)∈𝖯𝗋𝖿ℰ​\(s\)\.\\mathrm\{Asm\}\_\{D\}\(s\)=F\_\{\\mathrm\{win\}\_\{D\}\(s\)\}\(\\star\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\)\.\(20\)ForhD​\(s\)\>0h\_\{D\}\(s\)\>0, everysis\_\{i\}has smaller height\. The inner induction givespi=AsmD​\(si\)∈𝖯𝗋𝖿ℰ​\(si\)p\_\{i\}=\\mathrm\{Asm\}\_\{D\}\(s\_\{i\}\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\_\{i\}\), so

AsmD​\(s\)=FwinD​\(s\)​\(p1,…,pk\)∈𝖯𝗋𝖿ℰ​\(s\)\.\\mathrm\{Asm\}\_\{D\}\(s\)=F\_\{\\mathrm\{win\}\_\{D\}\(s\)\}\(p\_\{1\},\\ldots,p\_\{k\}\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(s\)\.\(21\)This proves \(I2\) att=0t=0\.

Assume \(I1\)–\(I3\) at indextt\. Ifstep𝒦\(D,δ\)=⊥\\mathrm\{step\}\_\{\\mathcal\{K\}\}\(D,\\delta\)=\\bot, Algorithm[1](https://arxiv.org/html/2608.26334#alg1)updates only the error store\. Therefore

Σt\+1=Σt,ℒt\+1=ℒt,𝔇t\+1=𝔇t\.\\Sigma\_\{t\+1\}=\\Sigma\_\{t\},\\qquad\\mathcal\{L\}\_\{t\+1\}=\\mathcal\{L\}\_\{t\},\\qquad\\mathfrak\{D\}\_\{t\+1\}=\\mathfrak\{D\}\_\{t\}\.\(22\)All three invariants follow immediately\.

Suppose instead thatstep𝒦​\(D,δ\)=D′\\mathrm\{step\}\_\{\\mathcal\{K\}\}\(D,\\delta\)=D^\{\\prime\}\. By Eq\. \([7](https://arxiv.org/html/2608.26334#S4.E7)\),D⪯D′D\\preceq D^\{\\prime\}and the new edge has a checked realizer\. All old edges retain their realizers, so \(I1\) holds for

𝔇t\+1=𝔇t∪\{D′\}\.\\mathfrak\{D\}\_\{t\+1\}=\\mathfrak\{D\}\_\{t\}\\cup\\\{D^\{\\prime\}\\\}\.\(23\)Apply the height induction in Eqs\. \([19](https://arxiv.org/html/2608.26334#A2.E19)\)–\([21](https://arxiv.org/html/2608.26334#A2.E21)\) to every closed node ofD′D^\{\\prime\}\. Its witnessing edges are either old edges, covered by the outer induction hypothesis, or the new edge, covered by Eq\. \([7](https://arxiv.org/html/2608.26334#S4.E7)\)\. Hence \(I2\) holds forD′D^\{\\prime\}and remains true for every DAG in𝔇t\\mathfrak\{D\}\_\{t\}\.

The library update is

ℒt\+1=ℒt∪Extract𝒦​\(D,D′\)⊇ℒt\.\\mathcal\{L\}\_\{t\+1\}=\\mathcal\{L\}\_\{t\}\\cup\\mathrm\{Extract\}\_\{\\mathcal\{K\}\}\(D,D^\{\\prime\}\)\\supseteq\\mathcal\{L\}\_\{t\}\.\(24\)Every extracted pair satisfies Eq\. \([14](https://arxiv.org/html/2608.26334#S4.E14)\), so \(I3\) is preserved\. Equation \([11](https://arxiv.org/html/2608.26334#S4.E11)\) stores eitherD′D^\{\\prime\}or the previous valid incumbent\. This completes the outer induction\. ∎

### B\.3Validity of returned proofs

See[1](https://arxiv.org/html/2608.26334#Thmcorollary1)

###### Proof\.

The return guard in Algorithm[1](https://arxiv.org/html/2608.26334#alg1), the equivalence in Eq\. \([10](https://arxiv.org/html/2608.26334#S4.E10)\), and Theorem[1](https://arxiv.org/html/2608.26334#Thmtheorem1)\(I2\) give

ρ⁡\(D′\)=1⟹ClosedD′​\(r\)⟹AsmD′​\(r\)∈𝖯𝗋𝖿ℰ​\(r\)\.\\rho\(D^\{\\prime\}\)=1\\Longrightarrow\\mathrm\{Closed\}\_\{D^\{\\prime\}\}\(r\)\\Longrightarrow\\mathrm\{Asm\}\_\{D^\{\\prime\}\}\(r\)\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(r\)\.\(25\)The algorithm returnsp=AsmD′​\(r\)p=\\mathrm\{Asm\}\_\{D^\{\\prime\}\}\(r\)\. By Eq\. \([1](https://arxiv.org/html/2608.26334#S3.E1)\),

p∈𝖯𝗋𝖿ℰ\(Γ0⊢T\)⟹ℰ;Γ0⊢𝒦p:T\.p\\in\\mathsf\{Prf\}\_\{\\mathcal\{E\}\}\(\\Gamma\_\{0\}\\vdash T\)\\Longrightarrow\\mathcal\{E\};\\Gamma\_\{0\}\\vdash\_\{\\mathcal\{K\}\}p:T\.\(26\)∎

## Appendix CSetup of Open\-weight Models

This appendix gives the setup for the test\-time compute scaling study in Section[5\.5](https://arxiv.org/html/2608.26334#S5.SS5)\. The study uses the ProofEvolve mechanism from Section[4](https://arxiv.org/html/2608.26334#S4)and varies the base model and composite per\-target budget\. Each reported proof elaborates in the frozen Lean 4 environment with the matched Mathlib commit\. It contains no unresolved metavariables or placeholders, does not usenative\_decide, and passes an independent\#print axiomscheck\. We use seeds\{19,36,65\}\\\{19,36,65\\\}\.

#### Target set\.

The scheduled evaluation manifest contains485485targets from the benchmarks in Table[1](https://arxiv.org/html/2608.26334#S4.T1): PutnamBench \(326326\), IMO\-LeanProofBench \(6060\), and CombiBench \(9999\)\. Each target is scheduled with all three seeds\.

#### Models and serving\.

All open\-weight serving ran on the computation nodes with8×8\\timesNVIDIA B200 GPUs \(192192GB HBM each\), dual\-socket Intel Xeon hosts \(224224vCPUs, about3\.93\.9TB RAM\), running Ubuntu 22\.04\.5 LTS \(kernel6\.8\.0\-1040\-gcp\) with CUDA 12\.8\. We serve under Python 3\.11\.15 with two engines: vLLM 0\.19\.0 \(PyTorch 2\.10\.0\+cu128\) for the Qwen models and SGLang 0\.5\.10 \(PyTorch 2\.9\.1\+cu128\) for GLM\-5\.1, Kimi\-K2\.6, and gpt\-oss\-120b\. Per\-model tensor parallelism is listed in Table[2](https://arxiv.org/html/2608.26334#A3.T2)\. Proof verification uses Lean 4\.29\.1 with Mathlib commit5e932f97and pantograph 0\.3\.15\. Proprietary baselines \(Claude Opus 4\.8\) are accessed through the vendor API\. The headline results in Table[1](https://arxiv.org/html/2608.26334#S4.T1)therefore use API inference plus local Lean kernel verification and do not consume the B200 cluster\.

#### Decoding\.

Table[2](https://arxiv.org/html/2608.26334#A3.T2)gives the decoding parameters, which remain fixed across budget scales\. The per\-call output cap is32,76832\{,\}768tokens for every run\.

Table 2:Self\-hosted fixed\-weight models and their serving and decoding settings\. TP denotes tensor parallelism per replica, and dashes mark parameters left at their vendor defaults\. Qwen instant modes use a presence penalty of1\.51\.5, compared with00in thinking mode\. For gpt\-oss\-120b, we vary the reasoning effort\.
#### Composite budget\.

The profiles\{0\.25,0\.5,1,2\}×\\\{0\.25,0\.5,1,2\\\}\\timesjointly scale four hard caps relative to the1×1\\timesreference in Table[3](https://arxiv.org/html/2608.26334#A3.T3): model calls, Lean calls, tokens, and wall\-clock time\. The mechanism, decoding parameters, and verification procedure remain fixed\. Because all four caps change together, the study does not isolate the effect of any one resource\.

Table 3:Per\-target composite budget profiles\. Each row gives four hard caps\. “Tokens” is the combined input\+\+output allowance; the per\-call output cap remains32,76832\{,\}768\.

## Appendix DResults of Test\-Time Budget Scaling

#### Search activity\.

Table[4](https://arxiv.org/html/2608.26334#A4.T4)reports mean kernel\-verified transitions per target for each seed in\{19,36,65\}\\\{19,36,65\\\}\. Figure[6](https://arxiv.org/html/2608.26334#S5.F6)a plots the target\-weighted mean across the three seeds\. Among recorded outcomes, seven of the eight configurations increase monotonically with budget in every seed\. Low\-effort gpt\-oss\-120b remains near zero\. The number of recorded outcomes decreases for some runs in thinking mode at larger budgets\. For example, Qwen3\.5\-397B in thinking mode hasn=1441/1428/1359/1271n=1441/1428/1359/1271recorded target–seed outcomes at0\.25/0\.5/1/2×0\.25/0\.5/1/2\\times\. The reported values are target\-weighted over recorded outcomes\.

#### Parser coverage\.

The proof\-state S\-expression parser deliberately does not support the AST forms:mv,:mvd,:subst, and:proj\. When the parser encounters one of these forms, the runner exits before writing a terminal outcome\. These exits occur more often in deeper searches, so missing outcome records become more frequent as the budget grows\. Means computed only from recorded outcomes may therefore be biased upward at larger budgets\. We treat the curves as descriptive search activity, not as unbiased estimates for the full manifest or measures of proposal efficiency\.

Table 4:Mean kernel\-verified transitions per target, with entries ordered asseed 19 / seed 36 / seed 65\. Figure[6](https://arxiv.org/html/2608.26334#S5.F6)a plots the target\-weighted mean across the three seeds\. These counts measure cumulative verified search activity, not unique proofs or solve rates\.
#### Solves\.

Table[5](https://arxiv.org/html/2608.26334#A4.T5)reports both solve events and distinct target coverage\. Between0\.25×0\.25\\timesand2×2\\times, the number of solve events rises from2828to4444, while the union of solved targets rises from22to1010\. Kimi\-K2\.6 and the two Qwen3\.5 modes account for most of the endpoint increase\. Four targets are solved at2×2\\timesbut not at a lower budget:brualdi\_ch10\_31,brualdi\_ch1\_10,hackmath\_4, andputnam\_1977\_a5\. The budget arms are separate stochastic runs, and the number of recorded outcomes varies with budget\. These counts describe observed coverage; they do not establish monotone per\-model scaling or isolate the effect of any one resource\.

ModelMode0\.25×0\.25\\times0\.5×0\.5\\times1×1\\times2×2\\timesQwen3\.5\-397Bthinking33445599Qwen3\.5\-397Binstant33333366Qwen3\.6\-35Binstant33334433Qwen3\.6\-35Bthinking44333344GLM\-5\.1instant33445533Kimi\-K2\.6instant3377991111gpt\-oss\-120bmedium66556666gpt\-oss\-120blow33330022All eight configurations: solve events2828323235354444Union of solved targets2266661010Table 5:Final kernel\-verified outcomes across seeds\{19,36,65\}\\\{19,36,65\\\}\. A solve event is one run for a particular model, mode, seed, and target that returns a valid proof\. Repeated solutions of the same target count separately\. The last row counts target identifiers solved at least once\. Budget columns correspond to separate runs rather than cumulative prefixes\.
#### Solved\-target inventory\.

Across all budgets and seeds, the open\-weight runs solve1111distinct targets:44from PutnamBench and77from CombiBench\. None is from IMO\-LeanProofBench\. Table[6](https://arxiv.org/html/2608.26334#A4.T6)gives the model, budget, and search statistics for one representative run per target\. All five models solvebrualdi\_ch14\_33\. The listed solves forputnam\_2012\_a2andputnam\_1977\_a5occur only at the larger budgets\.

Table 6:The1111distinct targets solved in the open\-weight runs\. For one representative run per target, “Trans\.” gives kernel\-verified transitions, “Calls” gives model calls, and “Lean” gives kernel calls\. Every listed run reachesρ=1\\rho=1\. Medium\-effort gpt\-oss\-120b also solvesbrualdi\_ch14\_33andbrualdi\_ch7\_7\. Appendix[E](https://arxiv.org/html/2608.26334#A5)gives the corresponding proofs\.
#### Re\-verification\.

We re\-verify every solve in the frozen Lean 4\.29\.1 environment with Mathlib commit5e932f97\. Each returned proof term is elaborated from scratch, and\#print axiomsenumerates its axiom dependencies\. All139139kernel\-verified solve events have a stored closing proof, with no reportedρ=1\\rho=1lacking one\. Every proof depends only on\{propext,Classical\.choice,Quot\.sound\}\\\{\\texttt\{propext\},\\ \\texttt\{Classical\.choice\},\\ \\texttt\{Quot\.sound\}\\\}, and none usesnative\_decide\. Re\-verification found00false positives\.

#### Verified substrate\.

In addition to Mathlib, the ProofEvolve environmentℰ\\mathcal\{E\}contains the library of158158kernel\-verified lemmas\. The library has no occurrences ofsorryand introduces no axioms beyond the standard three\. A proof that uses one of these lemmas therefore has the same axiom footprint as a proof built directly on Mathlib\. During re\-verification, we inline the library so that\#print axiomschecks its dependencies transitively\. The proof ofputnam\_1977\_a5in Appendix[E](https://arxiv.org/html/2608.26334#A5)uses one lemma from this library\.

#### Comparison with agentic baselines\.

We also evaluate pass@1616, escalating whole\-proof search, ReAct, LEAP, Hilbert, and ProofEvolve on a fixed random subset shared across models\. All methods solve few targets with these open\-weight models, so we draw no quantitative cross\-method conclusion from this subset\. Verified closure and kernel\-verified transition counts are specific to ProofEvolve’s DAG and do not support a comparison with the other methods\. Table[1](https://arxiv.org/html/2608.26334#S4.T1), which uses Claude Opus 4\.8 on the full benchmarks, provides the matched solve\-rate comparison\.

## Appendix EKernel\-Certified Open\-Weight Proofs on PutnamBench and CombiBench

This appendix gives the kernel\-certified proofs for all1111distinct open\-weight solves in Table[6](https://arxiv.org/html/2608.26334#A4.T6)\. We verify them as described in Appendix[D](https://arxiv.org/html/2608.26334#A4)\. Each theorem name is its benchmark target identifier\. The caption records the solving model and the kernel\-verified transitions and model calls for one solving run\.

### E\.1PutnamBench

importMathlib

importProofLib

openMatrix

theoremputnam\_2012\_a2

\(S:Type\*\)\[CommSemigroupS\]

\(abc:S\)

\(hS:∀xy:S,∃z:S,x\*z=y\)

\(habc:a\*c=b\*c\)

:a=b:=by

obtain⟨z,hz⟩:=hSca

obtain⟨e,he⟩:=hScc

haveh\_id:∀x:S,x\*e=x:=by

introx

obtain⟨w,hw⟩:=hScx

calc

x\*e=\(c\*w\)\*e:=byrw\[hw\]

\_=c\*\(w\*e\):=byrw\[mul\_assoc\]

\_=c\*\(e\*w\):=byrw\[mul\_commwe\]

\_=\(c\*e\)\*w:=byrw\[mul\_assoc\]

\_=c\*w:=byrw\[he\]

\_=x:=byrw\[hw\]

obtain⟨d,hd⟩:=hSce

exactcalc

a=a\*e:=byrw\[h\_ida\]

\_=a\*\(c\*d\):=byrw\[hd\]

\_=\(a\*c\)\*d:=byrw\[mul\_assoc\]

\_=\(b\*c\)\*d:=byrw\[habc\]

\_=b\*\(c\*d\):=byrw\[mul\_assoc\]

\_=b\*e:=byrw\[hd\]

\_=b:=byrw\[h\_idb\]

right cancellation in a commutative semigroup satisfying the stated divisibility condition\. The proof first establishes∀x,x∗e=x\\forall x,\\ x\*e=xand then uses this identity in the cancellation argument\.

importMathlib

importProofLib

openRingHomSetNat

theoremputnam\_1977\_a5

\(pmn:ℕ\)

\(hp:Nat\.Primep\)

\(hmgen:m≥n\)

:\(choose\(p\*m\)\(p\*n\)≡choosemn\[MODp\]\):=by

rw\[Nat\.ModEq\]

haveI:Fact\(Nat\.Primep\):=⟨hp⟩

rw\[Choose\.choose\_modEq\_choose\_mod\_mul\_choose\_div\_nat\]

simp\[Nat\.mul\_mod,Nat\.mul\_div\_cancel\_left,Nat\.choose\_zero\_right,Nat\.mod\_eq\_of\_lt\]

simp\[Nat\.mul\_div\_cancel\_left,Nat\.Prime\.poshp\]

the Lucas\-type congruence\(p​mp​n\)≡\(mn\)\(modp\)\\binom\{pm\}\{pn\}\\equiv\\binom\{m\}\{n\}\\pmod\{p\}\. The proof applies app\-adic binomial congruence lemma from ProofLib and finishes withsimp\.

importMathlib

importProofLib

openSetFilterTopology

theoremputnam\_1988\_b1

:∀a≥2,∀b≥2,∃xyz:ℤ,x\>0∧y\>0∧z\>0∧a\*b=x\*y\+x\*z\+y\*z\+1:=by

introahabhb;use1,a\-1,b\-1;constructor;norm\_num;constructor;linarith;constructor;linarith;ring

every producta​babwitha,b≥2a,b\\geq 2equalsx​y\+x​z\+y​z\+1xy\+xz\+yz\+1for positive integersx,y,zx,y,z\. The proof setsx=1x=1,y=a−1y=a\-1, andz=b−1z=b\-1, then finishes withlinarithandring\.

importMathlib

importProofLib

openTopologyFilter

theoremputnam\_2001\_a1

\(S:Type\*\)

\[MulS\]

\(hS:∀ab:S,\(a\*b\)\*a=b\)

:∀ab:S,a\*\(b\*a\)=b:=by

introab

haveh:=hSba;haveh2:=hS\(b\*a\)b;rw\[h\]ath2;exacth2

if a magma satisfies\(a∗b\)∗a=b\(a\*b\)\*a=bfor alla,ba,b, thena∗\(b∗a\)=ba\*\(b\*a\)=b\. The proof instantiates the hypothesis twice and rewrites once\.

### E\.2CombiBench

importMathlib

theoremhackmath\_4:IsLeast\{n\|∀f:Finn→Fin12,∃ab,a≠b∧fa=fb\}\(\(13\):ℕ\):=by

constructor

·–Show13isintheset

introf

haveh1:Fintype\.card\(Fin13\)=13:=bysimp

haveh2:Fintype\.card\(Fin12\)=12:=bysimp

haveh3:Fintype\.card\(Fin13\)\>Fintype\.card\(Fin12\):=byrw\[h1,h2\];norm\_num

obtain⟨a,b,hab,heq⟩:=Fintype\.exists\_ne\_map\_eq\_of\_card\_ltfh3

exact⟨a,b,hab,heq⟩

·–Show13istheleastelementintheset

intronhn

by\_contrah

push\_negath

haveh4:n≤12:=byomega

haveh5:∃f:Finn↪Fin12,True:=by

haveh6:Fintype\.card\(Finn\)≤Fintype\.card\(Fin12\):=by

simp

omega

haveh7:Nonempty\(Finn↪Fin12\):=Function\.Embedding\.nonempty\_of\_card\_leh6

obtain⟨f⟩:=h7

exact⟨f,trivial⟩

obtain⟨f,\_⟩:=h5

haveh7:∀ab,a≠b→fa≠fb:=by

introabhab

exactf\.injective\.nehab

haveh8:=hnf

obtain⟨a,b,hab,heq⟩:=h8

haveh9:fa≠fb:=h7abhab

contradiction

1313is the least group size that forces two people into the same month\. The proof establishes membership withFintype\.exists\_ne\_map\_eq\_of\_card\_ltand minimality by constructing an embedding forn≤12n\\leq 12\.

importMathlib

structureIsMagicSquare\{n:ℕ\}\(M:Matrix\(Finn\)\(Finn\)ℕ\):Propwhere

mem:∀ij,Mij∈Finset\.Icc1\(n\*n\)

pairwise:∀iji’j’,i≠i’∨j≠j’→Mij≠Mi’j’

same\_sum:∃s,\(∀i,∑j,Mij=s\)∧\(∀j,∑i,Mij=s\)∧\(∑i,Mii\.rev=s\)∧∑i,Mii=s

theorembrualdi\_ch1\_10:¬∃\(M:Matrix\(Fin2\)\(Fin2\)ℕ\),IsMagicSquareM:=by

introh

rcaseshwith⟨M,hM⟩

rcaseshMwith⟨h\_rows,h\_cols,h\_diag,h\_anti,h\_pairwise⟩

haveh1:=h\_rows00

haveh2:=h\_rows01

haveh3:=h\_rows10

haveh4:=h\_rows11

haveh5:=h\_cols0001\(Or\.inr\(bydecide\)\)

haveh6:=h\_cols0010\(Or\.inl\(bydecide\)\)

haveh7:=h\_cols0011\(Or\.inl\(bydecide\)\)

haveh8:=h\_cols0110\(Or\.inl\(bydecide\)\)

haveh9:=h\_cols0111\(Or\.inl\(bydecide\)\)

haveh10:=h\_cols1011\(Or\.inr\(bydecide\)\)

simp\[Finset\.mem\_Icc\]ath1h2h3h4

haveh\_row0:=h\_anti0

haveh\_row1:=h\_anti1

haveh\_col0:=h\_pairwise\.10

haveh\_col1:=h\_pairwise\.11

haveh\_diag1:=h\_pairwise\.2\.2

haveh\_anti\_diag:=h\_pairwise\.2\.1

simp\[Fin\.sum\_univ\_two,Fin\.rev\]ath\_row0h\_row1h\_col0h\_col1h\_diag1h\_anti\_diag

omega

no order\-22magic square exists\. The proof states the range, distinctness, and row, column, and diagonal sum constraints, then solves the resulting integer system withomega\.

importMathlib

theorembrualdi\_ch7\_7\(mnd:ℕ\+\)\(hmd:d=Nat\.gcdmn\):

Nat\.gcd\(Nat\.fibm\)\(Nat\.fibn\)=Nat\.fibd:=by

haveh1:\(Nat\.fib↑m\)\.gcd\(Nat\.fib↑n\)=Nat\.fib\(Int\.gcd\(↑m:ℤ\)\(↑n:ℤ\)\):=byrw\[←Int\.gcd\_fib\(↑m:ℤ\)\(↑n:ℤ\)\];simp

rw\[hmd\]

simp\[hmd\]ath1⊢;exacth1

gcd⁡\(Fm,Fn\)=Fgcd⁡\(m,n\)\\gcd\(F\_\{m\},F\_\{n\}\)=F\_\{\\gcd\(m,n\)\}for Fibonacci numbers\. The proof converts between theℕ\\mathbb\{N\}andℤ\\mathbb\{Z\}formulations and applies the library identity\.

importMathlib

theorembrualdi\_ch8\_6\(n:ℕ\)\(h:ℕ→ℝ\)\(h’:∀i,hi=2\*i^2\-i\+3\):

∑i∈Finset\.range\(n\+1\),hi=\(\(funn=\>\(\(n\+1\)\*\(4\*n^2\-n\+18\)/6\)\):ℕ→ℝ\)n:=by

inductionnwith

\|zero=\>

simp\[Finset\.sum\_range\_succ,h’\]

all\_goalsnorm\_num

\|succnih=\>

rw\[Finset\.sum\_range\_succ,ih\]

simp\[h’\]

ring\_nf

<;\>field\_simp

<;\>ring\_nf

<;\>norm\_num

<;\>ring

the closed form∑k=0n\(2​k2−k\+3\)=\(n\+1\)​\(4​n2−n\+18\)6\\sum\_\{k=0\}^\{n\}\(2k^\{2\}\-k\+3\)=\\tfrac\{\(n\+1\)\(4n^\{2\}\-n\+18\)\}\{6\}, proved by induction\.

importMathlib

theorembrualdi\_ch14\_33\{α:Type\*\}\[Fintypeα\]\[DecidableEqα\]\(σ:Equiv\.Permα\):

σ\.cycleType=σ⁻¹\.cycleType:=by

rw\[Equiv\.Perm\.cycleType\_inv\]

a permutation and its inverse have the same cycle type\. The proof applies the library identityEquiv\.Perm\.cycleType\_inv; all five models solve this target\.

importMathlib

openFinset

theorembrualdi\_ch2\_11:

\(\(Icc\(1:ℕ\)20\)\.powersetCard3\|\>\.filter\(funS=\>∀a∈S,a\-1∉S∧a\+1∉S\)\)\.card=

\(\(816\):ℕ\):=by

set\_optionmaxRecDepth1000000indecide

there are816816size\-33subsets of\{1,…,20\}\\\{1,\\dots,20\\\}with no two consecutive elements\. The kernel tacticdecideverifies the count withoutnative\_decide\.

importMathlib

defisDifferenceSet\(n:ℕ\)\(B:Finset\(ZModn\)\):Prop:=

∃k,∀x:\(ZModn\),x≠0→∑i∈B,∑j∈B\\\{i\},List\.countx\[i\-j\]=k

theorembrualdi\_ch10\_31:isDifferenceSet21\{0,3,4,9,11\}:=by

dsimponly\[isDifferenceSet\]

use1;decide

\{0,3,4,9,11\}\\\{0,3,4,9,11\\\}is a difference set inℤ21\\mathbb\{Z\}\_\{21\}\. The proof supplies the multiplicity witness and uses the kernel tacticdecide, notnative\_decide\.

## Appendix FDetailed Setup for the Lean Workbook Study

This appendix records the corpus, library construction, screening, retrieval and evaluation used in Section[5\.6](https://arxiv.org/html/2608.26334#S5.SS6)\.

### F\.1Corpus and verification

We use theorem statements from Lean Workbook\([Ying et al\., 2024](https://arxiv.org/html/2608.26334#bib.bib54)\)and the machine\-generated proofs released by Goedel\-Prover\([Lin et al\., 2025a](https://arxiv.org/html/2608.26334#bib.bib24)\)\. We re\-elaborate every candidate in a fixed Lean 4 environment\([de Moura and Ullrich, 2021](https://arxiv.org/html/2608.26334#bib.bib11)\)with a matched Mathlib commit\([The mathlib Community, 2020](https://arxiv.org/html/2608.26334#bib.bib42)\), under the same acceptance criteria used throughout the paper: an accepted proof has no unresolved metavariables or placeholders, passes the Lean kernel at the stated type, and a restricted\#print axiomscheck must show dependencies only onpropext,Classical\.choiceandQuot\.sound\. We reject proofs that usenative\_decidebecause its code generation path introduces an axiom outside the standard kernel\. Each candidate runs in a fresh process with a300300\-second timeout\. This verification retains20,55420\{,\}554statement and proof pairs\.

### F\.2Deduplication and the evaluation split

Lean Workbook contains many restatements of the same theorem, so we deduplicate before splitting\. We generate candidate pairs with MinHash LSH over statement shingles using128128permutations,3232bands of44rows, seed2026080620260806and an approximate threshold of0\.420\.42\. This produces2,362,9462\{,\}362\{,\}946candidate pairs\. We confirm each pair with direct similarity tests or a guarded signature match\. The direct tests use alpha equivalence of the elaborated statement, statementnn\-gram Jaccard above0\.80\.8and docstringnn\-gram Jaccard above0\.80\.8\. The guarded match requires signature Jaccard above0\.950\.95over at least five symbols and statement Jaccard above0\.60\.6\. We disable the dense embedding channel for deduplication because transitive embedding matches can join distinct theorems into one cluster\. The exact tests retain26,33026\{,\}330edges and5,2165\{,\}216multi\-theorem clusters\. The largest cluster contains106106theorems\. Removing6,9356\{,\}935alpha\-exact duplicates and2,6512\{,\}651near duplicates leaves10,96810\{,\}968representatives, a46\.6%46\.6\\%reduction\. A fixed seed assigns1,0001\{,\}000theorems to evaluation and9,9689\{,\}968to the source stream\. A post\-split audit checks the boundary again for residual near duplicates\.

### F\.3Leakage screening

The exact tests can still miss the same theorem written in a different form\. Five independent language\-model judges therefore screen each evaluation theorem against its6464nearest library neighbors\. A judge flags a residual near duplicate when a neighbor states the same theorem up to renaming or a change of constants\. We record every verdict and its reason, then exclude a theorem when at least two judges flag it\. The screen removes256256theorems, or25\.6%25\.6\\%, and leaves the744744used throughout the study\. Screening occurs before condition outcomes are compared, and every condition uses the same evaluation set\.

The panel is five Claude models spanning four releases \(claude\-opus\-5,claude\-opus\-4\.8,claude\-opus\-4\.7,claude\-opus\-4\.6andclaude\-sonnet\-5\), each queried once per evaluation theorem at medium reasoning effort\. Verdicts are independent across models but not across model families\. Flag counts over the1,0001\{,\}000candidates are624624,120120,5757,3737,5656and106106for zero through five flags\. Agreement is therefore bimodal:730730theorems, or73\.0%73\.0\\%, receive a unanimous verdict, and only9494fall in the two\-to\-three\-flag band where the threshold is decisive\. Raising the threshold to three flags would retain801801theorems instead of744744\. Promptgives the template; each judge sees only the evaluation theorem and its retrieved neighbors\.

YouareaLEAKAGEauditorforaheld\-outLeantheorem\-provingbenchmark\.Read

ONLYtherecordforthisevaluationtheorem\(asingleJSONobjectwith

holdout\_statement,holdout\_docstring,anda”retrieved”array–eachitemhas

statement\+proof\_body\+docstring\)\.DoNOTreadanyotherfile\.

RuleLEAKifANYretrieveditemisaNEAR\-DUPLICATEoftheholdout\(thesame

problemuptovariablerenaming/constantchanges/trivialrewrite\)OR

directlycontainstheholdout’sansweroraproofthatwouldtransferby

copying\(memorization,notreasoning\)\.

RuleCLEANiftheretrieveditemsareonlyrelated\-but\-distinct\(sametechnique

/topic,genuinelydifferentproblem\)\.

Givetheverdict\+aone\-sentencereason\.

### F\.4Verified theorem schema library

The base model attempts every buildable theorem in the9,9689\{,\}968\-theorem source stream once under the same one\-shot budget used for evaluation\. Target files cannot be built for384384theorems\. Of the remaining9,5849\{,\}584, the kernel and axiom audit accept5,5465\{,\}546proofs\. The self\-solve rate is57\.9%57\.9\\%over scoreable theorems and55\.6%55\.6\\%over the full source stream\. These5,5465\{,\}546theorem and proof pairs form the persistent verified theorem schema library\. Every entry contains a proof written by the base model and checked by Lean\. No human proof or released Goedel\-Prover proof enters the library\. Unlike ProofLib, whose lemmas are installed inℰ\\mathcal\{E\}and therefore enter the axiom footprint of any proof that uses them \(Appendix[D](https://arxiv.org/html/2608.26334#A4)\), this library is a retrieval corpus only: its entries never enter the Lean environment and never appear in any proof’s axiom footprint\. The library\-size conditions use nested subsets drawn once with a fixed seed, so the1,0001\{,\}000\-proof library is contained in the2,0002\{,\}000\-proof library, which is contained in the4,0004\{,\}000\-proof library\.

### F\.5Semantic retrieval

The semantic retriever embeds theorem statements withbge\-large\-en\-v1\.5\. Raw cosine similarities occupy a narrow band because the corpus contains many competition\-style algebra and inequality theorems\. We subtract the library mean from each vector before computing cosine similarity\. The encoder uses asymmetric instructions\. Evaluation queries carry the prefixRepresent this sentence for searching relevant passages:, while library entries are embedded without a prefix\. Cosine scores are rounded to two decimal places, with lexical statement Jaccard breaking ties\. The rank excludes the symbol and type signature channel because it saturates at1\.01\.0on this corpus\. Retrieval is deterministic, so each run receives the sameKKlibrary entries for a given theorem\.

### F\.6Base model, serving and decoding

The base model is Qwen3\.5\-397B\-A17B in FP8\([Qwen Team, 2026a](https://arxiv.org/html/2608.26334#bib.bib36)\), the same open\-weight model used in the test\-time scaling study of Appendix[C](https://arxiv.org/html/2608.26334#A3), but served differently here\. We serve it with SGLang rather than vLLM, at tensor\-parallel size88rather than44\. Each replica uses eight B200 GPUs, a context window of65,53665\{,\}536tokens and GPU memory utilization of0\.920\.92\. A client distributes requests across1616replicas and retries transport errors on the next live replica\. The model runs in its default thinking mode without a chat\-template argument\. Library construction and all evaluation conditions use one decoding profile pinned by hash: temperature0\.60\.6, top\-pp0\.950\.95, top\-kk2020, min\-pp0\.00\.0, presence penalty0\.00\.0, repetition penalty1\.01\.0, and a client\-side limit of32,76832\{,\}768output tokens\. We do not pin a decode seed\. The three runs are independent samples from the decoder, and the reported standard deviation measures variation across these runs\.

### F\.7Prompt

All three conditions use one template containing a system prefix, the target, base premises, worked examples and previous attempts\. Only the worked\-examples section changes\. Zero\-shot renders this section asNone available\.rather than omitting it\. Base premises and previous attempts are empty in every condition, so the schema library is the only source of retrieved proof knowledge\. Each schema is rendered as a compilable Leanexamplewith its theorem statement and the proof body accepted by Lean\.

\[system\]

YouareprovingatheoreminLean4withMathlib\.

Replywithasinglefenced“‘leanblockcontainingONLYthetacticblock

thatcompletesthegiventheorem\.Donotrestatethetheorem,donotadd

imports,anddonotdeclareanythingatthetoplevel:thesurroundingfile

isfixedandyourreplyisinsertedafter‘:=by‘\.

Ifyoucannotclosethegoal,stillreplywithyourbesttacticblock\.

Neveremit‘sorry‘\.

\[user\]

\#\#Target

Thefilebelowisfrozen\.Yourtacticblockisinsertedwheremarked\.

“‘lean

importMathlib

theorem<name\><statement\>:=by

<yourtacticblockhere\>

“‘

\#\#Proofstate

Oneopenobligation:thetheoremstatementabove\.

\#\#Basepremises

Noneselectedforthisrequest\.

\#\#Workedexamples

Solvedproblemsfromyourownlibrary,forreference\.Theyaredifferent

problems;adaptthetechniques,donotcopy\.

\#\#\#Example1

“‘lean

example<librarystatement1\>:=by

<verifiedproofbody1\>

“‘

…\(Kexamples\)

\#\#Previousattempts

None\.

### F\.8Conditions, budget and compute

Every condition gives one attempt per theorem with no self\-repair or second sample\. The Lean environment imports Mathlib\. Relevant retrieval usesK∈\{8,16,32,64\}K\\in\\\{8,16,32,64\\\}over the full library\. We also evaluate library sizes\{1,000,2,000,4,000,full\}\\\{1\{,\}000,\\,2\{,\}000,\\,4\{,\}000,\\,\\text\{full\}\\\}atK=8K\{=\}8\. Random retrieval usesK=8K\{=\}8with a fixed draw seed for each run\. We run all nine configurations three times over the same1,0001\{,\}000evaluation candidates, then score the common744744\-theorem screened subset in every condition\. Every run produces one record per candidate\. Condition contrasts are computed as paired differences across matched runs\.

For the copy rate in Section[5\.6](https://arxiv.org/html/2608.26334#S5.SS6), we remove comments and normalize whitespace in every accepted proof body\. We then compare it with the eight proof bodies shown for that theorem\. For each run index, we count cases where relevant retrieval closes a theorem and the corresponding zero\-shot run leaves it open\.

The fleet contains1616FP8 replicas of88B200 GPUs each, or128128B200 GPUs in total\. Building the library over9,9689\{,\}968source theorems takes about five hours of fleet time\. A three\-run sweep of one configuration takes about seven hours\. The complete study uses a few thousand B200\-GPU\-hours across library construction, the depth and size sweeps and leakage screening\.

Table 7:Solve rate on the744744screened evaluation theorems\. We report the mean over three independent runs, and the±\\pmfigure is the run\-to\-run standard deviation*of the solve rate*\. Lift is the paired difference from zero\-shot, computed per run before rounding, so it need not equal the difference of the two rounded means\.

## Appendix GRetrieval\-to\-Proof Traces on Lean Workbook

Section[5\.6](https://arxiv.org/html/2608.26334#S5.SS6)reports that322322of the351351theorems closed by relevant retrieval and left open by zero\-shot, or91\.7%91\.7\\%, do not reproduce any shown proof verbatim\. That is an aggregate\. This appendix gives the individual form of it: two complete traces from the evaluation theorem, through what the retriever actually returned, to the proof Lean accepted\. Each trace runs through five stages\.\(1\)the evaluation theorem and why it is not immediate;\(2\)two of the eight schemas the retriever placed in the proposal context;\(3\)the proof the model produced and the kernel accepted;\(4\)a comparison with the reference proof released with Lean Workbook, which shows the two take different routes; and\(5\)the outcome of all three conditions over the three runs\. The selected Lean statements preserve the informal problem and avoid truncated natural\-number arithmetic, inconsistent assumptions and trivial goals\.

Example 1\. A bound on\[0,1\]\[0,1\]\(1\) Target\.For0≤x≤10\\leq x\\leq 1, show that\|x⁡\(x−1\)​\(x6\+2​x4\+3​x2\+4\)\|<5/2\|x\(x\-1\)\(x^\{6\}\+2x^\{4\}\+3x^\{2\}\+4\)\|<5/2\. The two natural factor bounds do not prove the strict inequality: multiplyingx⁡\(1−x\)≤1/4x\(1\-x\)\\leq 1/4andx6\+2​x4\+3​x2\+4≤10x^\{6\}\+2x^\{4\}\+3x^\{2\}\+4\\leq 10gives only≤5/2\\leq 5/2\.[⬇](data:text/plain;base64,KHggOiDihJ0pIChoeCA6IDAg4omkIHgg4oinIHgg4omkIDEpIDoKICB8eCAqICh4IC0gMSkgKiAoeF42ICsgMiAqIHheNCArIDMgKiB4XjIgKyA0KXwgPCA1IC8gMg==)\(x:ℝ\\mathbb\{R\}\)\(hx:0≤\\leqx∧\\wedgex≤\\leq1\):\|x\*\(x\-1\)\*\(x^6\+2\*x^4\+3\*x^2\+4\)\|<5/2\(2\) Retrieved\.Two of the eight schemas placed in the proposal context\. Both are bounds on the same interval, and neither states the target\.[⬇](data:text/plain;base64,ZXhhbXBsZSAoeCA6IOKEnSkgKGh4IDogMCDiiaQgeCDiiKcgeCDiiaQgMSkgOgogICAgMCDiiaQgeCAtIHheMiDiiKcgeCAtIHheMiDiiaQgMS80IDo9IGJ5CiAgY2FzZXMgaHgKICBjb25zdHJ1Y3RvciA8Oz4gbmxpbmFyaXRoIFtzcV9ub25uZWcgKHggLSAxLzIpXQoKZXhhbXBsZSAoeCA6IOKEnSkgKGh4IDogMCDiiaQgeCDiiKcgeCDiiaQgMSkgOgogICAgeCAqICh4IF4gMyAtIDYgKiB4ICsgOSkg4omkIDQgOj0gYnkKICBubGluYXJpdGggW3NxX25vbm5lZyAoeCAtIDEpLCBzcV9ub25uZWcgKHheMiAtIDEpLCBzcV9ub25uZWcgKHheMiAtIHgpLAogICAgbXVsX25vbm5lZyBoeC4xIChzcV9ub25uZWcgKHggLSAxKSksCiAgICBtdWxfbm9ubmVnIChzdWJfbm9ubmVnLm1wciBoeC4yKSAoc3Ffbm9ubmVnICh4IC0gMSkpXQ==)example\(x:ℝ\\mathbb\{R\}\)\(hx:0≤\\leqx∧\\wedgex≤\\leq1\):0≤\\leqx\-x^2∧\\wedgex\-x^2≤\\leq1/4:=bycaseshxconstructor<;\>nlinarith\[sq\_nonneg\(x\-1/2\)\]example\(x:ℝ\\mathbb\{R\}\)\(hx:0≤\\leqx∧\\wedgex≤\\leq1\):x\*\(x^3\-6\*x\+9\)≤\\leq4:=bynlinarith\[sq\_nonneg\(x\-1\),sq\_nonneg\(x^2\-1\),sq\_nonneg\(x^2\-x\),mul\_nonneghx\.1\(sq\_nonneg\(x\-1\)\),mul\_nonneg\(sub\_nonneg\.mprhx\.2\)\(sq\_nonneg\(x\-1\)\)\]\(3\) Generated\.The kernel\-accepted proof\. It determines the sign of the product first, which neither retrieved schema does, and then reuses thesq​\_​nonneg​\(x−1/2\)\\mathrm\{sq\\\_nonneg\}\(x\-1/2\)hint that both of them turn on\.[⬇](data:text/plain;base64,Y2FzZXMgaHggd2l0aAp8IGludHJvIGh4MSBoeDIgPT4KICBoYXZlIGgxIDogeCAqICh4IC0gMSkg4omkIDAgOj0gYnkgbmxpbmFyaXRoCiAgaGF2ZSBoMiA6IHheNiArIDIgKiB4XjQgKyAzICogeF4yICsgNCDiiaUgNCA6PSBieQogICAgbmxpbmFyaXRoIFtwb3dfbm9ubmVnIGh4MSAyLCBwb3dfbm9ubmVnIGh4MSA0LCBwb3dfbm9ubmVnIGh4MSA2XQogIGhhdmUgaDMgOiB4ICogKHggLSAxKSAqICh4XjYgKyAyKnheNCArIDMqeF4yICsgNCkg4omkIDAgOj0gYnkKICAgIG5saW5hcml0aCBbcG93X25vbm5lZyBoeDEgMiwgcG93X25vbm5lZyBoeDEgNCwgcG93X25vbm5lZyBoeDEgNl0KICBydyBbYWJzX29mX25vbnBvcyBoM10KICBubGluYXJpdGggW3NxX25vbm5lZyAoeCAtIDEvMiksIHBvd19ub25uZWcgaHgxIDIsIHBvd19ub25uZWcgaHgxIDMsCiAgICBwb3dfbm9ubmVnIGh4MSA0LCBwb3dfbm9ubmVnIGh4MSA1LCBwb3dfbm9ubmVnIGh4MSA2LAogICAgbXVsX25vbm5lZyBoeDEgKHNxX25vbm5lZyAoeCAtIDEvMikpLAogICAgbXVsX25vbm5lZyAoc3ViX25vbm5lZy5tcHIgaHgyKSAoc3Ffbm9ubmVnICh4IC0gMS8yKSld)caseshxwith\|introhx1hx2=\>haveh1:x\*\(x\-1\)≤\\leq0:=bynlinarithhaveh2:x^6\+2\*x^4\+3\*x^2\+4≥\\geq4:=bynlinarith\[pow\_nonneghx12,pow\_nonneghx14,pow\_nonneghx16\]haveh3:x\*\(x\-1\)\*\(x^6\+2\*x^4\+3\*x^2\+4\)≤\\leq0:=bynlinarith\[pow\_nonneghx12,pow\_nonneghx14,pow\_nonneghx16\]rw\[abs\_of\_nonposh3\]nlinarith\[sq\_nonneg\(x\-1/2\),pow\_nonneghx12,pow\_nonneghx13,pow\_nonneghx14,pow\_nonneghx15,pow\_nonneghx16,mul\_nonneghx1\(sq\_nonneg\(x\-1/2\)\),mul\_nonneg\(sub\_nonneg\.mprhx2\)\(sq\_nonneg\(x\-1/2\)\)\]\(4\) Compared\.The reference proof released with Lean Workbook splits the absolute value into two inequalities without determining the sign of the product\. None of its auxiliary inequalities appears in the accepted proof\.[⬇](data:text/plain;base64,cncgW2Fic19sdF0KY29uc3RydWN0b3IgPDs+CiAgbmxpbmFyaXRoIFtwb3dfbm9ubmVnIChzdWJfbm9ubmVnLm1wciBoeC4xKSAwLCAuLi4sCiAgICAgICAgICAgICBwb3dfbm9ubmVnIChzdWJfbm9ubmVnLm1wciBoeC4xKSA5XQ==)rw\[abs\_lt\]constructor<;\>nlinarith\[pow\_nonneg\(sub\_nonneg\.mprhx\.1\)0,\.\.\.,pow\_nonneg\(sub\_nonneg\.mprhx\.1\)9\]\(5\) Outcome over three runs\.Zero\-shot closes zero runs, relevant retrieval closes two and random retrieval closes one\.

Example 2\. A three\-part symmetric conclusion\(1\) Target\.Ifx,y,z\>0x,y,z\>0andx4\+y4\+z4=3x^\{4\}\+y^\{4\}\+z^\{4\}=3, thenx\+y\+z≤3x\+y\+z\\leq 3,x​y\+y​z\+z​x≤3xy\+yz\+zx\\leq 3andx​y​z≤1xyz\\leq 1\. The conclusion is a conjunction, so a single inequality tactic has to discharge three different bounds at once\.[⬇](data:text/plain;base64,KHggeSB6IDog4oSdKSAoaHggOiAwIDwgeCkgKGh5IDogMCA8IHkpIChoeiA6IDAgPCB6KQogICAgKGggOiB4XjQgKyB5XjQgKyB6XjQgPSAzKSA6CiAgeCArIHkgKyB6IOKJpCAzIOKIpyB4KnkgKyB5KnogKyB6Kngg4omkIDMg4oinIHgqeSp6IOKJpCAx)\(xyz:ℝ\\mathbb\{R\}\)\(hx:0<x\)\(hy:0<y\)\(hz:0<z\)\(h:x^4\+y^4\+z^4=3\):x\+y\+z≤\\leq3∧\\wedgex\*y\+y\*z\+z\*x≤\\leq3∧\\wedgex\*y\*z≤\\leq1\(2\) Retrieved\.Two of the eight schemas\. Both are symmetric three\-variable inequalities under a different constraint\.[⬇](data:text/plain;base64,ZXhhbXBsZSAoeCB5IHogOiDihJ0pIChoeCA6IDAg4omkIHgpIChoeSA6IDAg4omkIHkpIChoeiA6IDAg4omkIHopCiAgICAoaCA6IHheMiArIHleMiArIHpeMiArIHgqeSp6ID0gNCkgOgogICAgMyooeF4yKnkgKyB5XjIqeiArIHpeMip4KSDiiaQgKHggKyB5ICsgeikqKHheMiArIHleMiArIHpeMikgOj0gYnkKICBubGluYXJpdGggW3NxX25vbm5lZyAoeCAtIHkpLCBzcV9ub25uZWcgKHkgLSB6KSwgc3Ffbm9ubmVnICh6IC0geCksCiAgICBtdWxfbm9ubmVnIGh4IGh5LCBtdWxfbm9ubmVnIGh5IGh6LCBtdWxfbm9ubmVnIGh6IGh4LAogICAgbXVsX25vbm5lZyAoc3Ffbm9ubmVnICh4IC0geSkpIGh6LCAuLi5dCgpleGFtcGxlICh4IHkgeiA6IOKEnSkgKGh4IDogMCDiiaQgeCDiiKcgeCDiiaQgMSkgKGh5IDogMCDiiaQgeSDiiKcgeSDiiaQgMSkKICAgIChoeiA6IDAg4omkIHog4oinIHog4omkIDEpIDoKICAgIDIgKiAoeCp5ICsgeSp6ICsgeip4KSDiiaQgMyp4KnkqeiArIHggKyB5ICsgeiA6PSBieQogIGhhdmUgaDEgOiAwIOKJpCAoMSAtIHgpICogKDEgLSB5KSAqIHogOj0gYnkKICAgIGFwcGx5IG11bF9ub25uZWcKICAgIMK3IGFwcGx5IG11bF9ub25uZWcgPDs+IGxpbmFyaXRoCiAgICDCtyBsaW5hcml0aAogIC4uLg==)example\(xyz:ℝ\\mathbb\{R\}\)\(hx:0≤\\leqx\)\(hy:0≤\\leqy\)\(hz:0≤\\leqz\)\(h:x^2\+y^2\+z^2\+x\*y\*z=4\):3\*\(x^2\*y\+y^2\*z\+z^2\*x\)≤\\leq\(x\+y\+z\)\*\(x^2\+y^2\+z^2\):=bynlinarith\[sq\_nonneg\(x\-y\),sq\_nonneg\(y\-z\),sq\_nonneg\(z\-x\),mul\_nonneghxhy,mul\_nonneghyhz,mul\_nonneghzhx,mul\_nonneg\(sq\_nonneg\(x\-y\)\)hz,\.\.\.\]example\(xyz:ℝ\\mathbb\{R\}\)\(hx:0≤\\leqx∧\\wedgex≤\\leq1\)\(hy:0≤\\leqy∧\\wedgey≤\\leq1\)\(hz:0≤\\leqz∧\\wedgez≤\\leq1\):2\*\(x\*y\+y\*z\+z\*x\)≤\\leq3\*x\*y\*z\+x\+y\+z:=byhaveh1:0≤\\leq\(1\-x\)\*\(1\-y\)\*z:=byapplymul\_nonneg⋅\\cdotapplymul\_nonneg<;\>linarith⋅\\cdotlinarith\.\.\.\(3\) Generated\.The kernel\-accepted proof builds eleven named intermediate results and assembles the conjunction at the end, rather than attacking it in one step\. Supporting expressions are elided at\.\.\.for space\.[⬇](data:text/plain;base64,aGF2ZSBoMSA6IHheMiArIHleMiArIHpeMiDiiaQgMyA6PSBieQogIG5saW5hcml0aCBbc3Ffbm9ubmVnICh4XjIgLSAxKSwgLi4uLCBoXQpoYXZlIGgyIDogeCp5ICsgeSp6ICsgeip4IOKJpCB4XjIgKyB5XjIgKyB6XjIgOj0gYnkKICBubGluYXJpdGggW3NxX25vbm5lZyAoeCAtIHkpLCBzcV9ub25uZWcgKHkgLSB6KSwgc3Ffbm9ubmVnICh6IC0geCldCmhhdmUgaDMgOiB4KnkgKyB5KnogKyB6Kngg4omkIDMgOj0gYnkgbGluYXJpdGggW2gxLCBoMl0KaGF2ZSBoNCA6ICh4ICsgeSArIHopXjIg4omkIDkgOj0gYnkgbmxpbmFyaXRoIFtoMSwgaDJdCmhhdmUgaDUgOiB4ICsgeSArIHog4omkIDMgOj0gYnkgbmxpbmFyaXRoIFtzcV9ub25uZWcgKHggKyB5ICsgeiAtIDMpLCBoNF0KaGF2ZSBoNiA6IHheMip5XjIgKyB5XjIqel4yICsgel4yKnheMiDiiaQgMyA6PSBieQogIG5saW5hcml0aCBbc3Ffbm9ubmVnICh4XjIgLSB5XjIpLCAuLi4sIGhdCmhhdmUgaDcgOiAoeF4yICsgeV4yICsgel4yKSAqICh4XjIqeV4yICsgeV4yKnpeMiArIHpeMip4XjIpCiAgICDiiaUgOSAqIHheMiAqIHleMiAqIHpeMiA6PSBieQogIG5saW5hcml0aCBbbXVsX25vbm5lZyAoc3Ffbm9ubmVnIHgpIChzcV9ub25uZWcgKHleMiAtIHpeMikpLCAuLi5dCmhhdmUgaFAgOiAwIOKJpCB4XjIqeV4yICsgeV4yKnpeMiArIHpeMip4XjIgOj0gYnkKICBubGluYXJpdGggW3NxX25vbm5lZyAoeCp5KSwgc3Ffbm9ubmVnICh5KnopLCBzcV9ub25uZWcgKHoqeCldCmhhdmUgaF9TUCA6ICh4XjIgKyB5XjIgKyB6XjIpICogKHheMip5XjIgKyB5XjIqel4yICsgel4yKnheMikg4omkIDkgOj0gYnkKICBubGluYXJpdGggW211bF9ub25uZWcgaFAgKHN1Yl9ub25uZWcubXByIGgxKSwgLi4uXQpoYXZlIGg4IDogeF4yICogeV4yICogel4yIOKJpCAxIDo9IGJ5IG5saW5hcml0aCBbaDcsIGhfU1BdCmhhdmUgaDkgOiB4ICogeSAqIHog4omkIDEgOj0gYnkgbmxpbmFyaXRoIFtzcV9ub25uZWcgKHgqeSp6IC0gMSksIGg4XQpleGFjdCDin6hoNSwgaDMsIGg54p+p)haveh1:x^2\+y^2\+z^2≤\\leq3:=bynlinarith\[sq\_nonneg\(x^2\-1\),\.\.\.,h\]haveh2:x\*y\+y\*z\+z\*x≤\\leqx^2\+y^2\+z^2:=bynlinarith\[sq\_nonneg\(x\-y\),sq\_nonneg\(y\-z\),sq\_nonneg\(z\-x\)\]haveh3:x\*y\+y\*z\+z\*x≤\\leq3:=bylinarith\[h1,h2\]haveh4:\(x\+y\+z\)^2≤\\leq9:=bynlinarith\[h1,h2\]haveh5:x\+y\+z≤\\leq3:=bynlinarith\[sq\_nonneg\(x\+y\+z\-3\),h4\]haveh6:x^2\*y^2\+y^2\*z^2\+z^2\*x^2≤\\leq3:=bynlinarith\[sq\_nonneg\(x^2\-y^2\),\.\.\.,h\]haveh7:\(x^2\+y^2\+z^2\)\*\(x^2\*y^2\+y^2\*z^2\+z^2\*x^2\)≥\\geq9\*x^2\*y^2\*z^2:=bynlinarith\[mul\_nonneg\(sq\_nonnegx\)\(sq\_nonneg\(y^2\-z^2\)\),\.\.\.\]havehP:0≤\\leqx^2\*y^2\+y^2\*z^2\+z^2\*x^2:=bynlinarith\[sq\_nonneg\(x\*y\),sq\_nonneg\(y\*z\),sq\_nonneg\(z\*x\)\]haveh\_SP:\(x^2\+y^2\+z^2\)\*\(x^2\*y^2\+y^2\*z^2\+z^2\*x^2\)≤\\leq9:=bynlinarith\[mul\_nonneghP\(sub\_nonneg\.mprh1\),\.\.\.\]haveh8:x^2\*y^2\*z^2≤\\leq1:=bynlinarith\[h7,h\_SP\]haveh9:x\*y\*z≤\\leq1:=bynlinarith\[sq\_nonneg\(x\*y\*z\-1\),h8\]exact⟨\\langleh5,h3,h9⟩\\rangle\(4\) Compared\.The released reference proof splits the conjunction first and discharges all three parts with one shared list of auxiliary inequalities\. Six of its nine inequalities appear nowhere in the accepted proof\.[⬇](data:text/plain;base64,cmVmaW5lJyDin6hfLCBfLCBf4p+pCmFsbF9nb2FscyBubGluYXJpdGggW3NxX25vbm5lZyAoeCAtIHkpLCBzcV9ub25uZWcgKHkgLSB6KSwgc3Ffbm9ubmVnICh6IC0geCksCiAgc3Ffbm9ubmVnICh4ICsgeSksIHNxX25vbm5lZyAoeSArIHopLCBzcV9ub25uZWcgKHogKyB4KSwgaCwKICBzcV9ub25uZWcgKHggLSAxKSwgc3Ffbm9ubmVnICh5IC0gMSksIHNxX25vbm5lZyAoeiAtIDEpXQ==)refine’⟨\\langle\_,\_,\_⟩\\rangleall\_goalsnlinarith\[sq\_nonneg\(x\-y\),sq\_nonneg\(y\-z\),sq\_nonneg\(z\-x\),sq\_nonneg\(x\+y\),sq\_nonneg\(y\+z\),sq\_nonneg\(z\+x\),h,sq\_nonneg\(x\-1\),sq\_nonneg\(y\-1\),sq\_nonneg\(z\-1\)\]\(5\) Outcome over three runs\.Zero\-shot closes zero runs, relevant retrieval closes two and random retrieval closes one\.