ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

# ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
Source: [https://arxiv.org/html/2605.22885](https://arxiv.org/html/2605.22885)
Riyaz Ahuja Carnegie Mellon University riyaza@andrew\.cmu\.edu &Tate Rowney Carnegie Mellon University trowney@andrew\.cmu\.edu &Jeremy Avigad Carnegie Mellon University avigad@andrew\.cmu\.edu &Sean Welleck Carnegie Mellon University swelleck@andrew\.cmu\.edu

###### Abstract

Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers\. However, scalable proof optimization is hindered by heterogeneous and heuristically specified objectives, scarce data, and high training and inference costs\. To overcome these challenges, we introduce ImProver 2, a neurosymbolic framework for automated proof optimization in Lean 4\. ImProver 2 combines a data\-efficient expert\-iteration pipeline with a scaffold that exposes formal structure alongside lightweight informal abstractions\. We further introduce a suite of metrics capturing structural proof properties\. Using ImProver 2, we train a 7B\-parameter model that outperforms orders\-of\-magnitude larger models within the same model family, and is competitive with mid\-tier frontier models across metrics\. We additionally demonstrate that our neurosymbolic scaffold significantly improves performance across both small and frontier models\. We show that with proper scaffolding and training, small models can effectively restructure research\-level proofs over complex and varied metrics, matching substantially larger systems and establishing proof optimization as a scalable, learnable task\.

## 1Introduction

Formal proof assistants such as Lean\(Moura and Ullrich,[2021](https://arxiv.org/html/2605.22885#bib.bib1)\), Rocq\(The Coq Development Team,[2024](https://arxiv.org/html/2605.22885#bib.bib2)\), and Isabelle\(Wenzelet al\.,[2008](https://arxiv.org/html/2605.22885#bib.bib3)\)have transformed mathematical practice by making the correctness of proofs explicit and mechanized\. Community libraries such as Lean’s Mathlib\(The Mathlib Community,[2020](https://arxiv.org/html/2605.22885#bib.bib4)\)now grow at a pace driven both by increasing human contributions and by recent advances in neural theorem proving and autoformalization\(Achimet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib12); Hubertet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib10)\)\.

This rapid expansion raises multiple concerns about issues of data quality\. First, this expansion stresses the maintainability, coherence, and long\-term usability of libraries due to proofs that are often heterogeneous in style and clarity\(The Mathlib Community,[2020](https://arxiv.org/html/2605.22885#bib.bib4)\)\. Second, low library quality decreases its utility as training data: modern theorem provers and autoformalizers increasingly train on these very corpora, so the structure and readability of proofs directly shape downstream prover performance\(Guet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib8)\)\. Unfortunately, the growth rate of formal libraries already exceeds what human reviewers and maintainers can reliably curate; and moreover, this discrepancy is only expected to widen due to increasing volumes of machine\-generated proofs which, even when guaranteed to be correct, do not carry similar guarantees as to the proof’s quality, modularity, or understandability\(Chenet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib17)\)\.

This motivates automated proof optimization: given a verified proof, produce a formally correct rewrite that scores better under a user\-defined objective, such as shorter length, higher modularity, or fewer explicit dependencies\(Ahujaet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib9)\)\. Because objectives vary by use case and formal context, a practical method must scale across arbitrary metrics and research\-level theorems\. Small specialized models are especially attractive for this setting because relevant data is scarce in general corpora, library\-scale deployment can require millions of samples, and local open\-weight models are more accessible to formalization projects\.

We address these problems withImProver 2, a self\-improving pipeline that trains small language models \(SLMs\) to optimize Lean proofs under a wide\-ranging class of metrics\. Our core idea is to leverageiterative preference optimization: iterating between generating proof candidates, scoring them according to correctness and the desired optimization criterion, and learning from the resulting pairs of higher and lower scoring proofs\. In particular, we extend the Iterative Reasoning Preference Optimization \(IRPO\)\(Panget al\.,[2024](https://arxiv.org/html/2605.22885#bib.bib26)\)algorithm with a new replay buffer that balances old and newly generated data for use in the next round of training, preventing model collapse and allowing for monotonic improvement over many rounds\. We additionally give the model access to rich information from the Lean theorem proving environment, including goal states, informalized summaries, lemma context, and examples, which we termneurosymbolic augmentation\. We useImProver 2to train models for three different metrics: thelengthof the proof,modularity\(the ability to divide the proof into a series of smaller lemmas\), and the explicitdependenciesused by the theorem, and show that our trained models can substantially improve over their base model and remain competitive with much larger unscaffolded systems on research\-level theorems\. In summary, our contributions are:

1. 1\.*Self\-improving SLMs for proof refactoring\.*We show that iterative preference optimization can bootstrap small language models on proof optimization in specialized research libraries, making them competitive with much larger models in several unscaffolded comparisons\.
2. 2\.*Structural optimization metrics\.*Beyond proof length\(Ahujaet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib9); Guet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib8)\), we studymodularityanddependencymetrics that leverage proof structure and the surrounding library\. These metrics were chosen with formal mathematics experts and target distinct proof\-refactoring objectives\.
3. 3\.*Neurosymbolic augmentation for research mathematics\.*We extract relevant lemmas or definitions, goal\-state traces, and automatic informalizations of target proofs\. This augmentation boosts both small and large models on proof optimization\.

We additionally open\-source our code and data111[Github](https://github.com/riyazahuja/improver)\.

## 2Related Work

Interest in neurosymbolic theorem proving–the use of deep learning to create or manipulate verified mathematical proofs in languages such as Lean 4\(Moura and Ullrich,[2021](https://arxiv.org/html/2605.22885#bib.bib1)\)–has seen significant advancements in recent years\(Luet al\.,[2023](https://arxiv.org/html/2605.22885#bib.bib5); Liet al\.,[2024](https://arxiv.org/html/2605.22885#bib.bib6)\)\. In particular, much research has focused on generating formal proofs given their statements\(Polu and Sutskever,[2020](https://arxiv.org/html/2605.22885#bib.bib7)\), with recent systems achieving high performance on nontrivial benchmarks and internationally renowned mathematics competitions\(Hubertet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib10); Achimet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib12); Chenet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib17)\)\. Many systems additionally utilize neurosymbolic augmentation, providing a generative prover model with information gathered from within the proof environment\(Yanget al\.,[2023](https://arxiv.org/html/2605.22885#bib.bib11); Ahujaet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib9); Linet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib14)\)\. However, both formal and informal proofs generated by current LLM\-based systems often suffer from stylistic irregularities even when they are sound, including redundant steps or a structure which does not clearly represent the broader logical argument\(Friederet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib13)\)\.

Previous work by\(Ahujaet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib9); Guet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib8)\)has attempted to rectify these issues by creating LLM\-based agents to refactor formal proofs\.Ahujaet al\.\([2025](https://arxiv.org/html/2605.22885#bib.bib9)\)created a system capable of optimizing towards multiple metrics of improvement; however, it relied on general\-purpose closed\-source models, leading to substantial deployment costs and limited ability to improve performance beyond these models’ baseline\.Guet al\.\([2025](https://arxiv.org/html/2605.22885#bib.bib8)\)focused solely on optimizing the token count of proofs according to a complex tokenizer intended to reduce the time required to compile them; they do not examine other metrics, leaving out important use cases and limiting its utility to research mathematicians\. Furthermore, the works above do not fully utilize the information available through working in an interactive theorem proving environment via goal\-state extraction\(Polu and Sutskever,[2020](https://arxiv.org/html/2605.22885#bib.bib7)\), premise retrieval\(Yanget al\.,[2023](https://arxiv.org/html/2605.22885#bib.bib11)\), or auto\-informalization\(Hattoriet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib28)\); both of the above overlook at least one of these aspects\.

## 3Proof Optimization

Given a verified proof, a proof optimization agent synthesizes a semantically equivalent proof that is “better” under a user\-specified objective while remaining correct according to the Lean kernel\. We follow the setup ofAhujaet al\.\([2025](https://arxiv.org/html/2605.22885#bib.bib9)\); Guet al\.\([2025](https://arxiv.org/html/2605.22885#bib.bib8)\)and introduce two additional structural metrics:modularityanddependencies\.

Original

theoremisCoatom\_iff\[OrderTopA\]\{K:A\}:

IsCoatomK↔K≠T∧∀Hg,K≤H→g∉K→g∈H→H=T:=by

simp\_rw\[IsCoatom,lt\_iff\_le\_not\_le,SetLike\.not\_le\_iff\_exists,

and\_comm\(a:=\_≤\_\),and\_imp,exists\_imp,←and\_imp,and\_comm\]

Original

theoremmem\_cross\_iff\(xy:TSetγ\):

∀a,a∈’crosshβhγhδxy↔∃bc,a=⟨b,c⟩’∧b∈’x∧c∈’y:=by

introa

rw\[cross,mem\_inter\_iff,vCross\_spec\]

constructor

·rintro⟨h₁,b,c,rfl,h₂⟩

simponly\[op\_mem\_converse\_iff,vCross\_spec,op\_inj\]ath₁

obtain⟨b’,c’,⟨rfl,rfl⟩,h₁⟩:=h₁

exact⟨b,c,rfl,h₁,h₂⟩

·rintro⟨b,c,rfl,h₁,h₂⟩

simponly\[op\_mem\_converse\_iff,vCross\_spec,op\_inj\]

exact⟨⟨c,b,⟨rfl,rfl⟩,h₁⟩,⟨b,c,⟨rfl,rfl⟩,h₂⟩⟩

Original

lemmaKD\_weakerThan\_KDB:\(Hilbert\.KDα\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KDBα\\alpha\):=normal\_weakerThan\_of\_subset$\\mathdollarbyintro;aesop;

Optimized \(Dependency\)

theoremisCoatom\_iff\[OrderTopA\]\{K:A\}:

IsCoatomK↔K≠T∧∀Hg,K≤H→\\rightarrowg∉K→\\rightarrowg∈H→\\rightarrowH=T:=by

constructor<;\>introh

<;\>simp\_all\[IsCoatom,lt\_iff\_le\_not\_le,SetLike\.not\_le\_iff\_exists\]

<;\>tauto

Optimized \(Length\)

theoremmem\_cross\_iff\(xy:TSetγ\):

∀a,a∈’crosshβhγhδxy↔∃bc,a=⟨b,c⟩’∧b∈’x∧c∈’y:=by

simp\_all\[cross,mem\_inter\_iff,vCross\_spec,

op\_mem\_converse\_iff,op\_inj\]

<;\>aesop

Optimized \(Modularity\)

lemmaKD\_weakerThan\_KDB:\(Hilbert\.KDα\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KDBα\\alpha\):=by

haveh1:\(LO\.Modal\.Hilbert\.KDα\\alpha\)\.axioms⊆\\subseteq\(LO\.Modal\.Hilbert\.KDBα\\alpha\)\.axioms→\\rightarrow\(Hilbert\.KDα\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KDBα\\alpha\):=by

introh

applynormal\_weakerThan\_of\_subset

applyh

haveh2:\(LO\.Modal\.Hilbert\.KDα\\alpha\)\.axioms⊆\\subseteq\(LO\.Modal\.Hilbert\.KDBα\\alpha\)\.axioms:=by

introφ\\varphihPhi

cases’hPhiwithhPhihPhi

⋅\\cdotsimp\_all\[LO\.Modal\.Hilbert\.KD\]

⋅\\cdotsimp\_all\[LO\.Modal\.Hilbert\.KDB\]

exacth1h2

Figure 1:ImProver 2 automatically optimizes human\-written proofs to reduce explicit dependencies, minimize length, or maximize proof modularity, while maintaining formal correctness\.

### 3\.1Setup and notation

Let𝒞\\mathcal\{C\}denote proof contexts \(imports, local declarations, module metadata, etc\.\),𝒳\\mathcal\{X\}theorem statements, and𝒴\\mathcal\{Y\}proofs\. We consider\(c,x,y\)∈𝒞×𝒳×𝒴\(c,x,y\)\\in\\mathcal\{C\}\\times\\mathcal\{X\}\\times\\mathcal\{Y\}, whereyyis a purported proof ofxxinccwhich may or may not be sound\.

We define averifieras a computable function

v​\(c,x,y\):𝒞×𝒳×𝒴→\{0,1\},\\text\{v\}\(c,x,y\):\\mathcal\{C\}\\times\\mathcal\{X\}\\times\\mathcal\{Y\}\\to\\\{0,1\\\},This function outputs11ifyyis a syntactically correct and sound proof ofxxincc\. We also define

ℱ​\(c,x\)=\{y∈𝒴:v​\(c,x,y\)=1\}\.\\mathcal\{F\}\(c,x\)=\\\{y\\in\\mathcal\{Y\}:\\text\{v\}\(c,x,y\)=1\\\}\.Two proofsy,y′∈ℱ​\(c,x\)y,y^\{\\prime\}\\in\\mathcal\{F\}\(c,x\)are said to be*semantically equivalent*\.

We use the Lean 4 language\(Moura and Ullrich,[2021](https://arxiv.org/html/2605.22885#bib.bib1)\)as our verifier; the language’s kernel/type\-checker provides a strong guarantee of correspondence with a type\-theoretic model of modern mathematics\.

### 3\.2Optimization Objective

Two semantically equivalent proofs may have significant syntactic differences, and moreover certain characteristics may make them more or less desirable for use in practice\. To quantify this, we define anoptimization metricas a computable function

μ:𝒞×𝒳×𝒴→ℝ,\\mu:\\mathcal\{C\}\\times\\mathcal\{X\}\\times\\mathcal\{Y\}\\to\\mathbb\{R\},Given an initial theorem and proof\(c,x,y0\)\(c,x,y\_\{0\}\), we aim to find a verifiably correct proof that maximizes metric score:

arg⁡maxy∈𝒴v​\(c,x,y\)=1μ​\(c,x,y\)\{\\arg\\max\}\_\{\\begin\{subarray\}\{c\}y\\in\\mathcal\{Y\}\\\\ v\(c,x,y\)=1\\end\{subarray\}\}\\quad\\mu\(c,x,y\)\(1\)
In practice, we approximate this via language model\-based Lean 4 code generation: by independently generating multiple variants, we may pick the one with greatest improvement, if it surpasses the original\.

#### 3\.2\.1Metrics of Interest

In this work, we focus and evaluate on a collection of three metrics, which are designed to be practical and interpretable structural objectives for formal proof optimization\. These metrics are proxies rather than reviewer\-validated measures of subjective proof quality: they support automatic evaluation at scale, but they do not by themselves establish human maintainer preference or downstream theorem\-prover utility\.

- •Length:We aim to minimize the length of proofs, measured by the number of tactics used\. In practice, proof shortening \(or “golfing"\) is a common activity in formal mathematics\(The Mathlib Community,[2020](https://arxiv.org/html/2605.22885#bib.bib4)\), as shorter proofs are often easier to read and maintain, and reduce overhead during compilation\. As such, we define the length metricμl​e​n\\mu\_\{len\}as the negative of the number of tactics\.
- •Dependencies:We aim to minimize the explicit dependency footprint of proofs, measured by the number of unique external lemmas explicitly named in the proof\. This metric does not measure semantic independence from the library: a proof usingsimporomegamay still rely on many facts internally\. This encourages self\-contained proofs that do not require the use or memorization of large numbers of dependency names, improving maintainability\.222We would like to thank Dr\. Heather Macbeth of Imperial College London for reaching out to suggest the idea behind this metric\.\. More specifically, given a theorem and proof\(c,x,y\)\(c,x,y\), we computeDepsc,x,y\\text\{Deps\}\_\{c,x,y\}, the set of all theorems explicitly named in the proofyy\(see Section[B](https://arxiv.org/html/2605.22885#A2)\)\. The metric is then defined asμd​e​p​\(c,x,y\):=−\|Depsc,x,y\|\\mu\_\{dep\}\(c,x,y\):=\-\\left\|\\text\{Deps\}\_\{c,x,y\}\\right\|\.
- •Modularity:We aim to maximize themodularityof proofs, which is intuitively understood to be the number of independent subproofs in our proof\. This is a structural objective motivated by proof decomposition, lemma\-generation workflows, and maintainable proof organization\. To quantify modularity, we postprocess Lean proofs to deconstruct them into a tree of tactics, with edges representing the logical dependencies and flow between tactics in the proof\. In this tree, we mark a subset of edges as “spawned" if they correspond to goals that are introduced by the proof but are not direct subgoals of the current tactic, which naturally arise from tactics likehave,calc, etc\., and correspond with the informal notion of "modular" independent subproofs\. We therefore define the modularity metric asμm​o​d​\(c,x,y\)=\|\{effective spawned goals in​y\}\|\\mu\_\{mod\}\(c,x,y\)=\|\\\{\\text\{effective spawned goals in \}y\\\}\|\. The designation of which spawned goals are non\-trivial and “effective" requires the use of several heuristics; a complete definition is provided in Appendix[A](https://arxiv.org/html/2605.22885#A1)\. These safeguards reduce trivial goal\-spawning and duplicate\-wrapper artifacts, but they do not eliminate all stylistically debatable decompositions\. Example Proof Tree lemmaKD5\_weakerThan\_KD45:\(Hilbert\.KD5α\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KD45α\\alpha\):=by haveh1:\(LO\.Modal\.Hilbert\.KD5α\\alpha\)\.axioms⊆\\subseteq\(LO\.Modal\.Hilbert\.KD45α\\alpha\)\.axioms→\\rightarrow\(Hilbert\.KD5α\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KD45α\\alpha\):=by introh applynormal\_weakerThan\_of\_subset <;\>assumption haveh2:\(LO\.Modal\.Hilbert\.KD5α\\alpha\)\.axioms⊆\\subseteq\(LO\.Modal\.Hilbert\.KD45α\\alpha\)\.axioms:=by introφ\\varphihPhi cases’hPhiwithhPhihPhi <;\>simp\_all\[LO\.Modal\.Hilbert\.KD5,LO\.Modal\.Hilbert\.KD45\] <;\>aesop exacth1h2 have h1:\[…\]:= byintro hhave h2:\[…\]:= byintroφ\\varphihφ\\varphiapply \[…\]assumptionexact h1h2cases’ hφ\\varphiwith hφ\\varphihφ\\varphisimp\_all \[…\]simp\_all \[…\]aesop⊤\\top⊤\\top⊤\\top⊤\\top Figure 2:Example Lean proof \(top\) and its generated proof tree \(bottom\)\. Note the root node \(in blue\), and the two effective spawned goals coming fromh1h\_\{1\}andh2h\_\{2\}\(in red\)\.

## 4ImProver 2

We present ImProver 2, a training pipeline that bootstraps small language models \(SLMs\) for a target proof\-optimization metric\. It combines IRPO training \([4\.3\.2](https://arxiv.org/html/2605.22885#S4.SS3.SSS2)\), a replay buffer balancing old and newly generated data \([4\.3\.1](https://arxiv.org/html/2605.22885#S4.SS3.SSS1)\), and neurosymbolic augmentation for generation \([4\.2](https://arxiv.org/html/2605.22885#S4.SS2)\)\.

InferenceDataset BufferData ShapingTrainingGtG\_\{t\}𝒟nr\(t\)\\mathcal\{D\}\_\{\\mathrm\{nr\}\}^\{\(t\)\}𝒟test\(t\)\\mathcal\{D\}\_\{\\mathrm\{test\}\}^\{\(t\)\}Scoret=Sμ¯​\(𝒟test\(t\)\)=\\overline\{S\_\{\\mu\}\}\(\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{test\}\}\)𝒫train\\mathcal\{P\}\_\{\\mathrm\{train\}\}𝒫test\\mathcal\{P\}\_\{\\mathrm\{test\}\}𝒟re\(t\)\\mathcal\{D\}\_\{\\mathrm\{re\}\}^\{\(t\)\}𝒟fil\(t\)\\mathcal\{D\}\_\{\\mathrm\{fil\}\}^\{\(t\)\}Add toBufferRetrieve𝒟re\(t−1\)\\mathcal\{D\}\_\{\\mathrm\{re\}\}^\{\(t\-1\)\}𝒟IRPO\(t\)\\mathcal\{D\}\_\{\\mathrm\{IRPO\}\}^\{\(t\)\}Gt\+1G\_\{t\+1\}Add Replay BufferFilterStoreCurate PairsTrain \(IRPO\)Update

Figure 3:ImProver2training loop\.The diagram illustrates the iterative process of generation, retrieval, filtering, and training\. Node colors represent the evolution of data from initial sampling \(Blue\) through processing \(Purple\) to training \(Magenta\)\.### 4\.1Overview

Given an un\-modified base language modelG0G\_\{0\}, at thett\-th iteration ImProver 2’s core loop aims to train the modelGt\+1G\_\{t\+1\}fromGtG\_\{t\}as follows \(also depicted in Figure[3](https://arxiv.org/html/2605.22885#S4.F3)\):

1. 1\.For some budget hyperparametern∈ℕn\\in\\mathbb\{N\}, generatenncandidate proofs per problem in the training set using the current modelGtG\_\{t\}\([4\.2](https://arxiv.org/html/2605.22885#S4.SS2)\), providing the model with neurosymbolic augmentation \([4\.2\.1](https://arxiv.org/html/2605.22885#S4.SS2.SSS1)\) and a description of the metric to assist in generation\. These new potential proofs form a new dataset \(denoted𝒟nr\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{nr\}\}\)\.
2. 2\.The previous iteration’s dataset,𝒟re\(t−1\)\\mathcal\{D\}^\{\(t\-1\)\}\_\{\\mathrm\{re\}\}\(ourreplay buffer\), is interleaved with𝒟nr\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{nr\}\}to get𝒟re\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{re\}\}\(see[4\.3\.1](https://arxiv.org/html/2605.22885#S4.SS3.SSS1)\)\.
3. 3\.The modelGtG\_\{t\}is trained to obtainGt\+1G\_\{t\+1\}\([4\.3\.2](https://arxiv.org/html/2605.22885#S4.SS3.SSS2)\)\. Our reinforcement learning policy of choice, known as Iterative Reasoning Preference Optimization or IRPO\(Panget al\.,[2024](https://arxiv.org/html/2605.22885#bib.bib26)\), relies on preference pairs of desirable/undesirable proofs, so𝒟re\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{re\}\}is filtered to remove low\-quality solutions and pairs are created to form𝒟IRPO\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{IRPO\}\}\(again described in[4\.3\.1](https://arxiv.org/html/2605.22885#S4.SS3.SSS1)\)\.
4. 4\.Gt\+1G\_\{t\+1\}is evaluated withnnsamples on the test set, again similarly to[4\.2](https://arxiv.org/html/2605.22885#S4.SS2)\. The improvement in metric score of the new proofs over the originals is calculated\.

The loop is repeated until convergence of the average improvement score, or exhaustion of the compute budget\.

### 4\.2Generation

A central feature of ImProver 2 is self\-generation of training data: at each round, the current modelG\(t\)G^\{\(t\)\}receives the theorem statement, original proof, target metric, and proof\-environment context, then samplesnncandidate rewrites per theorem\.

#### 4\.2\.1Neurosymbolic Augmentation

Formal proof environments provide substantial opportunities to obtain relevant information about a proof\. We prompt our language model with additional neurosymbolic context that exposes the structure and dependencies of a problem at both a formal and informal level\. This augmentation comes from three sources: a context slice to find relevant lemmas or definitions, goal\-state traces to highlight the exact effect of each tactic on the progress of the proof, and auto\-informalization to provide a higher\-level natural language description of the proof in question\. Each of these sources is described in detail below\.

##### Context

When working with proofs in high\-dependency environments, it is likely that a given proofy0y\_\{0\}relies on many lemmas, definitions, and other formal objects defined in the contextcc\. We aim to extract and serialize a minimal set of these objects to better inform our generation process: the signatures of all definitions and theorems that are directly referenced by name in the theorem statementxxor the original proofy0y\_\{0\}are collected and provided provided to the model, along with any associated documentation comments\. The process of collecting and filtering these is outlined in Appendix[B](https://arxiv.org/html/2605.22885#A2)\.

##### Chain\-of\-States \(CoS\)

Chain\-of\-states prompting\(Ahujaet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib9)\)provides a language model with the explicit state and remaining goals of a proof following the application of each tactic/step, providing richer information about the proof’s structure than is normally available\. We utilize Lean’sInfoTreestructures to obtain and serialize these states, and interleave them into the original proof as comments\. This process is described formally in Appendix[D](https://arxiv.org/html/2605.22885#A4)\.

##### Auto\-informalization

Utilizing natural language to guide the generation of formal proofs has been shown to significantly increase the capabilities of LLM\-based systems on formal mathematical tasks\(Jianget al\.,[2023](https://arxiv.org/html/2605.22885#bib.bib29)\)\. We therefore expose natural\-language sketches of each target proof to the model, providing a fuzzy layer of abstraction that captures the “meaning” of formal items while being robust to syntactic variation and surface\-level noise\.

More concretely, we prompt a language model using the proof’s chain\-of\-states information as described above to translate a Lean proof into natural language by explaining the effect of each tactic on the proof state and providing this to the proof optimizer model\. We emphasize that this informalization is a secondary channel for the generator and serves simply as an additional representation of the target theorem; outputs are still prompted to be generated formally, and correctness is still judged formally\.

### 4\.3Training

We adapt IRPO\(Panget al\.,[2024](https://arxiv.org/html/2605.22885#bib.bib26)\)for proof optimization by ranking candidates using both correctness and metric improvement, yielding denser preference signals than binary success alone\. We also mix new and old samples through replay, and train only on the final proof output rather than the reasoning trace\.

#### 4\.3\.1Datasets and Replay Buffer

Indiscriminate self\-training can collapse model output distributions\(Shumailovet al\.,[2024](https://arxiv.org/html/2605.22885#bib.bib31)\)\. Our replay buffer filters new samples, combines them with existing data, and sorts them by improvement before training\.

After generating𝒟nr\(t\)\\mathcal\{D\}\_\{\\text\{nr\}\}^\{\(t\)\}, we combine candidates for each eligible problem with prior candidates, remove trivially easy problems, and partition proofs into “winners” \(compiling, high\-improvement proofs\) and “losers” \(all others\)\. Appendix[C](https://arxiv.org/html/2605.22885#A3)gives details\.

##### IRPO Dataset

We form two preference\-pair types: winner–winner pairs ordered by metric improvement, and winner–loser pairs preferring valid improving proofs over failures\. The construction and hyperparametersW,LW,Lappear in Algorithm[1](https://arxiv.org/html/2605.22885#alg1)\.

#### 4\.3\.2IRPO \(Iterative Reasoning Preference Optimization\)

With this dataset𝒟IRPO\(t\)\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}, we calculate the IRPO loss on each itemTTas the \(weighted\) sum of the DPO loss of the preference pair and the negative log\-likelihood \(NLL\) loss over the winner:

ℒIRPO​\(T\)=\\displaystyle\\mathcal\{L\}\_\{\\text\{IRPO\}\}\(T\)=ℒDPO​\(yT,ℓ,yT,w∣Ψ​\(cT,xT,yT,0\),μ\)\\displaystyle\\mathcal\{L\}\_\{\\text\{DPO\}\}\(y\_\{T,\\ell\},y\_\{T,w\}\\mid\\Psi\(c\_\{T\},x\_\{T\},y\_\{T,0\}\),\\mu\)\+α​ℒNLL​\(yT,ℓ,yT,w∣Ψ​\(cT,xT,yT,0\),μ\)\\displaystyle\+\\alpha\\mathcal\{L\}\_\{\\text\{NLL\}\}\(y\_\{T,\\ell\},y\_\{T,w\}\\mid\\Psi\(c\_\{T\},x\_\{T\},y\_\{T,0\}\),\\mu\)
In the above, we represent the relevant neurosymbolic augmentation with the functionΨ\\Psi\. After training with respect to this objective for one epoch, we obtainGt\+1G\_\{t\+1\}\.

## 5Experiments

### 5\.1Setup

We evaluate ImProver 2 on all three metrics using public research\-level mathematics repositories, benchmarking against open\-source and closed\-source baselines at varying parameter counts\.

##### Dataset and split

We utilize Lean proofs from several open\-source projects formalizing research\-level mathematics across multiple domains\(The Mathlib Community,[2020](https://arxiv.org/html/2605.22885#bib.bib4); Tooby\-Smith,[2025](https://arxiv.org/html/2605.22885#bib.bib23); Tao,[2026](https://arxiv.org/html/2605.22885#bib.bib25); van Doornet al\.,[2026](https://arxiv.org/html/2605.22885#bib.bib19); Wilshaw,[2026](https://arxiv.org/html/2605.22885#bib.bib20); Buzzard and Taylor,[2026](https://arxiv.org/html/2605.22885#bib.bib21); Saito and Noguchi,[2026](https://arxiv.org/html/2605.22885#bib.bib22); Sergeevet al\.,[2026](https://arxiv.org/html/2605.22885#bib.bib24)\)\. We hold out all theorems in miniCTX\-v2 as the test set\. To prevent data leakage, we additionally exclude from training every theorem that appears in the same source file as a miniCTX\-v2 theorem\. Training and validation sets are drawn from all remaining files in an80%/20%80\\%/20\\%split, although we pre\-filter the Mathlib portion of the dataset to a uniformly sampled subset of 37 files, due to its significantly larger scale\.

We use miniCTX\-v2 as a proxy for deployment on human\-written research\-level mathematics\. Although ImProver 2 could in principle be applied to other domains, such as long machine\-generated proofs, these settings fall outside the scope of our main evaluation\. As a qualitative test, however, we also evaluate ImProver 2 on machine\-generated AlphaProof proofs from the 2024 International Mathematical Olympiad in Appendix[F\.2](https://arxiv.org/html/2605.22885#A6.SS2)\.

##### Evaluation protocol

All evaluations use Lean v4\.17\.0\. For all main results, we evaluate with best@16 sampling \([4\.2](https://arxiv.org/html/2605.22885#S4.SS2)\) and report the improvement scoreμ​\(c,x,y\)−μ​\(c,x,y0\)\\mu\(c,x,y\)\-\\mu\(c,x,y\_\{0\}\)for all problems in the test set andμ∈\{μl​e​n,μd​e​p,μm​o​d\}\\mu\\in\\\{\\mu\_\{len\},\\mu\_\{dep\},\\mu\_\{mod\}\\\}\. With this we compute the mean of the improvement scores, as well as ancillary metrics such as the compilation accuracy𝒜​\(𝒟t​e​s​t\(t\)\)\\mathcal\{A\}\(\\mathcal\{D\}\_\{test\}^\{\(t\)\}\)and improved accuracy𝒜μ\+​\(𝒟t​e​s​t\(t\)\)\\mathcal\{A\}^\{\+\}\_\{\\mu\}\(\\mathcal\{D\}\_\{test\}^\{\(t\)\}\), defined as the percentage of compiling theorems that have a strictly positive improvement score\. We operate with a base model ofG0=G\_\{0\}=DeepSeek\-R1\-Distill\-Qwen\-7B\(DeepSeek\-AI,[2025](https://arxiv.org/html/2605.22885#bib.bib16)\)\. All models are evaluated, prompted – and forG0G\_\{0\}, trained – with the hyperparameters and configuration described in Appendix[E](https://arxiv.org/html/2605.22885#A5)\.

##### Systems compared

Our main evaluation compares ImProver 2 against three classes of baselines on MiniCTX\-v2 under best@16 sampling: \(i\) theDeepSeek\-R1family at multiple scales, to study parameter scaling within a fixed model family; \(ii\) frontier GPT\-based and open\-weight systems, includingGPT\-5\-high\(a full\-size high\-reasoning variant\),GPT\-5\-chat,GPT\-5\-mini,GPT\-5\-nano, andGPT\-oss\-120B; and \(iii\) the priorImProversystem and its base modelGPT\-4o\. We also report current API inference costs in Table[5\.2](https://arxiv.org/html/2605.22885#S5.SS2)\.

We also evaluate all generators with and without the neurosymbolic scaffoldΨ\\Psito isolate the effect of augmentation from the effect of training\. For each metric, we train IRPO until validation improvement regresses and report the best checkpoint for that objective\.

### 5\.2Main Results

Table 1:Frontier & Intra\-family Evaluations\.Comparison with frontier models, intra\-family baselines, and prior proof optimization systems\. Mean improvement at best@16 on MiniCTX\-v2\. Input/output cost per 1M tokens also listed for API models\.Table 2:Per\-iteration improvements\.Progression of mean improvement at best@16 on MiniCTX\-v2 across IRPO training iterations across all three metrics\.
Table[5\.2](https://arxiv.org/html/2605.22885#S5.SS2)shows that ImProver 2 improves theDeepSeek\-R1 7Bbase model on all three objectives, leads all evaluated unscaffolded systems on modularity, and is competitive with frontier models on dependency and length\. Namely, after IRPO training, the model improves from0\.1180\.118to0\.3300\.330on length,0\.0030\.003to0\.1430\.143on modularity, and0\.0500\.050to0\.2060\.206on dependency\. These gains also exceed the largerDeepSeek\-R1 14BandDeepSeek\-R1 671Bbaselines on every metric, suggesting that task\-specific training can compensate for substantial generic scale within this model family\.

Against frontier and prior systems, ImProver 2 is strongest on the structural metrics in the unscaffolded comparison\. It leads all evaluated unscaffolded systems on modularity and is effectively tied withGPT\-5\-highon dependency \(0\.2060\.206vs\.0\.2080\.208\)\. On length, it matchesGPT\-5\-mini, exceeds unscaffoldedGPT\-oss\-120B, and trails the high\-reasoningGPT\-5\-highand prior multi\-stepGPT\-4o\-basedImProversystem\. When frontier models receive the same scaffold \(Table[3](https://arxiv.org/html/2605.22885#S5.T3)\), several outperform ImProver 2; we therefore interpret these results as evidence for effective specialization rather than dominance over the strongest scaffolded frontier systems\.

We next unpack these aggregate results through three complementary analyses: intra\-family parameter scaling, best@nncomparisons against frontier and prior systems, and the evolution of performance across IRPO iterations\. We then isolate the contribution of the neurosymbolic scaffold across model families\.

#### 5\.2\.1Performance and Parameter Scaling

A central question is whether proof optimization performance is primarily driven by scale or by task\-specific specialization, when all else is equal\. Figure[4](https://arxiv.org/html/2605.22885#S5.F4)shows that within theDeepSeek\-R1model family, larger models generally achieve higher mean improvement under a fixed prompting and sampling protocol\. This trend is clearest for length and dependency, indicating that generic reasoning capacity does help with proof refactoring\.

At the same time, scale is not the full story\. ImProver 2, trained from a 7B base model, outperforms the much larger 671B DeepSeek model on all three objectives\. The gap is especially pronounced for modularity \(0\.1430\.143vs\.0\.0550\.055\) and dependency \(0\.2060\.206vs\.0\.1530\.153\), suggesting that for structural proof optimization, the relevant bottleneck is not only reasoning capacity but also whether the model has been adapted to the structure of the formal task\.

This interpretation is reinforced by the accuracy metrics\. Namely, within the same model family, larger general\-purpose models often maintain stronger raw compilation rates, but ImProver 2 is more likely to produce compiling proofs that are also improved under the target metric\.

We therefore interpret the scaling results as evidence that proof optimization is only partly a scale problem; it is also a specialization problem, and one for which iterative preference optimization is particularly effective\.

![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Modularity/declarativity2_param_perf.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/dependency_param_perf.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_param_perf.png)

Figure 4:Effect of parameter count on model performance on mean improvement at best@16 across all three metrics, with ImProver 2 marked\.
#### 5\.2\.2Comparison to Frontier and Prior Systems

![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_gpt_improver_comparison.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Modularity/declarativity2_gpt_improver_comparison.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/dependency_gpt_improver_comparison.png)

Figure 5:Comparison of ImProver 2 against frontier GPT\-based models and ImProver, evaluated on mean improvement at best@nnon all metrics, fromn=1n=1ton=16n=16\.We compare ImProver 2 against frontier closed\-source models, a large open\-weight baseline, and the priorImProversystem\. The resulting picture is mixed but informative: frontier systems are already strong proof rewriters, yet their strengths differ by objective, while ImProver 2 is most competitive on the structural metrics\.

Among the frontier baselines evaluated without scaffolding, ImProver 2 achieves the strongest modularity score \(0\.1430\.143\), showing that iterative task\-specific training can produce structural rewrites that generalist frontier models do not always find under the same single\-shot, unscaffolded protocol\. On dependency, ImProver 2 \(0\.2060\.206\) is competitive with the strongest frontier model evaluated,GPT\-5\-high\(0\.2080\.208\), and leadsGPT\-5\-mini\(0\.2030\.203\); we treat all three as effectively tied at the level of mean performance\. On length, ImProver 2 \(0\.3300\.330\) matchesGPT\-5\-miniand exceeds unscaffoldedGPT\-oss\-120B\(0\.3210\.321\), trailing onlyGPT\-5\-high\(0\.6600\.660\), which represents a qualitatively different operating point in terms of inference cost\.

Relative to large open\-weight baselines, ImProver 2 is also strong in the unscaffolded comparison\. It matches or exceeds unscaffoldedGPT\-oss\-120Bon all three metrics despite starting from a smaller base model\. We note thatGPT\-oss\-120Bis a sparse mixture\-of\-experts model activating approximately 5B parameters per token, so the raw parameter count comparison overstates the computational gap\. Moreover, whenGPT\-oss\-120Breceives the same scaffold, it substantially outperforms ImProver 2 on length and dependency \(Table[3](https://arxiv.org/html/2605.22885#S5.T3)\)\. We therefore interpret the result as evidence that metric\-specific iterative self\-improvement can make a small dense model useful and competitive in some settings, not as evidence that it dominates the strongest scaffolded open\-weight baselines\.

The comparison with the priorImProversystem is also revealing\. The original ImProver system leads ImProver 2 on length \(0\.3550\.355vs\.0\.3300\.330\), consistent with its use of a multi\-step prompting strategy with a strong proprietary base model\. By contrast, ImProver 2 leads on modularity \(0\.1430\.143vs\.0\.0880\.088\) and outperforms ImProver substantially on dependency \(0\.2060\.206vs\.0\.0470\.047\), suggesting that iterative structural supervision can learn refactoring behaviors that are not reliably induced by prompting alone\.

#### 5\.2\.3Per\-Iteration Improvement

Table[5\.2](https://arxiv.org/html/2605.22885#S5.SS2)shows that most improvement occurs within the first two or three IRPO rounds\. Dependency peaks at iteration 2, while length and modularity peak at iteration 3, so we select checkpoints separately by metric\. These gains suggest that the model is learning useful refactoring behavior from its own filtered generations, and that the replay\-buffered preference data remains informative for multiple rounds\. Indeed, as shown by the full best@nncurves \(Figure[6](https://arxiv.org/html/2605.22885#S5.F6)\), the trained checkpoints dominate the untrained and scaffold\-only baselines across nearly all sample budgets, indicating that the gains are not caused by a single high\-sample outlier\.

Improvement is not indefinite, however, as later rounds plateau or regress\. We interpret this as indicating saturation rather than instability, as once the most common and highest\-yield refactoring patterns have been absorbed, later rounds appear to produce fewer genuinely novel improvements and increasingly focus on narrower or noisier examples\.

![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/dependency_iterations.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Modularity/declarativity2_iterations.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_iterations.png)

Figure 6:Performance of ImProver 2 as a function of sample budget across training iterations\. Gains are largest in early iterations, with saturation by iterations 2–3 and mild regression thereafter\.
#### 5\.2\.4Effect of Neurosymbolic Scaffolding

Table[3](https://arxiv.org/html/2605.22885#S5.T3)isolates the effect of the scaffoldΨ\\Psifrom training\. Namely, across nearly all evaluated generators and metrics, adding the scaffoldΨ\\Psiimproves mean best@16 performance, often by a large margin\. For example, on length, we observeDeepSeek\-R1 7Bimproves from0\.1180\.118to0\.2360\.236,GPT\-5\-minifrom0\.3300\.330to0\.6320\.632, andGPT\-5\-highfrom0\.6600\.660to0\.8750\.875\. Dependency also improves for most systems, while modularity gains are smaller but generally positive\. This suggests that the scaffold is not merely compensating for weak base models; rather, it changes the representation of the task in a way that makes better rewrites easier to discover under a fixed sampling budget\. Overall, the scaffold appears to expand the set of useful rewrites the model can reliably attempt\. As such, by exposing goal\-state information, relevant context, and informal abstractions, it helps both small and large models move beyond surface\-level editing toward more substantive proof refactoring by improving models’ abilities to search over valid higher\-value rewrites under a fixed sampling budget\.

Table 3:Scaffold Evaluations\.Effect of neurosymbolic scaffolding\. Mean improvement at best@16 with and without the scaffoldΨ\\Psi, across model families and metrics\.
#### 5\.2\.5Additional Analyses

##### Improvement vs Accuracy

Mean improvement alone does not distinguish between broad, reliable gains and a smaller set of high\-reward successes\. We therefore also report compilation accuracy𝒜\\mathcal\{A\}and improved accuracy𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}, where𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}measures the fraction of test problems for which the model produces a compiling proof that has a strictly positive metric improvement score\.

Across both models and training iterations, optimization tends to raise𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}faster than𝒜\\mathcal\{A\}\. This is especially visible in the iteration study \(Table[5](https://arxiv.org/html/2605.22885#S5.T5)\)\. For dependency minimization, the base model begins with high compilation accuracy but low improved accuracy \(0\.7540\.754and0\.0370\.037respectively\), indicating that it often produces valid rewrites without meaningfully reducing dependency footprint\. After training, improved accuracy rises sharply, peaking at0\.1060\.106in iteration 2, while compilation accuracy drops to0\.4640\.464\. This reflects a central tradeoff of proof refactoring: larger structural edits are more likely to yield real gains when they succeed, but they also create more opportunities for compilation failure\.

The same pattern appears in cross\-model comparisons\. For example,GPT\-5\-nanoattains very high compilation accuracy on dependency \(0\.8940\.894\) but only moderate improved accuracy \(0\.0650\.065\), whereas ImProver 2 attains lower compilation accuracy \(0\.3680\.368\) but slightly higher improved accuracy \(0\.0690\.069\)\. This suggests that conservative models often preserve correctness by making safer edits, while specialized optimizers are more willing to attempt riskier transformations that improve the target metric when successful\. Accordingly, we view𝒜\\mathcal\{A\}and𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}as complementary:𝒜\\mathcal\{A\}measures stability, while𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}more directly captures whether the system is solving the optimization problem rather than merely preserving compilability\.

Table 4:Accuracy Evaluations\.Compilation accuracy and improved accuracy comparison amongst the best@16 mean improvement samples across all three metrics\. Each entry is reported as𝒜μ\+/𝒜\\mathcal\{A\}\_\{\\mu\}^\{\+\}/\\mathcal\{A\}, where𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}is improved accuracy and𝒜\\mathcal\{A\}is compilation accuracy\.Table 5:Accuracy Progression\.Compilation accuracy and improved accuracy progression amongst the best@16 mean improvement samples across IRPO training iterations\. Each entry is reported as𝒜μ\+/𝒜\\mathcal\{A\}\_\{\\mu\}^\{\+\}/\\mathcal\{A\}, where𝒜μ\+\\mathcal\{A\}\_\{\\mu\}^\{\+\}is improved accuracy and𝒜\\mathcal\{A\}is compilation accuracy\.
##### Per\-repository heterogeneity

Table 6:Average improvement by project and metric\.Performance varies substantially across repositories \(Table[6](https://arxiv.org/html/2605.22885#S5.T6)\), suggesting that optimization opportunity may be mediated by project\-specific proof style, theorem difficulty distributions, and domain\. For example, Mathlib exhibits very small length gains but relatively strong dependency and modularity improvements, consistent with a library whose proofs are often already concise but still admit structural refactoring\. By contrast, HepLean and ConNF show much larger length and dependency gains, suggesting that these corpora contain more opportunities for proof compression and simplification\. We treat these repository\-level results as descriptive rather than definitive, since they likely reflect both stylistic differences and variation in theorem composition across projects\.

### 5\.3Overview of Additional Experiments

##### Ablation Studies

Appendix[F\.1](https://arxiv.org/html/2605.22885#A6.SS1)separates the scaffold channels and reports the hyperparameter searches used during training\. The ablation shows that goal\-state traces, informalizations, and retrieved context each help \(albiet with a majority of improvement stemming from the chain\-of\-states annotations\), while the grid searches motivate per\-iteration and per\-metric hyperparameter selection and evolution\.

##### Qualitative Examples

Appendix[F\.2](https://arxiv.org/html/2605.22885#A6.SS2)gives representative optimized proofs from the MiniCTX\-v2 dataset for all three objectives, including provenance and old/new metric scores\. Moreover, we additionally include a case study of evaluation on AI\-generated proofs \(Alphaproof on IMO 2024\(Hubertet al\.,[2025](https://arxiv.org/html/2605.22885#bib.bib10)\)\) with a higher compute budget\.

## 6Limitations and Future Work

In this work, we posit and study a set of particular structural metrics, which may not necessarily align with corpus maintainers’ subjective preferences of proof quality\. Namely, the dependency and modularity metrics measure the number of explicitly named dependencies and effective spawned goals respectively, which are structural formal objects and therefore may carry discrepancies between raw dependency scores and maintainer preferences\. We do not include a maintainer preference study, and future work may wish to address this gap by engineering maintainer preferences directly \(perhaps through informal, LLM\-based metrics\)\. Additionally, future work may also wish to study the effects of training dataset optimization on downstream prover performance\.

Additionally, we study single\-step rewriting rather than full agentic systems\. The scaffold can be exposed as a tool, but we do not evaluate Codex\- or Claude\-Code\-style agents in this particular work as this work primarily focuses on the development and evaluation of our training pipeline and scaffold, and as such, we prioritize the robust evaluation of single\-step rewriting\. However, we do find that stronger optimization often lowers compilation accuracy[5\.2\.5](https://arxiv.org/html/2605.22885#S5.SS2.SSS5.Px1), suggesting that such agents and agentic iterative repair loops are potential methods to balance this trade\-off\.

## 7Conclusion

We have introduced ImProver 2, a pipeline for boosting the formal proof\-optimization ability of small language models\. We have demonstrated the utility of our neurosymbolic augmentations to many varieties of models, showcased iterative self\-improvement using our replay buffer architecture, and introduced two novel metrics \(as well as revisiting an old one\) for practical proof improvement\. We have found that our system leads all evaluated unscaffolded systems on proof modularity, is competitive with the strongest frontier models on dependency, and matches mid\-tier frontier models on length — all from a 7B base model\.

## Acknowledgements

This research is partially supported by the DARPA expMath program through the DARPA CMO contract number HR0011262E028 and NSF Grant DMS\-2434614\. We would like to thank Dr\. Patrick Shafto, expMath Program Manager, for useful technical discussions\.

## References

- T\. Achim, A\. Best, A\. Bietti, K\. Der, M\. Fédérico, S\. Gukov, D\. Halpern\-Leistner, K\. Henningsgard, Y\. Kudryashov, A\. Meiburg, M\. Michelsen, R\. Patterson, E\. Rodriguez, L\. Scharff, V\. Shanker, V\. Sicca, H\. Sowrirajan, A\. Swope, M\. Tamas, V\. Tenev, J\. Thomm, H\. Williams, and L\. Wu \(2025\)Aristotle: imo\-level automated theorem proving\.External Links:2510\.01346,[Link](https://arxiv.org/abs/2510.01346)Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p1.1),[§2](https://arxiv.org/html/2605.22885#S2.p1.1)\.
- ImProver: agent\-based automated proof optimization\.InInternational Conference on Representation Learning,Y\. Yue, A\. Garg, N\. Peng, F\. Sha, and R\. Yu \(Eds\.\),Vol\.2025,pp\. 29521–29543\.External Links:[Link](https://proceedings.iclr.cc/paper_files/paper/2025/file/4864005cfdea7ebd07086ed1b9846825-Paper-Conference.pdf)Cited by:[item 2](https://arxiv.org/html/2605.22885#S1.I1.i2.p1.1),[§1](https://arxiv.org/html/2605.22885#S1.p3.1),[§2](https://arxiv.org/html/2605.22885#S2.p1.1),[§2](https://arxiv.org/html/2605.22885#S2.p2.1),[§3](https://arxiv.org/html/2605.22885#S3.p1.1),[§4\.2\.1](https://arxiv.org/html/2605.22885#S4.SS2.SSS1.Px2.p1.1)\.
- K\. Buzzard and R\. Taylor \(2026\)Fermat’s last theorem\.External Links:[Link](https://imperialcollegelondon.github.io/FLT/blueprint.pdf)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- J\. Chen, W\. Chen, J\. Du, J\. Hu, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, W\. Shi, Z\. Wang, M\. Wang, C\. Wei, S\. Wei, H\. Xin, F\. Yang, W\. Gao, Z\. Yuan, T\. Zhan, Z\. Zheng, T\. Zhou, and T\. H\. Zhu \(2025\)Seed\-prover 1\.5: mastering undergraduate\-level theorem proving via learning from experience\.External Links:2512\.17260,[Link](https://arxiv.org/abs/2512.17260)Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p2.1),[§2](https://arxiv.org/html/2605.22885#S2.p1.1)\.
- DeepSeek\-AI \(2025\)DeepSeek\-r1: incentivizing reasoning capability in llms via reinforcement learning\.External Links:2501\.12948,[Link](https://arxiv.org/abs/2501.12948)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px2.p1.6)\.
- S\. Frieder, J\. Bayer, S\. Looi, J\. Loader, J\. Berner, K\. M\. Collins, A\. Juhász, F\. Ruehle, S\. Welleck, G\. Poesia, R\. Griffiths, A\. Weller, A\. Goyal, C\. Freer, T\. Lukasiewicz, and T\. Gowers \(2025\)Data for mathematical copilots: better ways of presenting proofs for machine learning\.External Links:2412\.15184,[Link](https://arxiv.org/abs/2412.15184)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p1.1)\.
- A\. Gu, B\. Piotrowski, F\. Gloeckle, K\. Yang, and A\. H\. Markosyan \(2025\)ProofOptimizer: training language models to simplify proofs without human demonstrations\.InThe 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025,External Links:[Link](https://openreview.net/forum?id=ghxS7M35FU)Cited by:[item 2](https://arxiv.org/html/2605.22885#S1.I1.i2.p1.1),[§1](https://arxiv.org/html/2605.22885#S1.p2.1),[§2](https://arxiv.org/html/2605.22885#S2.p2.1),[§3](https://arxiv.org/html/2605.22885#S3.p1.1)\.
- S\. Hattori, T\. Matsuzaki, and M\. Fujiwara \(2025\)Natural language translation of formal proofs through informalization of proof steps and recursive summarization along proof structure\.InProceedings of the 18th International Natural Language Generation Conference,L\. Flek, S\. Narayan, L\. H\. Phuong, and J\. Pei \(Eds\.\),Hanoi, Vietnam,pp\. 376–389\.External Links:[Link](https://aclanthology.org/2025.inlg-main.23/)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p2.1)\.
- T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom, O\. Bertolli, T\. Zahavy, A\. Mandhane, J\. Yung, I\. Beloshapka, B\. Ibarz, V\. Veeriah, L\. Yu, O\. Nash, P\. Lezeau, S\. Mercuri, C\. Sönne, B\. Mehta, A\. Davies, D\. Zheng, F\. Pedregosa, Y\. Li, I\. von Glehn, M\. Rowland, S\. Albanie, A\. Velingker, S\. Schmitt, E\. Lockhart, E\. Hughes, H\. Michalewski, N\. Sonnerat, D\. Hassabis, P\. Kohli, and D\. Silver \(2025\)Olympiad‐level formal mathematical reasoning with reinforcement learning\.Nature\.Note:Published: 12 November 2025External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y),[Link](https://www.nature.com/articles/s41586-025-09833-y)Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p1.1),[§2](https://arxiv.org/html/2605.22885#S2.p1.1),[§5\.3](https://arxiv.org/html/2605.22885#S5.SS3.SSS0.Px2.p1.1)\.
- A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample \(2023\)Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs\.InInternational Conference on Learning Representations,External Links:[Link](https://doi.org/10.48550/arXiv.2210.12283)Cited by:[§4\.2\.1](https://arxiv.org/html/2605.22885#S4.SS2.SSS1.Px3.p1.1)\.
- Z\. Li, J\. Sun, L\. Murphy, Q\. Su, Z\. Li, X\. Zhang, K\. Yang, and X\. Si \(2024\)A survey on deep learning for theorem proving\.InFirst Conference on Language Modeling,External Links:[Link](https://openreview.net/forum?id=zlw6AHwukB)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p1.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun, J\. Wu, J\. Gesi, X\. Lu, D\. Acuna, K\. Yang, H\. Lin, Y\. Choi, D\. Chen, S\. Arora, and C\. Jin \(2025\)Goedel\-Prover\-V2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.External Links:2508\.03613,[Link](https://arxiv.org/abs/2508.03613)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p1.1)\.
- P\. Lu, L\. Qiu, W\. Yu, S\. Welleck, and K\. Chang \(2023\)A survey of deep learning for mathematical reasoning\.InProceedings of the 61st Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),A\. Rogers, J\. Boyd\-Graber, and N\. Okazaki \(Eds\.\),Toronto, Canada,pp\. 14605–14631\.External Links:[Link](https://aclanthology.org/2023.acl-long.817/),[Document](https://dx.doi.org/10.18653/v1/2023.acl-long.817)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p1.1)\.
- L\. d\. Moura and S\. Ullrich \(2021\)The lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28,A\. Platzer and G\. Sutcliffe \(Eds\.\),Cham,pp\. 625–635\.External Links:ISBN 978\-3\-030\-79876\-5Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p1.1),[§2](https://arxiv.org/html/2605.22885#S2.p1.1),[§3\.1](https://arxiv.org/html/2605.22885#S3.SS1.p3.1)\.
- R\. Y\. Pang, W\. Yuan, K\. Cho, H\. He, S\. Sukhbaatar, and J\. Weston \(2024\)Iterative reasoning preference optimization\.External Links:2404\.19733,[Link](https://arxiv.org/abs/2404.19733)Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p4.1),[item 3](https://arxiv.org/html/2605.22885#S4.I1.i3.p1.4),[§4\.3](https://arxiv.org/html/2605.22885#S4.SS3.p1.1)\.
- S\. Polu and I\. Sutskever \(2020\)Generative language modeling for automated theorem proving\.External Links:2009\.03393,[Link](https://arxiv.org/abs/2009.03393)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p1.1),[§2](https://arxiv.org/html/2605.22885#S2.p2.1)\.
- S\. Saito and M\. Noguchi \(2026\)Foundation\.External Links:[Link](https://github.com/FormalizedFormalLogic/Foundation)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- I\. Sergeev, M\. Dvorak, T\. Figueroa\-Reid, R\. Hamadani, B\. Hwang, E\. Karunus, V\. Kolmogorov, A\. Meiburg, P\. Nelson, and M\. Sandey \(2026\)Regularity of 1\-, 2\-, and 3\-sums of matroids\.External Links:[Link](https://ivan-sergeyev.github.io/seymour/blueprint.pdf)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- I\. Shumailov, Z\. Shumaylov, Y\. Zhao, N\. Papernot, R\. Anderson, and Y\. Gal \(2024\)AI models collapse when trained on recursively generated data\.Nature,pp\. 755–759\.External Links:[Link](https://doi.org/10.1038/s41586-024-07566-y)Cited by:[§4\.3\.1](https://arxiv.org/html/2605.22885#S4.SS3.SSS1.p1.1)\.
- T\. Tao \(2026\)PFR blueprint\.External Links:[Link](https://teorth.github.io/pfr/blueprint.pdf)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- The Coq Development Team \(2024\)The coq proof assistantExternal Links:[Document](https://dx.doi.org/10.5281/zenodo.14542673),[Link](https://doi.org/10.5281/zenodo.14542673)Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p1.1)\.
- The Mathlib Community \(2020\)The lean mathematical library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,CPP 2020,New York, NY, USA,pp\. 367–381\.External Links:ISBN 9781450370974,[Link](https://doi.org/10.1145/3372885.3373824),[Document](https://dx.doi.org/10.1145/3372885.3373824)Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p1.1),[§1](https://arxiv.org/html/2605.22885#S1.p2.1),[1st item](https://arxiv.org/html/2605.22885#S3.I1.i1.p1.1),[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- J\. Tooby\-Smith \(2025\)HepLean: digitalising high energy physics\.Computer Physics Communications308,pp\. 109457\.External Links:ISSN 0010\-4655,[Document](https://dx.doi.org/https%3A//doi.org/10.1016/j.cpc.2024.109457),[Link](https://www.sciencedirect.com/science/article/pii/S0010465524003801)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- F\. van Doorn, M\. Rothgang, P\. Monticone, J\. T\. J\. Rui, J\. Sundstrom, M\. I\. de Frutos\-Fernández, R\. V\. de Velde, S\. Gouezel, L\. Diedering, J\. Portegies, and J\. Roos \(2026\)Formalizing carleson’s theorem in lean\.External Links:[Link](https://florisvandoorn.com/carleson/)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- M\. Wenzel, L\. C\. Paulson, and T\. Nipkow \(2008\)The isabelle framework\.InTheorem Proving in Higher Order Logics,O\. A\. Mohamed, C\. Muñoz, and S\. Tahar \(Eds\.\),Berlin, Heidelberg,pp\. 33–38\.External Links:ISBN 978\-3\-540\-71067\-7Cited by:[§1](https://arxiv.org/html/2605.22885#S1.p1.1)\.
- S\. Wilshaw \(2026\)New foundations is consistent\.External Links:[Link](https://leanprover-community.github.io/con-nf/print/print.pdf)Cited by:[§5\.1](https://arxiv.org/html/2605.22885#S5.SS1.SSS0.Px1.p1.1)\.
- K\. Yang, A\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar \(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InNeural Information Processing Systems \(NeurIPS\),External Links:[Link](https://icml.cc/virtual/2023/27190)Cited by:[§2](https://arxiv.org/html/2605.22885#S2.p1.1),[§2](https://arxiv.org/html/2605.22885#S2.p2.1)\.

## Appendix AFormal Definition of the Modularity Metric

This appendix presents a precise, proof\-theoretic and type\-theoretic definition of the modularity metricμmod\\mu\_\{\\mathrm\{mod\}\}used throughout the paper, matching its concrete implementation in Lean 4\. We proceed from first principles, beginning with Lean’s elaboration semantics, and culminate in the exact algorithm used to count effective spawned goals\.

### A\.1Lean Elaboration Semantics

Lean elaborates tactic proofs by incrementally constructing and solving metavariables\. At any point in elaboration, the system maintains a metavariable contextM=\(Δ,σ\)M=\(\\Delta,\\sigma\)whereΔ\\Deltais a finite set of metavariable declarations of the form?m:\(Γ?​m⊢A?​m\)?m:\(\\Gamma\_\{?m\}\\vdash A\_\{?m\}\), with local contextΓ?​m\\Gamma\_\{?m\}and target typeA?​mA\_\{?m\}\. Similarly,σ\\sigmais a partial assignment mapping metavariables to terms\.

A goal is an unassigned metavariable?​m∈Δ∖dom​\(σ\)?m\\in\\Delta\\setminus\\mathrm\{dom\}\(\\sigma\)\. At elaboration stepii, Lean maintains a list of*active goals*𝒜i\\mathcal\{A\}\_\{i\}\.

Each tactic stepτi\\tau\_\{i\}:

1. 1\.Focuses a goal?​mi∈𝒜i?m\_\{i\}\\in\\mathcal\{A\}\_\{i\},
2. 2\.Produces an assignmentσi\+1​\(?​mi\)=ti\\sigma\_\{i\+1\}\(?m\_\{i\}\)=t\_\{i\},
3. 3\.Potentially introduces new metavariables corresponding to subgoals\.

The set of newly created metavariables is exactly the set of free metavariables occurring intit\_\{i\}after assignment\.

### A\.2Direct Children vs\. Spawned Goals

LetChildren​\(τi\)\\mathrm\{Children\}\(\\tau\_\{i\}\)denote the set of metavariables that occur free intit\_\{i\}and therefore represent*direct subgoals*of the focused goal?​mi?m\_\{i\}\.

However, Lean tactics may surface additional obligations that are*not*direct children of?​mi?m\_\{i\}\. These arise from nested tactic blocks \(e\.g\.have,calc,by\), automation introducing auxiliary lemmas, goal defocus/refocus patterns, tactics that internally elaborate subproofs, etc\.

To capture this distinction, define:

Currenti=\{?​mi\}∪Children​\(τi\),\\mathrm\{Current\}\_\{i\}=\\\{?m\_\{i\}\\\}\\cup\\mathrm\{Children\}\(\\tau\_\{i\}\),and letSiS\_\{i\}be the set of all metavariables that have previously appeared as children:Si\+1=Si∪Children​\(τi\)S\_\{i\+1\}=S\_\{i\}\\cup\\mathrm\{Children\}\(\\tau\_\{i\}\)\.

###### Definition 1\(Spawned Goals\)\.

The*spawned goals*of stepτi\\tau\_\{i\}are defined as:

Spawned​\(τi\)=\(Currenti∖Children​\(τi\)\)∖Si\.\\mathrm\{Spawned\}\(\\tau\_\{i\}\)=\\bigl\(\\mathrm\{Current\}\_\{i\}\\setminus\\mathrm\{Children\}\(\\tau\_\{i\}\)\\bigr\)\\setminus S\_\{i\}\.

Intuitively, these are goals that first appear at stepii, are not logical subgoals of the focused goal, correspond to independent subproof obligations\.

### A\.3Proof Graph over Steps

We represent a proof as a directed graph over steps rather than metavariables\.

Let steps be indexed byi=1,…,Ti=1,\\dots,T\. We define:

- •A*normal edge*i→ji\\to jif the goal solved at stepjjis a direct child of stepii\.
- •A*spawned edge*i↝ji\\rightsquigarrow jif the goal solved at stepjjwas spawned at stepii\.

This yields a labeled directed forest

\(V,Enormal,Espawned\),\(V,E\_\{\\mathrm\{normal\}\},E\_\{\\mathrm\{spawned\}\}\),withEspawned⊆EnormalE\_\{\\mathrm\{spawned\}\}\\subseteq E\_\{\\mathrm\{normal\}\}\. We refer to this as the proof tree\.

### A\.4Canonical Goal Representation

To prevent adversarial or spurious inflation of modularity, goals are compared modulo definitional equality,α\\alpha\-equivalence, and universal abstraction\.

Each goal is assigned a canonical representation consisting of:

- •A base target hash,
- •A sorted list of hypothesis type hashes \(proof\-relevant hypotheses only\),
- •A set of sequent variant hashes, obtained by progressively discharging∀\\forall\-binders and implications,
- •A set of target\-only variant hashes, used for wrapper detection\.

All hashes are computed afterβ​δ​ι\\beta\\delta\\iota\-normalization, metadata erasure, binder name scrubbing \(forα\\alpha\-invariance\), and replacement of free variables by deterministic canonical constants\.

This representation ensures that goals differing only by irrelevant syntactic structure or parameter order are identified\.

### A\.5Duplicate and Wrapper Detection

A spawned goal is considered duplicate and discarded if either:

1. 1\.Its sequent variant hash matches any previously seen goal \(global duplicate\), or
2. 2\.Its target is a definitional wrapper of its parent goal, i\.e\.target​\(gchild\)∈targetVariants​\(gparent\)\\text\{target\}\(g\_\{\\text\{child\}\}\)\\in\\text\{targetVariants\}\(g\_\{\\text\{parent\}\}\)or vice versa\.

This eliminates the potential for many types of reward hacking cases, such as trivial∀\\forall\-introductions, restatements of the parent goal, and redundant lemma spawning\.

### A\.6Nontriviality Filter

LetTgT\_\{g\}be the subtree of steps rooted at a spawned goalgg\.

We require\|Tg\|\>2\|T\_\{g\}\|\>2, ensuring that the goal is not solved immediately, and namely, the goal is not discharged by a single automation step\.

This empirically excludes trivial goals solvable by tactics such assimp,tauto,linarith,ring,aesop, orgrind\.

### A\.7Effectiveness via Fixed\-Point Semantics

Let each spawned goalggintroduce a set of proof variables𝖨𝗇𝗍𝗋𝗈​\(g\)\\mathsf\{Intro\}\(g\)corresponding to hypotheses unavailable in the parent context\.

We define a spawned subtree rooted atggto be effective if its introduced hypotheses are used in the main \(non\-spawned\) proof, or in another spawned subtree that is itself effective\.

Formally, define a monotone operatorΦ\\Phion sets of spawned roots:

Φ\(S\)=\{g∣𝖨𝗇𝗍𝗋𝗈\(g\)is used outside all spawned subtrees\\displaystyle\\Phi\(S\)=\\\{g\\mid\\mathsf\{Intro\}\(g\)\\text\{ is used outside all spawned subtrees\}\\newline∨∃g′∈S,g′≠g,𝖨𝗇𝗍𝗋𝗈\(g\)used in subtreeg′\}\.\\displaystyle\\vee\\ \\exists g^\{\\prime\}\\in S,\\,g^\{\\prime\}\\neq g,\\ \\mathsf\{Intro\}\(g\)\\text\{ used in subtree \}g^\{\\prime\}\\\}\.
###### Definition 2\(Effective Spawned Goals\)\.

The set of effective spawned goals is the least fixed point ofΦ\\Phi\.

This is computed by standard fixed\-point iteration, guaranteed to terminate since the set of spawned roots is finite\.

### A\.8Modularity Metric

###### Definition 3\(Modularity Metric\)\.

Given a verified proofyyof\(c,x\)\(c,x\), letℰ​\(y\)\\mathcal\{E\}\(y\)be the set of effective spawned goals\. The modularity metric is defined as:

μmod​\(c,x,y\)=\|ℰ​\(y\)\|\.\\mu\_\{\\mathrm\{mod\}\}\(c,x,y\)=\|\\mathcal\{E\}\(y\)\|\.

## Appendix BContext Extraction

To facilitate extraction of relevant context from the proof environment, we consider the Lean 4 concrete syntax tree \(CST\) and abstract syntax tree \(AST\)\. The CST preserves surface tokens and references locations in source code; the AST resolves names, binds variables, and canonicalizes declarations \(e\.g\., definitions/theorems/structure/etc\. nodes\)\. Context extraction uses both:

- •CST view \(textual reachability\): harvest all surface identifiers and their source spans that occur inxxand in the proof text ofy0y\_\{0\}\.
- •AST view \(semantic reachability\): resolve those identifiers to fully qualified symbols under the language’s environment \(imports, namespaces, instances, modules\); record declaration categories \(e\.g\., definition, theorem\) and provenance \(module/package\)\.

##### Graphs and the slice\.

From the AST we build two standard graphs: \(i\) an import DAG over files/modules, and \(ii\) an entity graph whose vertices are declarations \(constants, lemmas, definitions\) with edges for semantic references \(uses in types/bodies\)\. Let𝗍𝗈𝗎𝖼𝗁​\(x,y0\)\\mathsf\{touch\}\(x,y\_\{0\}\)be the set of AST nodes directly referenced by the CST identifiers collected fromxxandy0y\_\{0\}\(optionally augmented by a dynamic trace of proof states, if available\)\. The context slice is the subgraph

S​\(c,x,y0\)=Reach​\(Gent,\(𝗍𝗈𝗎𝖼𝗁​\(x,y0\)\)\)S\(c,x,y\_\{0\}\)=\\mathrm\{Reach\}\\big\(G\_\{\\mathrm\{ent\}\},\\big\(\\mathsf\{touch\}\(x,y\_\{0\}\)\\big\)\\big\)optionally restricted by the import DAG to a budgeted neighborhood\. We then serialize each element ofSSwith metadata as to its object type \(e\.g\. lemma, definition, etc\.\), as well as a stable snippet of its source content\.

Because selection is driven by AST resolution,Ψctx\\Psi\_\{\\text\{ctx\}\}is invariant to superficial edits \(whitespace, formatting\) and robust to local refactors \(α\\alpha\-renaming within a module\)\. The slice size grows with the reachable subgraph, not raw file size, yielding a compact, minimal, and deterministic bundle of proof context that is read\-only with respect to the program state\.

## Appendix CReplay Buffer and Dataset Construction Details

We provide a more detailed overview of the replay buffer algorithm\. Given the problem set𝒫=𝒫train∪𝒫test\\mathcal\{P\}=\\mathcal\{P\}\_\{\\mathrm\{train\}\}\\cup\\mathcal\{P\}\_\{\\mathrm\{test\}\}and the current iterationttmodelGtG\_\{t\}, we run generation as described in §[4\.2](https://arxiv.org/html/2605.22885#S4.SS2)to obtainnncandidate proofs per problem in𝒫train\\mathcal\{P\}\_\{\\mathrm\{train\}\}\. This yields the raw \(no\-replay\) dataset:

𝒟nr\(t\)\\displaystyle\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{nr\}\}=\{\(cT,xT,yT,0,\{\(yT,i,s^T,i\)\}i=1n\)\}T∈𝒫train\\displaystyle=\\\{\(c\_\{T\},x\_\{T\},y\_\{T,0\},\\\{\(y\_\{T,i\},\\widehat\{s\}\_\{T,i\}\)\\\}\_\{i=1\}^\{n\}\)\\\}\_\{T\\in\\mathcal\{P\}\_\{\\mathrm\{train\}\}\}=\{\(cT,xT,yT,0,𝒴T\(t\)\)\}T∈𝒫train\\displaystyle=\\\{\(c\_\{T\},x\_\{T\},y\_\{T,0\},\\mathcal\{Y\}\_\{T\}^\{\(t\)\}\)\\\}\_\{T\\in\\mathcal\{P\}\_\{\\mathrm\{train\}\}\}wheres^T,i=Sμ​\(yT,i,yT,0∥cT,xT\)\\widehat\{s\}\_\{T,i\}=S\_\{\\mu\}\(y\_\{T,i\},y\_\{T,0\}\\\|c\_\{T\},x\_\{T\}\)is the improvement score of candidateyT,iy\_\{T,i\}over the baselineyT,0y\_\{T,0\}\.

We then construct the solutions \(replay\) dataset𝒟re\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{re\}\}by post\-processing𝒟nr\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{nr\}\}together with the previous iteration’s already post\-processed dataset𝒟re\(t−1\)\\mathcal\{D\}^\{\(t\-1\)\}\_\{\\mathrm\{re\}\}\. The procedure is parameterized by a target replay proportionρ∈\[0,1\]\\rho\\in\[0,1\], replay modemode∈\{mark,join,replace\}\\in\\\{\\texttt\{mark\},\\texttt\{join\},\\texttt\{replace\}\\\}, an improvement\-rate capπmax∈\[0,1\]\\pi\_\{\\max\}\\in\[0,1\], and a minimum gapγ∈\[0,1\]\\gamma\\in\[0,1\]\.

##### Improvement rate and eligibility\.

Additionally, for problemTT, define its improvement rate at iterationjjby

πT\(j\)=1n​∑i=1n𝕀​\[v​\(cT,xT,yT,i\(j\)\)=1∧s^T,i\(j\)\>0\]\.\\pi\_\{T\}^\{\(j\)\}=\\frac\{1\}\{n\}\\sum\_\{i=1\}^\{n\}\\mathbb\{I\}\\\!\\left\[\\text\{v\}\(c\_\{T\},x\_\{T\},y\_\{T,i\}^\{\(j\)\}\)=1\\ \\wedge\\ \\widehat\{s\}\_\{T,i\}^\{\(j\)\}\>0\\right\]\.A problem is replay\-eligible at iterationttiff it had at least one improved, compiling solution in some previous iterationj<tj<t\. We maintain a reservoirℰ\\mathcal\{E\}of replay\-eligible problems with preference for “easy” items \(largestπT\(j\)\\pi\_\{T\}^\{\(j\)\}acrossj<tj<t\)\.

##### Replay buffer construction

We proceed now to construct the post\-replay buffer dataset in two main steps:

1. 1\.Mark:We first mark problems in𝒟nr\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{nr\}\}asreplayorfrontierso that the fraction of replay equalsρ\\rho: 1. \(a\)Start with the subset of problems that are replay\-eligible; if their fraction exceedsρ\\rho, downsample them by removing highest\-πT\\pi\_\{T\}items \(i\.e\. the “easiest”\) until the replay fraction isρ\\rho\(cap atπmax\\pi\_\{\\max\}\)\. 2. \(b\)If their fraction is belowρ\\rho, replace uniformly chosen frontier items by items sampled from the reservoirℰ\\mathcal\{E\}\(taken from𝒟re\(t−1\)\\mathcal\{D\}^\{\(t\-1\)\}\_\{\\mathrm\{re\}\}\) until the replay fraction reachesρ\\rhoas best as possible\. This keeps dataset size fixed while achieving the target mix\. After this step, every item in the dataset is tagged asreplayorfrontierand the target mix is satisfied\.
2. 2\.Merge For each item markedreplaywith key\(cT,xT,yT,0\)\(c\_\{T\},x\_\{T\},y\_\{T,0\}\), find its counterpart in𝒟re\(t−1\)\\mathcal\{D\}^\{\(t\-1\)\}\_\{\\mathrm\{re\}\}, say with candidate \(multi\)set𝒴~T\(t−1\)\\mathcal\{\\widetilde\{Y\}\}^\{\(t\-1\)\}\_\{T\}\. Then, we case onmodeas follows: - •join: set the current candidates to the union𝒴~T\(t\)=𝒴T\(t\)∪𝒴~T\(t−1\)\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}=\\mathcal\{Y\}^\{\(t\)\}\_\{T\}\\cup\\mathcal\{\\widetilde\{Y\}\}^\{\(t\-1\)\}\_\{T\}\(deduplicated by normalized proof text\)\. This increases candidate diversity for IRPO\. - •replace: set𝒴~T\(t\)=𝒴~T\(t−1\)\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}=\\mathcal\{\\widetilde\{Y\}\}^\{\(t\-1\)\}\_\{T\}, i\.e\., overwrite the current candidates by the previous iteration’s\. Ifmodeismark, skip this step \(no candidate\-level splice\)\. In other words, set𝒴~T\(t\)=𝒴T\(t\)\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}=\\mathcal\{Y\}^\{\(t\)\}\_\{T\}

With this, we obtain the replay dataset:

𝒟re\(t\)=\{\(cT,xT,yT,0,𝒴~T\(t\)\)\|T∈𝒫train\}\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{re\}\}=\\Big\\\{\\,\\big\(c\_\{T\},x\_\{T\},y\_\{T,0\},\\ \\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}\\big\)\\ \\Big\|\\ T\\in\\mathcal\{P\}\_\{\\mathrm\{train\}\}\\Big\\\}

##### Filtering

Finally, we post\-process𝒟re\(t\)\\mathcal\{D\}^\{\(t\)\}\_\{\\mathrm\{re\}\}by filtering out low\-quality candidates and separating the samples into winner \(WW\) and loser \(LL\) sets\. Specifically, we filter the high improvement rate problems \(those which were sufficiently “easy” for the model to improve on many candidates\) by removing problemsTTwithπT\(t\)\>πmax\\pi\_\{T\}^\{\(t\)\}\>\\pi\_\{\\max\}\. Namely, we define𝒫~\(t\)=𝒫train∖\{T∣πT\(t\)\>πmax\}\\widetilde\{\\mathcal\{P\}\}^\{\(t\)\}=\\mathcal\{P\}\_\{\\mathrm\{train\}\}\\setminus\\\{T\\mid\\pi\_\{T\}^\{\(t\)\}\>\\pi\_\{\\max\}\\\}to be the filtered problem set\.

Then, for each problemTTin𝒫~\(t\)\\widetilde\{\\mathcal\{P\}\}^\{\(t\)\}, we partition𝒴~T\(t\)=WT\(t\)∪LT\(t\)\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}=W\_\{T\}^\{\(t\)\}\\cup L\_\{T\}^\{\(t\)\}such that:

- •WT\(t\)=\{y∈𝒴~T\(t\)∣v​\(cT,xT,y\)=1∧s^T,y\>δ\(t\)\}W\_\{T\}^\{\(t\)\}=\\\{y\\in\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}\\mid\\text\{v\}\(c\_\{T\},x\_\{T\},y\)=1\\land\\widehat\{s\}\_\{T,y\}\>\\delta^\{\(t\)\}\\\}, whereδ\(t\)\\delta^\{\(t\)\}is theγ\\gamma\-th percentile of all scores\{s^T,i:T∈𝒫~\(t\),yi∈𝒴~T\(t\)\}\\\{\\widehat\{s\}\_\{T,i\}:T\\in\\widetilde\{\\mathcal\{P\}\}^\{\(t\)\},y\_\{i\}\\in\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}\\\}\.
- •LT\(t\)=𝒴~T\(t\)∖WT\(t\)L\_\{T\}^\{\(t\)\}=\\mathcal\{\\widetilde\{Y\}\}^\{\(t\)\}\_\{T\}\\setminus W\_\{T\}^\{\(t\)\}\.

In other words, winners are those candidates that compile and have an improvement score above theγ\\gamma\-th percentile threshold across all samples in the dataset, while losers are the rest\.

With this, we finalize the filtered post\-replay buffer dataset as:

𝒟fil\(t\)=\{\(cT,xT,yT,0,WT\(t\),LT\(t\)\)∣T∈𝒫~\(t\)\}\\mathcal\{D\}\_\{\\text\{fil\}\}^\{\(t\)\}=\\Big\\\{\(c\_\{T\},x\_\{T\},y\_\{T,0\},W\_\{T\}^\{\(t\)\},L\_\{T\}^\{\(t\)\}\)\\mid T\\in\\widetilde\{\\mathcal\{P\}\}^\{\(t\)\}\\Big\\\}

##### IRPO Dataset

As IRPO is a preference\-based training method, we now convert𝒟fil\(t\)\\mathcal\{D\}\_\{\\text\{fil\}\}^\{\(t\)\}into a set of preference pairs\. This process is parameterized by two hyperparametersW,L∈ℕW,L\\in\\mathbb\{N\}, which control the number of winners and losers to sample per problem, respectively\.

First, for a given problemTTin𝒫~\(t\)\\widetilde\{\\mathcal\{P\}\}^\{\(t\)\}, we deduplicateWT\(t\)W\_\{T\}^\{\(t\)\}by equal scoress^T,i=s^T,j\\widehat\{s\}\_\{T,i\}=\\widehat\{s\}\_\{T,j\}and deduplicateLT\(t\)L\_\{T\}^\{\(t\)\}by string equality\.

With this, we form two families of preference pairs:

𝔓Tℓ→w=\{\(b,g\):b∈LT\(t\),g∈WT\(t\)\}\\mathfrak\{P\}^\{\\ell\\to w\}\_\{T\}=\\\{\(b,g\):b\\in L\_\{T\}^\{\(t\)\},\\ g\\in W\_\{T\}^\{\(t\)\}\\\}𝔓Tw→w=\{\(g′,g\):g,g′∈WT\(t\),s^T,g\>s^T,g′\}\.\\mathfrak\{P\}^\{w\\to w\}\_\{T\}=\\\{\(g^\{\\prime\},g\):g,g^\{\\prime\}\\in W\_\{T\}^\{\(t\)\},\\ \\widehat\{s\}\_\{T,g\}\>\\widehat\{s\}\_\{T,g^\{\\prime\}\}\\\}\.
And with this, we form our IRPO training dataset as the following set:

𝒟IRPO\(t\)=⋃T∈𝒫~\(t\)\(𝔓Tℓ→w∪𝔓Tw→w\)\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}=\\bigcup\_\{T\\in\\widetilde\{\\mathcal\{P\}\}^\{\(t\)\}\}\(\\mathfrak\{P\}^\{\\ell\\to w\}\_\{T\}\\cup\\mathfrak\{P\}^\{w\\to w\}\_\{T\}\)Which can be reinterpreted elementwise as a collection of tuples\(cT,xT,yT,0,yT,ℓ,yT,w\)\(c\_\{T\},x\_\{T\},y\_\{T,0\},y\_\{T,\\ell\},y\_\{T,w\}\)\.

Algorithm 1Preference Pair CreationInput:filtered dataset

𝒟fil\(t\)\\mathcal\{D\}\_\{\\text\{fil\}\}^\{\(t\)\}, hyperparameters

W∈ℕW\\in\\mathbb\{N\}and

L∈ℕL\\in\\mathbb\{N\}
Initialize

𝒟IRPO\(t\)=\[\]\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}=\[\\ \]
for

TTin

𝒟fil\(t\)\\mathcal\{D\}\_\{\\text\{fil\}\}^\{\(t\)\}do

De\-duplicate

WT\(t\)W\_\{T\}^\{\(t\)\}by total improvement score

De\-duplicate

LT\(t\)L\_\{T\}^\{\(t\)\}by string equality

Discard or duplicate elements uniformly at random until

\|WT\(t\)\|=W\|W\_\{T\}^\{\(t\)\}\|=Wand

\|LT\(t\)\|=L\|L\_\{T\}^\{\(t\)\}\|=L
for

w1w\_\{1\}in

WT\(t\)W\_\{T\}^\{\(t\)\}do

for

w2w\_\{2\}in

WT\(t\)W\_\{T\}^\{\(t\)\}do

if

μ​\(c,x,w1\)\>μ​\(c,x,w2\)\\mu\(c,x,w\_\{1\}\)\>\\mu\(c,x,w\_\{2\}\)then

𝒟IRPO\(t\):=\(w1,w2\)​::​𝒟IRPO\(t\)\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}:=\(w\_\{1\},w\_\{2\}\)\\texttt\{::\}\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}

endif

endfor

endfor

for

wwin

WT\(t\)W\_\{T\}^\{\(t\)\}do

for

llin

LT\(t\)L\_\{T\}^\{\(t\)\}do

𝒟IRPO\(t\):=\(w,l\)​::​𝒟IRPO\(t\)\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}:=\(w,l\)\\texttt\{::\}\\mathcal\{D\}\_\{\\text\{IRPO\}\}^\{\(t\)\}

endfor

endfor

endfor

## Appendix DChain\-of\-States Implementation

Given a verified proofy0y\_\{0\}, let its tactic steps be indexed byi=1,…,Ti=1,\\dots,T\. From theInfoTreewe obtain for each step\(goalsBeforei,goalsAfteri\)\(\\texttt\{goalsBefore\}\_\{i\},\\texttt\{goalsAfter\}\_\{i\}\)and a pretty\-printed tactic\. We define

Ψcos​\(y0\)=⟨\(goalsBeforei,τi,goalsAfteri\)⟩i=1T,\\Psi\_\{\\text\{cos\}\}\(y\_\{0\}\)\\ =\\ \\big\\langle\\,\(\\texttt\{goalsBefore\}\_\{i\},\\ \\tau\_\{i\},\\ \\texttt\{goalsAfter\}\_\{i\}\)\\,\\big\\rangle\_\{i=1\}^\{T\},and serialize each triple as a short snippet where goal lists are pretty\-printed into comments adjacent toτi\\tau\_\{i\}\. This turns hidden kernel states into explicit cues the model can condition on\.

## Appendix ESystem Configuration

### E\.1Compute Resources

All local model training and evaluation runs were performed on a machine with 8 NVIDIA L40S GPUs\. Local evaluations used this same GPU pool for batched best@nngeneration and Lean verification\. Closed\-source and hosted API baselines were accessed through OpenRouter; for these models, compute was provided by the API provider rather than by our local hardware\. We report the inference token costs used for the API baselines in Table[5\.2](https://arxiv.org/html/2605.22885#S5.SS2)\.

### E\.2Training

Training uses the same fixed systems configuration across metrics and IRPO rounds, while the main optimization hyperparameters are selected separately for each metric and iteration by validation grid search\. In particular, the preference gap, replay\-buffer ratio, learning rate, and related selection thresholds are tuned per round; the resulting searches are reported in Figures[9](https://arxiv.org/html/2605.22885#A6.F9)and[10](https://arxiv.org/html/2605.22885#A6.F10)\. Unless otherwise stated, each training run uses the following fixed configuration:

- •micro\-batch size: 1 example per GPU, with gradient accumulation 1, for an effective batch size of 8 examples across 8 GPUs;
- •epochs: 1;
- •optimizer:adamw\_torch;
- •learning\-rate scheduler: cosine, with 5 warmup steps;
- •weight decay: 0\.0 and maximum gradient norm: 1\.0;
- •precision and memory settings: bf16, FlashAttention\-2, gradient checkpointing, and DeepSpeed ZeRO\-3 CPU offload\.

Figure[7\(a\)](https://arxiv.org/html/2605.22885#A5.F7.sf1)–[7\(c\)](https://arxiv.org/html/2605.22885#A5.F7.sf3)shows representative training traces for the third dependency\-optimization round\.

![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/IRPO_Dependency_Iter_3_Acc.png)\(a\)Training accuracy over time on iteration 3 of the dependency metric\.
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/IRPO_Dependency_Iter_3_Loss.png)\(b\)Training loss over time on iteration 3 of the dependency metric\. Loss exhibits an overall downward trend\.
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/IRPO_Dependency_Iter_3_Margin.png)\(c\)Average margin over time during training on iteration 3 of the dependency metric\.

Figure 7:Training statistics during iteration 3 of the dependency metric\. Model shows stable performance despite overall regression on this iteration\.
### E\.3System Prompts

During generation, ImProver 2 is prompted by combining the following prompts: depending on the metric, we take one of thelength,modularity, ordependencyprompts, and append theannotation,context, andexamplesprompts along with the relevant neurosymbolic augmentation in the correct locations\.

##### Length:

You are an expert Lean4 theorem rewriting assistant\. Shorten the current Lean4 theorem \(wrapped in <CURRENT\>\.\.\.</CURRENT\>\) to be as short as possible in length \- measured in the number of tactics in the proof \- while also ensuring that the output is still a correct proof of the theorem\. Be sure to output your final response as a Lean4 theorem wrapped in <IMPROVED\>\.\.\.</IMPROVED\> tags, as shown in the example\. Namely, only return the statement and proof of the current theorem in Lean4 code, wrapped in <IMPROVED\>\.\.\.</IMPROVED\> tags\. Do not include any other text or comments\.

##### Modularity:

You are an expert Lean4 theorem rewriting assistant\. Given a Lean4 theorem enclosed in <CURRENT\>\.\.\.</CURRENT\> tags, rewrite the theorem to be as modular and declarative as possible\. Modularity is defined by the number of independent, meaningful subproofs, measured by the occurrence of tactics that spawn new goals \(such as ’have’ statements, case splits, automation tactics, or ’calc’ blocks\) \-\- with the caveat that these subproofs must be nontrivial and contribute to the overall proof structure\. That means any sort of duplicate, unused, or trivial spawned goals will be ignored and/or penalized; this includes trivial modifications to spawned goals such as changing binders into forall statements\. etc\. Your objective is to maximize the number of these useful, nontrivial, and interesting spawned subproofs, while ensuring that the theorem remains correct and is clearly structured and readable\. Optimize and rewrite the proof structure based on genuine sub\-arguments, not superficial goal spawning\. Validate that the revised theorem remains correct and that improvements in modularity are nontrivial and significant\. In your output, only provide the improved statement and proof, wrapped in <IMPROVED\>\.\.\.</IMPROVED\> tags, with no additional text or comments\. Under no circumstances should you create artificial or superficial modularity in order to optimize for or maximize a reward metric; prioritize exclusively genuine mathematical quality and proof clarity over any gamified optimization\.

##### Dependency:

You are an expert Lean4 theorem rewriting assistant\. Rewrite the current Lean4 theorem \(wrapped in <CURRENT\>\.\.\.</CURRENT\>\) to be as independent of external theorems and lemmas as possible\. Namely, you aim to rewrite the proof to minimize the number of external dependencies \- while also ensuring that the output is still a correct proof of the theorem\. Be sure to output your final response as a Lean4 theorem wrapped in <IMPROVED\>\.\.\.</IMPROVED\> tags, as shown in the example\. Namely, only return the statement and proof of the current theorem in Lean4 code, wrapped in <IMPROVED\>\.\.\.</IMPROVED\> tags\. Do not include any other text or comments\.

##### Annotation:

A version of the current theorem with the goal states annotated has also been provided for reference \(wrapped in <ANNOTATED\>\.\.\.</ANNOTATED\>\)\. Namely, the goal states have been interleaved between tactics as comments to help you better understand the proof and ensure the correctness of your response\. Do not include such state comments in your final response\.

##### Context:

The proof context, with relevant definitions and theorems, has additionally been provided to help you better understand the proof and ensure the correctness of your response\. It is wrapped in <CONTEXT\>\.\.\.</CONTEXT\>, with each item wrapped in <ITEM\>\.\.\.</ITEM\>\.

##### Examples:

Here are some examples of such optimization, as wrapped in <EXAMPLES\>\.\.\.</EXAMPLES\>\. Note that these examples are for illustrative purposes only and should not be copied directly\. Instead, use them to understand the kind of optimization expected and apply similar techniques to the current theorem, using these positive examples as an intuition and guidance on what kinds of optimizations you may do on your current target theorems\. Additionally, you will also be provided with a negative example which will be marked as such\. Use it to understand common pitfalls and avoid them in your response\. Use both the positive and negative examples to guide your optimization of the current theorem\.

### E\.4Autoinformalization

During the generation round at iterationt=0t=0, we create informal statements of each theorem for use in neurosymbolic augmentation\. This is carried out by prompting the base modelG0G\_\{0\}with the following:

You are an expert informalizer of formal mathematics to natural language\. Namely, given a formal theorem and proof in Lean4, you will generate an informalized statement of this same theorem in natural language, as well as \(2\) an informalized, natural language version of the same formal proof that is aligned with the informal statement\. Namely, when informalizing the proof, you should convert each tactic of the formal proof into a natural language step in the informal proof, and thereby, your informal proof should be written as a sequence of steps\. Consider the following example:

\(examples omitted\)

Now, with these examples in mind, it is now your turn to informalize the following formal statement and proof, which is wrapped in <FORMAL\>\.\.\.</FORMAL\> tags\.

You may think and reason as much as you want, but ensure that your final answer for \(1\): the informal statement is wrapped in <STATEMENT\>\.\.\.</STATEMENT\> tags, and \(2\): the informal proof is wrapped in <PROOF\>\.\.\.</PROOF\> tags\. Your final answer should have both a <STATEMENT\>\.\.\.</STATEMENT\> tag and a <PROOF\>\.\.\.</PROOF\> tag, and if there is no formal proof provided in the input, you may simply output <PROOF\></PROOF\> for the proof after informalizing the statement \(i\.e\. if you are given a theorem without a proof, or a definition/class/etc\.\)\. Input: <FORMAL\>

\(formal statement of proof is placed here\)

</FORMAL\>

The final informal statements are then parsed out for use in neurosymbolic augmentation\.

## Appendix FAdditional Experiments and Analyses

### F\.1Ablation Study

In addition to experiments presented in[5\.2](https://arxiv.org/html/2605.22885#S5.SS2), we study the effect of each source of neurosymbolic augmentation on model performance, finding that each added channel increases length\-metric performance \(Figure[8](https://arxiv.org/html/2605.22885#A6.F8)\)\. Additionally, we perform hyperparameter searches at each iteration for both the length \(Figure[9](https://arxiv.org/html/2605.22885#A6.F9)\) and dependency metric \(Figure[10](https://arxiv.org/html/2605.22885#A6.F10)\)\.

#### F\.1\.1Neurosymbolic Ablations

![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_neuro_ablation.png)Figure 8:Effect of neurosymbolic augmentation on base model performance \(DeepSeek\-R1\-Distill\-Qwen\-7B\) on the length metric, vs\. number of samples generated\. Each source of augmentation shows noticeable improvement in average score on somennvalues\.Figure[8](https://arxiv.org/html/2605.22885#A6.F8)shows that the unaugmented base model is consistently the weakest generator across sample budgets\. Adding chain\-of\-states information alone produces a substantial improvement, indicating that exposing intermediate Lean goals gives the model useful local structure for proof rewriting\. Adding informalized statements and proofs marginally improves performance across much of the curve, and the full scaffold, which additionally includes retrieved context, reaches the best performance at larger values ofnn\. However, we observe that the majority of this improvement comes from the initial chain\-of\-states annotation\. The gap is especially clear at best@8, where the full scaffold roughly doubles the improvement of the unaugmented base model\. These results support the claim that neurosymbolic augmentation is not merely a prompting detail, but a central part of making proof optimization learnable and sample\-efficient for small models\.

#### F\.1\.2Grid Search Results

![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_iter_1_gridsearch_all.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_iter_2_gridsearch_all.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Length/length_iter_3_gridsearch_all.png)

Figure 9:Hyperparameter grid searches for thelengthmetric across iterations 1–3\.![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/dependency_iter_1_gridsearch_all.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/dependency_iter_2_gridsearch_all.png)
![Refer to caption](https://arxiv.org/html/2605.22885v1/figures/Dependency/dependency_iter_3_gridsearch_all.png)

Figure 10:Hyperparameter grid searches for thedependencymetric across iterations 1–3\.Figures[9](https://arxiv.org/html/2605.22885#A6.F9)and[10](https://arxiv.org/html/2605.22885#A6.F10)show that the training pipeline is sensitive to optimization hyperparameters, but that several qualitative patterns are stable\. Increasing the sample budget generally improves scores for nearly all settings, so the relative comparisons are not artifacts of a single best@nnchoice\. For length optimization, lower preference gaps and moderate replay settings tend to perform well, suggesting that proof\-shortening benefits from keeping a broad set of successful rewrites in the training signal\. For dependency optimization, larger filtering gaps and more selective thresholds are often stronger, consistent with the metric rewarding more targeted structural changes\. Learning\-rate and winner/loser\-ratio effects vary across iterations, which is why we tune these settings separately for each metric and training round rather than reusing a single global configuration\.

### F\.2Qualitative Examples

Figures[11](https://arxiv.org/html/2605.22885#A6.F11)–[19](https://arxiv.org/html/2605.22885#A6.F19)show representative examples from the held\-out evaluation set\. For each example, we report the source module and declaration together with the original and optimized metric values\. The AlphaProof qualitative case studies use best@64 sampling rather than the best@16 budget used for the main MiniCTX\-v2 evaluations\. The original AlphaProof IMO 2024 release targets Lean v4\.10\.0; for these examples, we manually bumped the AlphaProof proofs to Lean v4\.17\.0\. The bumped version is available at \[Redacted\], and the original release is available at[https://storage\.googleapis\.com/deepmind\-media/DeepMind\.com/Blog/imo\-2024\-solutions/index\.html](https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html)\.

#### F\.2\.1Dependency Optimization

Original \(human\-written\)

theoremisCoatom\_iff\[OrderTopA\]\{K:A\}:

IsCoatomK↔K≠T∧∀Hg,K≤H→\\rightarrowg∉K→\\rightarrowg∈H→\\rightarrowH=T:=by

simp\_rw\[IsCoatom,lt\_iff\_le\_not\_le,SetLike\.not\_le\_iff\_exists,

and\_comm\(a:=\_≤\_\),and\_imp,exists\_imp,←and\_imp,and\_comm\]

ImProver 2 \(dependency\-optimized\)

theoremisCoatom\_iff\[OrderTopA\]\{K:A\}:

IsCoatomK↔K≠T∧∀Hg,K≤H→\\rightarrowg∉K→\\rightarrowg∈H→\\rightarrowH=T:=by

constructor<;\>introh

<;\>simp\_all\[IsCoatom,lt\_iff\_le\_not\_le,SetLike\.not\_le\_iff\_exists\]

<;\>tauto

Figure 11:ImProver 2 optimizes a proof for dependencies, reducing explicit dependencies by 3\.Figure[11](https://arxiv.org/html/2605.22885#A6.F11)comes fromMathlib\.Order\.Atoms, declarationSetLike\.isCoatom\_iff\. The original proof has explicit dependency count55, while the optimized proof has count22\. The rewrite replaces a longsimp\_rwchain naming several transformations with a case split, broader simplification, and propositional reasoning viatauto; this reduces the explicit dependency footprint while preserving the same theorem statement\.

Original \(human\-written\)

theoremmem\_cross\_iff\(xy:TSetγ\):

∀a,a∈’crosshβhγhδxy↔∃bc,a=⟨b,c⟩’∧b∈’x∧c∈’y:=by

introa

rw\[cross,mem\_inter\_iff,vCross\_spec\]

constructor

⋅\\cdotrintro⟨h1,b,c,rfl,h2⟩

simponly\[op\_mem\_converse\_iff,vCross\_spec,op\_inj\]ath1

obtain⟨b’,c’,⟨rfl,rfl⟩,h1⟩:=h1

exact⟨b,c,rfl,h1,h2⟩

⋅\\cdotrintro⟨b,c,rfl,h1,h2⟩

simponly\[op\_mem\_converse\_iff,vCross\_spec,op\_inj\]

exact⟨⟨c,b,⟨rfl,rfl⟩,h1⟩,⟨b,c,⟨rfl,rfl⟩,h2⟩⟩

ImProver 2 \(dependency\-optimized\)

theoremmem\_cross\_iff\(xy:TSetγ\):

∀a,a∈’crosshβhγhδxy↔∃bc,a=⟨b,c⟩’∧b∈’x∧c∈’y:=by

introa

\-\-Usethedefinitionofcrossandsimplifythemembershipconditionsdirectly

constructor<;\>introh

\-\-Firstdirection:Assumemembershipincross,constructthepair

<;\>simp\[cross\]ath⊢

\-\-Seconddirection:Decomposethepairexistenceclaimandverifyconditions

<;\>aesop

\-\-Handleremainingsimplecaseswithbasicreasoning

Figure 12:ImProver 2 optimizes a proof for dependencies, reducing explicit dependencies by 2\.Figure[12](https://arxiv.org/html/2605.22885#A6.F12)comes fromConNF\.External\.Basic, declarationConNF\.mem\_cross\_iff\. The dependency count decreases from22to0\. The optimized proof avoids explicitly naming the original rewrite lemmas and instead unfoldscrossand delegates the remaining elementary cases to automation\. This illustrates a common dependency\-optimization behavior: replacing brittle named rewrite sequences with more local simplification and search\.

Original \(AlphaProof\)

theoremimo\_2024\_p6

\(IsAquaesulian:\(ℚ\\mathbb\{Q\}→\\toℚ\\mathbb\{Q\}\)→\\toProp\)

\(IsAquaesulian\_def:∀\\forallf,IsAquaesulianf↔\\leftrightarrow

∀\\forallxy,f\(x\+fy\)=fx\+y∨\\veef\(fx\+y\)=x\+fy\):

IsLeast\{\(c:ℤ\\mathbb\{Z\}\)\|∀\\forallf,IsAquaesulianf→\\to\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.Finite∧\\wedge

\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.ncard≤\\leqc\}2:=by

exists@?\_

⋅\\cdot

useλ\\lambdaub=\>ifj:u0=0thenby\_contraλ\\lambdac=\>?\_else?\_

⋅\\cdot

suffices:\(\{J\|∃\\existsk,uk\+u\(\-k\)=J\}\)⊆\\subseteq\{0\}

⋅\\cdotsimp\_all\[this\.antisymm\]

rintro\-⟨\\langlea,rfl⟩\\rangle

contrapose\!c

simp\_all

suffices:\{U\|∃\\existsexamples6:ℚ\\mathbb\{Q\},uexamples6\+u\(\-examples6\)=U\}⊆\\subseteq\{0,\(u\(a:Rat\)\+\(u<\|@@↑\\uparrow\(\(\(\-a\)\)\)\)\)\}\.\.

⋅\\cdotconstructor

⋅\\cdotexact\(Set\.toFinite\(\_\)\)\.subset\(bysimpausingthis\)

⋅\\cdotexact\(Set\.ncard\_le\_ncard\(bysimpausingthis\)\)\.trans\(Set\.ncard\_pair\(Ne\.symm\(↑\\uparrow\(\(c\)\)\)\)\)\.le

rintro\-⟨\\langlehz,rfl⟩\\rangle

inductionb@hza

⋅\\cdot

have:=b\(\-a\)$hz\+ua

have:=bhzhz

simp\_all\[add\_comm\]

have:=b\(\-hz\)\(hz\+u↑\\uparrow\(hz\)\)

simp\_all\[add\_assoc,C\]

inductionthis

⋅\\cdot

simp\_all

have:=bhz\(hz\+\(ua\+u\(\-a\)\)\)

have:=b\(hz\+\(ua\+u\(\-a\)\)\)$hz\+\(ua\+u\(\-a\)\)

use\.inr$by\_contra$byhint

have:=bhz$hz\+\(uhz\+u\(\-hz\)\)

casesb\(hz\+\(uhz\+u\(\-hz\)\)\)$hz\+\(uhz\+u\(\-hz\)\)with\|\_=\>hint

have:=b\(\-hz\)\(uhz\+a\)

have:=b$\-a

specializethis\(uhz\+a\)

simp\_all\[←\\leftarrowadd\_assoc\]

have:=b0

have:=b

specializebaa

simp\_all\[add\_comm\]

have:=\(this<\|\-a\)\(↑\\uparrowa\+\(\(\(ua\)\)\):\(↑\\uparrow\_:\(\(\(\_\)\)\)\)\)\.\.

simp\_all\[add\_assoc\]

casesthis

⋅\\cdot

simp\_all

contrapose\!IsAquaesulian\_def

simp\_all

exfalso

have:=thisa\(a\+\(uhz\+u\(\-hz\)\)\)

simp\_all\[Ne\.symm,Bool\]

have:=⟨\\langle∀\\forallcongr\_argG,\_⟩\\rangle\(a\+\(uhz\+u\(\-hz\)\)\)$a\+\(u↑\\uparrowhz\+u↑\\uparrow\(\-hz\)\)

simp\_all

have:=thisa\(a\+\(ua\+u\(\-a\)\)\)

cases⟨\\langleforallJdS,\_⟩\\rangle\(a\+\(ua\+u\(\-a\)\)\)\(a\+\(ua\+u↑\\uparrow\(\-a\)\)\)with\|\_=\>hint

simp\_all

casesb00with\|\_=\>exactabsurd\(b0$\(0\+\(1\*\(@\(u↑\\uparrow\.\(\(0\)\)\)\)\)\)^01:↑\\uparrow\(\(\_\)\)\)\(id$\(by\(cases\(b\(u0\)\(\(u0\)\)\)with\|\_=\>continuity\)\)\)

rintroKV

specializeV$λ\\lambdaN=\>\-N\+2\*Int\.ceilN

specialize\(V$\(IsAquaesulian\_def\_\)\.mpr\_\)

⋅\\cdotsimp\_rw\[←\\leftarroweq\_sub\_iff\_add\_eq’\]

ring\_nf

usemod\_cast@?\_

norm\_num\[<\-add\_mul,Int\.ceil\_eq\_iff\]

useλ\\lambdacK=\>\(em\_\)\.imp\(⟨\\langlebylinarith\[Int\.ceil\_lt\_add\_onec,Int\.le\_ceilK\],\.⟩\\rangle\)\(byrepeatusebylinarith\[\.,Int\.le\_ceilc,or,Int\.ceil\_lt\_add\_one$K\]\)

simp\_all\[Int\.ceil\_neg,←\\leftarrowadd\_assoc\]

ImProver 2 \(dependencies\-optimized\)

theoremimo\_2024\_p6

\(IsAquaesulian:\(ℚ\\mathbb\{Q\}→\\toℚ\\mathbb\{Q\}\)→\\toProp\)

\(IsAquaesulian\_def:∀\\forallf,IsAquaesulianf↔\\leftrightarrow

∀\\forallxy,f\(x\+fy\)=fx\+y∨\\veef\(fx\+y\)=x\+fy\):

IsLeast\{\(c:ℤ\\mathbb\{Z\}\)\|∀\\forallf,IsAquaesulianf→\\to\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.Finite∧\\wedge

\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.ncard≤\\leqc\}2:=by

exists@?\_

⋅\\cdotuseλ\\lambdaub=\>ifj:u0=0thenby\_contraλ\\lambdac=\>?\_else?\_

⋅\\cdotsuffices:\(\{J\|∃\\existsk,uk\+u\(\-k\)=J\}\)⊆\\subseteq\{0\}

⋅\\cdotsimp\_all\[this\.antisymm\]

rintro\-⟨\\langlea,rfl⟩\\rangle

contrapose\!c

simp\_all

suffices:\{U\|∃\\existsexamples6:ℚ\\mathbb\{Q\},uexamples6\+u\(\-examples6\)=U\}⊆\\subseteq\{0,\(u\(a:Rat\)\+\(u<\|@@↑\\uparrow\(\(\(\-a\)\)\)\)\)\}\.\.

⋅\\cdotconstructor

⋅\\cdotexact\(Set\.toFinite\(\_\)\)\.subset\(bysimpausingthis\)

⋅\\cdotexact\(Set\.ncard\_le\_ncard\(bysimpausingthis\)\)\.trans\(Set\.ncard\_pair\(Ne\.symm\(↑\\uparrow\(\(c\)\)\)\)\)\.le

rintro\-⟨\\langlehz,rfl⟩\\rangle

inductionb@hza

⋅\\cdothave:=b\(\-a\)$hz\+ua

have:=bhzhz

simp\_all\[add\_comm\]

have:=b\(\-hz\)\(hz\+u↑\\uparrow\(hz\)\)

simp\_all\[add\_assoc,C\]

inductionthis

⋅\\cdotsimp\_all

have:=bhz\(hz\+\(ua\+u\(\-a\)\)\)

have:=b\(hz\+\(ua\+u\(\-a\)\)\)$hz\+\(ua\+u\(\-a\)\)

use\.inr$by\_contra$byhint

have:=bhz$hz\+\(uhz\+u\(\-hz\)\)

casesb\(hz\+\(uhz\+u\(\-hz\)\)\)$hz\+\(uhz\+u\(\-hz\)\)with\|\_=\>hint

have:=b\(\-hz\)\(uhz\+a\)

have:=b$\-a

specializethis\(uhz\+a\)

simp\_all\[←\\leftarrowadd\_assoc\]

have:=b0

have:=b

specializebaa

simp\_all\[add\_comm\]

have:=\(this<\|\-a\)\(↑\\uparrowa\+\(\(\(ua\)\)\):\(↑\\uparrow\_:\(\(\(\_\)\)\)\)\)\.\.

simp\_all\[add\_assoc\]

casesthis

⋅\\cdotsimp\_all

contrapose\!IsAquaesulian\_def

simp\_all

exfalso

have:=thisa\(a\+\(uhz\+u\(\-hz\)\)\)

simp\_all\[Ne\.symm,Bool\]

have:=⟨\\langle∀\\forallcongr\_argG,\_⟩\\rangle\(a\+\(uhz\+u\(\-hz\)\)\)$a\+\(u↑\\uparrowhz\+u↑\\uparrow\(\-hz\)\)

simp\_all

have:=thisa\(a\+\(ua\+u\(\-a\)\)\)

cases⟨\\langleforallJdS,\_⟩\\rangle\(a\+\(ua\+u\(\-a\)\)\)\(a\+\(ua\+u↑\\uparrow\(\-a\)\)\)with\|\_=\>hint

simp\_all

casesb00with\|\_=\>exactabsurd\(b0$\(0\+\(1\*\(@\(u↑\\uparrow\.\(\(0\)\)\)\)\)\)^01:↑\\uparrow\(\(\_\)\)\)\(id$\(by\(cases\(b\(u0\)\(\(u0\)\)\)with\|\_=\>continuity\)\)\)

rintroKV

specializeV$λ\\lambdaN=\>\-N\+2\*Int\.ceilN

specialize\(V$\(IsAquaesulian\_def\_\)\.mpr\_\)

⋅\\cdotsimp\_rw\[←\\leftarroweq\_sub\_iff\_add\_eq’\]

ring\_nf

usemod\_cast@?\_

norm\_num\[<\-add\_mul,Int\.ceil\_eq\_iff\]

useλ\\lambdacK=\>\(em\_\)\.imp\(⟨\\langlebylinarith\[Int\.ceil\_lt\_add\_onec,Int\.le\_ceilK\],\.⟩\\rangle\)\(byrepeatusebylinarith\[\.,Int\.le\_ceilc,or,Int\.ceil\_lt\_add\_one$K\]\)

letS:Setℚ\\mathbb\{Q\}:=\{x\|∃\\existsr:ℚ\\mathbb\{Q\},\(\-r\+2\*↑\\uparrow⌈\\lceilr⌉\\rceil\)\+\(\-\(\-r\)\+2\*↑\\uparrow⌈\\lceil\-r⌉\\rceil\)=x\}

havehsub:\(\{\(0:ℚ\\mathbb\{Q\}\),2\}:Setℚ\\mathbb\{Q\}\)⊆\\subseteqS:=by

introxhx

simpathx

rcaseshxwithrfl\|rfl

⋅\\cdotexact⟨\\langle\(\-1:ℚ\\mathbb\{Q\}\),bynorm\_num⟩\\rangle

Original \(continued\)

suffices:2<=V\.1\.toFinset\.card

⋅\\cdotletM:=V\.1\.toFinset

haveh2nat:2≤\\leq\(\{x\|∃\\existsr:ℚ\\mathbb\{Q\},2\*↑\\uparrow⌈\\lceilr⌉\\rceil\+\-\(2\*↑\\uparrow⌊\\lfloorr⌋\\rfloor\)=x\}:Setℚ\\mathbb\{Q\}\)\.ncard:=by

rwa\[Set\.ncard\_eq\_toFinset\_card\_V\.1\]

haveh2int:\(2:ℤ\\mathbb\{Z\}\)≤\\leq\(\{x\|∃\\existsr:ℚ\\mathbb\{Q\},2\*↑\\uparrow⌈\\lceilr⌉\\rceil\+\-\(2\*↑\\uparrow⌊\\lfloorr⌋\\rfloor\)=x\}:Setℚ\\mathbb\{Q\}\)\.ncard:=by

exact\_mod\_casth2nat

exacth2int\.transV\.2

useFinset\.one\_lt\_card\.2$by

refine⟨\\langle0,V\.1\.mem\_toFinset\.2?\_,2,V\.1\.mem\_toFinset\.2?\_,bynorm\_num⟩\\rangle

⋅\\cdotexact⟨\\langle\-1,bynorm\_num⟩\\rangle

⋅\\cdotexact⟨\\langle\(1/2:ℚ\\mathbb\{Q\}\),bynorm\_num⟩\\rangle

ImProver 2 \(dependencies\-optimized; continued\)

⋅\\cdotexact⟨\\langle\(1/2:ℚ\\mathbb\{Q\}\),bynorm\_num⟩\\rangle

haveh2nat:2≤\\leqS\.ncard:=by

havehp:\(\{\(0:ℚ\\mathbb\{Q\}\),2\}:Setℚ\\mathbb\{Q\}\)\.ncard=2:=by

simpausing\(Set\.ncard\_pair\(bynorm\_num:\(0:ℚ\\mathbb\{Q\}\)≠\\neq2\)\)

calc

2=\(\{\(0:ℚ\\mathbb\{Q\}\),2\}:Setℚ\\mathbb\{Q\}\)\.ncard:=hp\.symm

\_≤\\leqS\.ncard:=Set\.ncard\_le\_ncardhsubV\.1

haveh2int:\(2:ℤ\\mathbb\{Z\}\)≤\\leqS\.ncard:=by

exact\_mod\_casth2nat

exacth2int\.transV\.2

Figure 13:ImProver 2 optimizes an AlphaProof proof for dependencies, reducing explicit dependencies by 3\.Figure[13](https://arxiv.org/html/2605.22885#A6.F13)comes fromAlphaProof\.P6, declarationimo\_2024\_p6\. The score changes from1818to1515\. The optimized proof keeps the same global proof search structure but removes a few explicit named dependencies by relying more on local facts and consolidated arithmetic/set\-cardinality reasoning\. However, overall, this case demonstrates negligible impact by ImProver2 on such a large\-scale, complex problem\.

#### F\.2\.2Length Optimization

Original \(human\-written\)

lemmasummerCommute\_jacobi\_ofCrAnListF\(φ\\varphis1φ\\varphis2φ\\varphis3:List𝓕\\bm\{\\mathcal\{F\}\}\.CrAnFieldOp\):

\[ofCrAnListFφ\\varphis1,\[ofCrAnListFφ\\varphis2,ofCrAnListFφ\\varphis3\]sca\]sca=

𝓢\\bm\{\\mathcal\{S\}\}\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis1,𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis3\)∙\\bullet

\(\-𝓢\\bm\{\\mathcal\{S\}\}\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis2,𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis3\)∙\\bullet\[ofCrAnListFφ\\varphis3,\[ofCrAnListFφ\\varphis1,ofCrAnListFφ\\varphis2\]sca\]sca\-

𝓢\\bm\{\\mathcal\{S\}\}\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis1,𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis2\)∙\\bullet\[ofCrAnListFφ\\varphis2,\[ofCrAnListFφ\\varphis3,ofCrAnListFφ\\varphis1\]sca\]sca\):=by

repeatrw\[superCommuteF\_ofCrAnListF\_ofCrAnListF\]

simponly\[instCommGroup,map\_sub,map\_smul,neg\_smul\]

repeatrw\[superCommuteF\_ofCrAnListF\_ofCrAnListF\]

simponly\[instCommGroup\.eq\_1,ofList\_append\_eq\_mul,List\.append\_assoc\]

by\_casesh1:\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis1\)=bosonic<;\>

by\_casesh2:\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis2\)=bosonic<;\>

by\_casesh3:\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis3\)=bosonic

⋅\\cdotsimponly\[h1,h2,h3,mul\_self,bosonic\_exchangeSign,one\_smul,exchangeSign\_bosonic,neg\_sub\]

abel

⋅\\cdotsimponly\[h1,h2,bosonic\_exchangeSign,one\_smul,mul\_bosonic,mul\_self,map\_one,

exchangeSign\_bosonic,neg\_sub\]

abel

⋅\\cdotsimponly\[h1,h3,mul\_bosonic,bosonic\_exchangeSign,one\_smul,exchangeSign\_bosonic,neg\_sub,

mul\_self,map\_one\]

abel

⋅\\cdotsimponly\[neq\_bosonic\_iff\_eq\_fermionic\]ath1h2h3

simponly\[h1,h2,h3,mul\_self,bosonic\_exchangeSign,one\_smul,

fermionic\_exchangeSign\_fermionic,neg\_smul,neg\_sub,bosonic\_mul\_fermionic,sub\_neg\_eq\_add,

mul\_bosonic,smul\_add,exchangeSign\_bosonic\]

abel

⋅\\cdotsimponly\[neq\_bosonic\_iff\_eq\_fermionic\]ath1h2h3

simponly\[h1,h2,h3,mul\_self,map\_one,one\_smul,exchangeSign\_bosonic,mul\_bosonic,

bosonic\_exchangeSign,bosonic\_mul\_fermionic,neg\_sub\]

abel

⋅\\cdotsimponly\[neq\_bosonic\_iff\_eq\_fermionic\]ath1h2h3

simponly\[h1,h2,h3,bosonic\_mul\_fermionic,fermionic\_exchangeSign\_fermionic,neg\_smul,

one\_smul,sub\_neg\_eq\_add,bosonic\_exchangeSign,mul\_bosonic,smul\_add,exchangeSign\_bosonic,

neg\_sub,mul\_self\]

abel

⋅\\cdotsimponly\[neq\_bosonic\_iff\_eq\_fermionic\]ath1h2h3

simponly\[h1,h2,h3,mul\_bosonic,fermionic\_exchangeSign\_fermionic,neg\_smul,one\_smul,

sub\_neg\_eq\_add,exchangeSign\_bosonic,bosonic\_mul\_fermionic,smul\_add,mul\_self,

bosonic\_exchangeSign,neg\_sub\]

abel

⋅\\cdotsimponly\[neq\_bosonic\_iff\_eq\_fermionic\]ath1h2h3

simponly\[h1,h2,h3,mul\_self,map\_one,one\_smul,fermionic\_exchangeSign\_fermionic,neg\_smul,

neg\_sub\]

abel

ImProver 2 \(length\-optimized\)

lemmasummerCommute\_jacobi\_ofCrAnListF\(φ\\varphis1φ\\varphis2φ\\varphis3:List𝓕\\bm\{\\mathcal\{F\}\}\.CrAnFieldOp\):

\[ofCrAnListFφ\\varphis1,\[ofCrAnListFφ\\varphis2,ofCrAnListFφ\\varphis3\]sca\]sca=

𝓢\\bm\{\\mathcal\{S\}\}\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis1,𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis3\)∙\\bullet

\(\-𝓢\\bm\{\\mathcal\{S\}\}\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis2,𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis3\)∙\\bullet\[ofCrAnListFφ\\varphis3,\[ofCrAnListFφ\\varphis1,ofCrAnListFφ\\varphis2\]sca\]sca\-

𝓢\\bm\{\\mathcal\{S\}\}\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis1,𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis2\)∙\\bullet\[ofCrAnListFφ\\varphis2,\[ofCrAnListFφ\\varphis3,ofCrAnListFφ\\varphis1\]sca\]sca\):=by

simp\_all\[superCommuteF\_ofCrAnListF\_ofCrAnListF,

instCommGroup,map\_sub,map\_smul,neg\_smul,

superCommuteF\_ofCrAnListF\_ofCrAnListF,

instCommGroup\.eq\_1,ofList\_append\_eq\_mul,List\.append\_assoc,

neq\_bosonic\_iff\_eq\_fermionic\]

<;\>by\_casesh1:\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis1\)=bosonic<;\>

by\_casesh2:\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis2\)=bosonic<;\>

by\_casesh3:\(𝓕\\bm\{\\mathcal\{F\}\}\|\>sφ\\varphis3\)=bosonic

<;\>simp\_all\[h1,h2,h3,mul\_self,bosonic\_exchangeSign,

one\_smul,exchangeSign\_bosonic,neg\_sub,

fermionic\_exchangeSign\_fermionic,neg\_smul,

bosonic\_mul\_fermionic,sub\_neg\_eq\_add,

mul\_bosonic,smul\_add,exchangeSign\_bosonic,

neg\_sub,mul\_self\]<;\>abel

Figure 14:ImProver 2 optimizes a proof for length, reducing tactic count by 19\.Figure[14](https://arxiv.org/html/2605.22885#A6.F14)comes fromHepLean\.PerturbationTheory\.FieldOpFreeAlgebra\.SuperCommute, declarationsummerCommute\_jacobi\_ofCrAnListF\. The tactic count decreases from4343to2424\. The optimized proof collapses repeated rewriting and many case\-specific simplification branches into a single largersimp\_allcall followed by the same case split structure andabel\. This preserves the human proof’s algebraic strategy while eliminating repeated local boilerplate\.

Original \(human\-written\)

theoremmem\_cross\_iff\(xy:TSetγ\):

∀\\foralla,a∈’crosshβhγhδxy↔\\leftrightarrow∃\\existsbc,a=⟨\\langleb,c⟩\\rangle’∧\\wedgeb∈’x∧\\wedgec∈’y:=by

introa

rw\[cross,mem\_inter\_iff,vCross\_spec\]

constructor

⋅\\cdotrintro⟨\\langleh1,b,c,rfl,h2⟩\\rangle

simponly\[op\_mem\_converse\_iff,vCross\_spec,op\_inj\]ath1

obtain⟨\\langleb’,c’,⟨\\langlerfl,rfl⟩\\rangle,h1⟩\\rangle:=h1

exact⟨\\langleb,c,rfl,h1,h2⟩\\rangle

⋅\\cdotrintro⟨\\langleb,c,rfl,h1,h2⟩\\rangle

simponly\[op\_mem\_converse\_iff,vCross\_spec,op\_inj\]

exact⟨\\langle⟨\\langlec,b,⟨\\langlerfl,rfl⟩\\rangle,h1⟩\\rangle,⟨\\langleb,c,⟨\\langlerfl,rfl⟩\\rangle,h2⟩\\rangle⟩\\rangle

ImProver 2 \(length\-optimized\)

theoremmem\_cross\_iff\(xy:TSetγ\):

∀\\foralla,a∈’crosshβhγhδxy↔\\leftrightarrow∃\\existsbc,a=⟨\\langleb,c⟩\\rangle’∧\\wedgeb∈’x∧\\wedgec∈’y:=by

simp\_all\[cross,mem\_inter\_iff,vCross\_spec,

op\_mem\_converse\_iff,op\_inj\]

<;\>aesop

Figure 15:ImProver 2 optimizes a proof for length, reducing tactic count by 8\.Figure[15](https://arxiv.org/html/2605.22885#A6.F15)is another optimization ofConNF\.External\.Basic, declarationConNF\.mem\_cross\_iff, this time under the length metric\. The tactic count decreases from1010to22\. The optimized proof replaces the explicit bidirectional constructor proof with a compact simplification over the relevant definitions followed byaesop; this is the characteristic length\-optimization pattern of compressing routine structural reasoning into a small number of automation\-heavy tactics\.

Original \(AlphaProof\)

theoremimo\_2024\_p2:\{\(a,b\)\|0<a∧\\wedge0<b∧\\wedge∃\\existsgN,0<g∧\\wedge0<N∧\\wedge∀\\foralln≥\\geqN,Nat\.gcd\(a^n\+b\)\(b^n\+a\)=g\}=\{\(1,1\)\}:=by

induction\(10\)\+2

⋅\\cdotuseSet\.eq\_singleton\_iff\_unique\_mem\.2⟨\\langle?\_,λ\\lambdabg=\>by\_contra$g\.2\.2\.recλ\\lambdaYSi=\>S\.recλ\\lambdaLD=\>?\_⟩\\rangle

⋅\\cdot

exact⟨\\langlebyleft,byleft,2,3,bysimp\_all⟩\\rangle

have:b\.1\+b\.2∣\\midY:=?\_

⋅\\cdotsuffices:b\.1=b\.2

⋅\\cdotnorm\_num\[b\.ext\_iff,<\-D\.2\.2L,this\]at\*

use\(Nat\.pow\_lt\_pow\_right\(g\.1\.nat\_succ\_le\.lt\_of\_ne’i\)L\.lt\_succ\_self\)\.ne’\(D\.2\.2\_L\.le\_succ\)

suffices:b\.1\+b\.2∣\\midb\.fst^\(2\*L\)\+b\.2∧\\wedge\(b\)\.fst\+\(b\)\.snd∣\\midb\.snd^\(2\*L\)\+b\.1

⋅\\cdotsuffices:b\.1^2%\(b\.1\+b\.2\)=b\.2^2%\(b\.1\+b\.snd\)

⋅\\cdotnorm\_num\[Nat\.add\_mod,pow\_mul,this,Nat\.dvd\_iff\_mod\_eq\_zero,Nat\.pow\_mod\]at\*

norm\_num\[add\_comm,b\.ext\_iff,sq\_,←\\leftarrowNat\.pow\_mod,←\\leftarrowNat\.dvd\_iff\_mod\_eq\_zero\]at\*

zifyat\*

casesthis\.1\.subthis\.2with\|\_Z=\>nlinarith\[\(by\(nlinarith\):Z=0\)\]

apply@Nat\.modEq\_of\_dvd

use\(b\.snd\)\-b\.fst,\(by⋅\\cdotring:\(\(b\.snd\):ℤ\\mathbb\{Z\}\)^2\-b\.fst^2=\(b\.fst\+\(b\)\.2\)\*\_\)

norm\_num\[\(2\)\.le\_mul\_of\_pos\_left,Nat\.gcd\_dvd,←\\leftarrowD\.2\.2\(2\*L\),this\.trans,\(D\.right\.1:\_\)\]

suffices:b\.1\+b\.2∣\\midb\.1^\(2\*L\)\+b\.2∧\\wedgeb\.1\+b\.2∣\\midb\.snd^\(2\*L\)\+b\.1

⋅\\cdotexactD\.2\.2\(2\*\(L\)\)\(le\_mul\_of\_one\_le\_left’\(bydecide\)\)⊳\\trianglerightdvd\_gcd\(this\.left\)\(this\)\.2

exfalso

suffices:b\.1\*b\.2\+1∣\\midY

⋅\\cdotsuffices:b\.1^φ\\varphi\(b\.1\*b\.2\+1\)%\(b\.1\*b\.2\+1\)=1%\(b\.1\*b\.2\+1\)∧\\wedgeb\.2^φ\\varphi\(b\.1\*b\.snd\+1\)%\(\(b\)\.1\*↑\\uparrow\(b\.snd\)\+1\)=1%\(b\.1\*b\.snd\+1\)

⋅\\cdot

absurdD\.2\.2\(φ\\varphi\(b\.1\*b\.2\+1\)\*L\)\(bynlinarith\[\(\(b\.fst\*b\.2\+1\)\.totient\_pos\)\.2↑\\uparrowFin\.size\_pos’\]\)

applymt\(\.⊳\\trianglerightNat\.gcd\_dvd\_\_\)

useλ\\lambdaH=\>absurd\(⟨\\langle\_∣\\midY⟩\\rangle\.transH\.1\)\(λ\\lambdav=\>absurd\(⟨\\langle\_∣\\midY⟩\\rangle\.transH\.2\)?\_\)

norm\_num\[pow\_mul,b\.ext\_iff,\(1\)\.mod\_eq\_of\_lt,g\.symm,this,Nat\.add\_mod,Nat\.dvd\_iff\_mod\_eq\_zero,Nat\.pow\_mod\]at\(i\)v⊢\\vdash

norm\_num\[add\_comm,pow\_mul,<\-Nat\.dvd\_iff\_mod\_eq\_zero\]at\*

contrapose\!i

zifyat\*

repeatusebynlinarith\[Int\.le\_of\_dvd\(bylinarith\)v,Int\.le\_of\_dvd\(bylinarith\)i\]

repeatuse↑\\uparrow\(Nat\.ModEq\.pow\_totient\(bynorm\_num\)\)

by\_contra\!H

suffices:b\.1^φ\\varphi\(b\.1\*b\.2\+1\)%\(b\.1\*b\.2\+1\)=1%\(b\.1\*b\.2\+1\)∧\\wedgeb\.2^φ\\varphi\(b\.1\*b\.2\+1\)%\(b\.1\*b\.2\+1\)=1%\(b\.fst\*↑\\uparrow\(b\.snd\)\+1\)

⋅\\cdotsimp\_all

suffices:b\.1\*b\.2\+1∣\\midb\.1^\(φ\\varphi\(b\.1\*b\.2\+1\)\*\(L\+1\)\-1\)\+b\.2∧\\wedgeb\.1\*b\.2\+1∣\\midb\.2^\(φ\\varphi\(b\.1\*b\.2\+1\)\*\(L\+1\)\-1\)\+\(b\.fst\)

⋅\\cdotuseH$D\.2\.2\(φ\\varphi\_\*\(L\+1\)\-1\)\(L\.le\_sub\_of\_add\_le\(bynlinarith\[\(\(b\.1\*b\.2\+1\)\.totient\_pos\)\.2Nat\.succ\_pos’\]\)\)⊳\\triangleright\(\(\(Nat\.dvd\_gcd\)\(this\)\.1\)\)this\.right

casesB:Nat\.exists\_eq\_add\_of\_lt$\(\(b\.1\*b\.2\+1\)\.totient\_pos\)\.2\(bycontinuity\)

norm\_num\[\*,g,⟨\\langleφ\\varphi\_=\_⟩\\rangle,mul\_add,Nat\.pow\_mod,\(1\)\.mod\_eq\_of\_lt,pow\_add,Nat\.add\_mod,pow\_mul,Nat\.dvd\_iff\_mod\_eq\_zero,Nat\.mul\_mod\]atthis⊢\\vdash

simp\_all

suffices:b\.1\*b\.2\+1∣\\midb\.1\*\(\(b\.1%\(\(b\)\.1\*\(b\.snd\)\+1\):\_\)^⟨\\langleNat⟩\\rangle\+b\.snd\)∧\\wedge\(b\.fst\*↑\\uparrow\(b\.snd\)\+1\)∣\\mid\(b\)\.snd\*\(\(b\.snd%\(\(b\)\.fst\*b\.snd\+1\)\)^⟨\\langleNat⟩\\rangle\+b\.fst\)

⋅\\cdotnorm\_num\[<\-Nat\.dvd\_iff\_mod\_eq\_zero,g,\(1\)\.mod\_eq\_of\_lt,Nat\.dvd\_mul\]atthis⊢\\vdash

exists@?\_

⋅\\cdotcasesthis\.1with\|\_Qr=\>simp\_all\[\(Q\.dvd\_gcdr\.1⟨\\langle\_,\.symmr\.right\.choose\_spec\.2⟩\\rangle\)\.antisymm\]

cases@this\.2with\|\_FX=\>simp\_all\[\(F\.dvd\_gcdX\.1⟨\\langle\_,symmX\.2\.choose\_spec\.2⟩\\rangle\)\.antisymm\]

simp\_all\[mul\_comm,mul\_add,add\_comm,Nat\.add\_mod,Nat\.dvd\_iff\_mod\_eq\_zero\]

repeatuse\(Nat\.ModEq\.pow\_totient\(by\.\.\.norm\_num\)\)

congr26

ImProver 2 \(length\-optimized\)

theoremimo\_2024\_p2:\{\(a,b\)\|0<a∧\\wedge0<b∧\\wedge∃\\existsgN,0<g∧\\wedge0<N∧\\wedge∀\\foralln≥\\geqN,Nat\.gcd\(a^n\+b\)\(b^n\+a\)=g\}=\{\(1,1\)\}:=by

refineSet\.eq\_singleton\_iff\_unique\_mem\.2⟨\\langle⟨\\langleNat\.zero\_lt\_one,Nat\.zero\_lt\_one,2,1,Nat\.succ\_pos1,Nat\.zero\_lt\_one,bysimp⟩\\rangle,λ\\lambdabg=\>by\_contra$g\.2\.2\.recλ\\lambdaYSi=\>S\.recλ\\lambdaLD=\>?\_⟩\\rangle

suffices:b\.1\*b\.2\+1∣\\midY

⋅\\cdotsuffices:b\.1^φ\\varphi\(b\.1\*b\.2\+1\)%\(b\.1\*b\.2\+1\)=1%\(b\.1\*b\.2\+1\)∧\\wedgeb\.2^φ\\varphi\(b\.1\*b\.snd\+1\)%\(\(b\)\.1\*↑\\uparrow\(b\.snd\)\+1\)=1%\(b\.1\*b\.snd\+1\)

⋅\\cdotabsurdD\.2\.2\(φ\\varphi\(b\.1\*b\.2\+1\)\*L\)\(bynlinarith\[\(\(b\.fst\*b\.2\+1\)\.totient\_pos\)\.2↑\\uparrowFin\.size\_pos’\]\)

applymt\(\.⊳\\trianglerightNat\.gcd\_dvd\_\_\)

useλ\\lambdaH=\>absurd\(⟨\\langle\_∣\\midY⟩\\rangle\.transH\.1\)\(λ\\lambdav=\>absurd\(⟨\\langle\_∣\\midY⟩\\rangle\.transH\.2\)?\_\)

norm\_num\[pow\_mul,b\.ext\_iff,\(1\)\.mod\_eq\_of\_lt,g\.symm,this,Nat\.add\_mod,Nat\.dvd\_iff\_mod\_eq\_zero,Nat\.pow\_mod\]at\(i\)v⊢\\vdash

norm\_num\[add\_comm,pow\_mul,<\-Nat\.dvd\_iff\_mod\_eq\_zero\]at\*

contrapose\!i

zifyat\*

repeatusebynlinarith\[Int\.le\_of\_dvd\(bylinarith\)v,Int\.le\_of\_dvd\(bylinarith\)i\]

repeatuse↑\\uparrow\(Nat\.ModEq\.pow\_totient\(bynorm\_num\)\)

by\_contra\!H

suffices:b\.1^φ\\varphi\(b\.1\*b\.2\+1\)%\(b\.1\*b\.2\+1\)=1%\(b\.1\*b\.2\+1\)∧\\wedgeb\.2^φ\\varphi\(b\.1\*b\.2\+1\)%\(b\.1\*b\.2\+1\)=1%\(b\.fst\*↑\\uparrow\(b\.snd\)\+1\)

⋅\\cdotsimp\_all

suffices:b\.1\*b\.2\+1∣\\midb\.1^\(φ\\varphi\(b\.1\*b\.2\+1\)\*\(L\+1\)\-1\)\+b\.2∧\\wedgeb\.1\*b\.2\+1∣\\midb\.2^\(φ\\varphi\(b\.1\*b\.2\+1\)\*\(L\+1\)\-1\)\+\(b\.fst\)

⋅\\cdotuseH$D\.2\.2\(φ\\varphi\_\*\(L\+1\)\-1\)\(L\.le\_sub\_of\_add\_le\(bynlinarith\[\(\(b\.1\*b\.2\+1\)\.totient\_pos\)\.2Nat\.succ\_pos’\]\)\)⊳\\triangleright\(\(\(Nat\.dvd\_gcd\)\(this\)\.1\)\)this\.right

casesB:Nat\.exists\_eq\_add\_of\_lt$\(\(b\.1\*b\.2\+1\)\.totient\_pos\)\.2\(bycontinuity\)

norm\_num\[\*,g,⟨\\langleφ\\varphi\_=\_⟩\\rangle,mul\_add,Nat\.pow\_mod,\(1\)\.mod\_eq\_of\_lt,pow\_add,Nat\.add\_mod,pow\_mul,Nat\.dvd\_iff\_mod\_eq\_zero,Nat\.mul\_mod\]atthis⊢\\vdash

simp\_all

suffices:b\.1\*b\.2\+1∣\\midb\.1\*\(\(b\.1%\(\(b\)\.1\*\(b\.snd\)\+1\):\_\)^⟨\\langleNat⟩\\rangle\+b\.snd\)∧\\wedge\(b\.fst\*↑\\uparrow\(b\.snd\)\+1\)∣\\mid\(b\)\.snd\*\(\(b\.snd%\(\(b\)\.fst\*b\.snd\+1\)\)^⟨\\langleNat⟩\\rangle\+b\.fst\)

⋅\\cdotnorm\_num\[<\-Nat\.dvd\_iff\_mod\_eq\_zero,g,\(1\)\.mod\_eq\_of\_lt,Nat\.dvd\_mul\]atthis⊢\\vdash

exists@?\_

⋅\\cdotcasesthis\.1with\|\_Qr=\>simp\_all\[\(Q\.dvd\_gcdr\.1⟨\\langle\_,\.symmr\.right\.choose\_spec\.2⟩\\rangle\)\.antisymm\]

cases@this\.2with\|\_FX=\>simp\_all\[\(F\.dvd\_gcdX\.1⟨\\langle\_,symmX\.2\.choose\_spec\.2⟩\\rangle\)\.antisymm\]

simp\_all\[mul\_comm,mul\_add,add\_comm,Nat\.add\_mod,Nat\.dvd\_iff\_mod\_eq\_zero\]

repeatuse\(Nat\.ModEq\.pow\_totient\(by\.\.\.norm\_num\)\)

Figure 16:ImProver 2 optimizes an AlphaProof proof for length, reducing tactic count by 26\.Figure[16](https://arxiv.org/html/2605.22885#A6.F16)comes fromAlphaProof\.P2, declarationimo\_2024\_p2\. The score changes from8080to5454\. The optimized proof removes a discarded intermediate lemma and folds repeated divisibility and Euler\-theorem reasoning into the main argument\. The resulting proof is still dense, but it is materially shorter while preserving the same number\-theoretic spine: prove the singleton characterization, force divisibility bya​b\+1ab\+1, and derivea=b=1a=b=1\.

#### F\.2\.3Modularity Optimization

Original \(human\-written\)

lemmaKD\_weakerThan\_KDB:\(Hilbert\.KDα\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KDBα\\alpha\):=normal\_weakerThan\_of\_subset$\\mathdollarbyintro;aesop;

ImProver 2 \(modularity\-optimized\)

lemmaKD\_weakerThan\_KDB:\(Hilbert\.KDα\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KDBα\\alpha\):=by

\-\-IntroducealemmatohandlethesubsetrelationshipbetweentheaxiomsofKDandKDB

haveh1:\(LO\.Modal\.Hilbert\.KDα\\alpha\)\.axioms⊆\\subseteq\(LO\.Modal\.Hilbert\.KDBα\\alpha\)\.axioms→\\rightarrow\(Hilbert\.KDα\\alpha\)≤s\\leq\_\{s\}\(Hilbert\.KDBα\\alpha\):=by

introh

\-\-Applythelemmathatestablishestheweakeningrelationgiventhesubsetofaxioms

applynormal\_weakerThan\_of\_subset

\-\-Usethegivensubsetcondition

applyh

\-\-ProvethesubsetrelationshipbetweentheaxiomsofKDandKDB

haveh2:\(LO\.Modal\.Hilbert\.KDα\\alpha\)\.axioms⊆\\subseteq\(LO\.Modal\.Hilbert\.KDBα\\alpha\)\.axioms:=by

\-\-ProvethatallaxiomsofKDareincludedinKDB

introφ\\varphihPhi

cases’hPhiwithhPhihPhi

⋅\\cdot\-\-Case:KD’sbasicmodallogicaxiomsareincludedinKDB

simp\_all\[LO\.Modal\.Hilbert\.KD\]

⋅\\cdot\-\-Case:KD’sadditionalaxiom\(K\)isincludedinKDB

simp\_all\[LO\.Modal\.Hilbert\.KDB\]

\-\-Combinetheresultstoconcludetheweakeningrelation

exacth1h2

Figure 17:ImProver 2 optimizes a proof for modularity, increasing modularity score \(see[A](https://arxiv.org/html/2605.22885#A1)\) by 2\.Figure[17](https://arxiv.org/html/2605.22885#A6.F17)comes fromFoundation\.Modal\.Hilbert\.WeakerThan\.KD\_KDB, declarationLO\.Modal\.Hilbert\.KD\_weakerThan\_KDB\. The modularity score increases from0to22\. The original proof is a one\-line use ofnormal\_weakerThan\_of\_subset; the optimized proof introduces two explicit intermediate claims, one reducing the theorem to an axiom\-subset statement and one proving that subset statement\. This raises the modularity score by exposing reusable subproof structure\.

Original \(human\-written\)

lemmahilbertPoly\_eq\_zero\_of\_le\_rootMultiplicity\_one

\{p:F\[X\]\}\{d:ℕ\\mathbb\{N\}\}\(hdp:d≤\\leqp\.rootMultiplicity1\):

hilbertPolypd=0:=by

by\_caseshp:p=0

⋅\\cdotrw\[hp,hilbertPoly\_zero\_left\]

⋅\\cdotrcasesexists\_eq\_pow\_rootMultiplicity\_mul\_and\_not\_dvdphp1with⟨\\langleq,hq1,hq2⟩\\rangle

haveheq:p=q\*\(\-1\)^p\.rootMultiplicity1\*\(1\-X\)^p\.rootMultiplicity1:=by

simponly\[mul\_assoc,←\\leftarrowmul\_pow,neg\_mul,one\_mul,neg\_sub\]

exacthq1\.trans\(mul\_comm\_\_\)

rw\[heq,←\\leftarrowzero\_addd,←\\leftarrowNat\.sub\_add\_cancelhdp,pow\_add\(1\-X\),←\\leftarrowmul\_assoc,

hilbertPoly\_mul\_one\_sub\_pow\_add,hilbertPoly\]

ImProver 2 \(modularity\-optimized\)

lemmahilbertPoly\_eq\_zero\_of\_le\_rootMultiplicity\_one

\{p:F\[X\]\}\{d:ℕ\\mathbb\{N\}\}\(hdp:d≤\\leqp\.rootMultiplicity1\):

hilbertPolypd=0:=by

\-\-Considerthecasewherepisthezeropolynomial

haveh1:p=0→\\rightarrowhilbertPolypd=0:=by

introhp

rw\[hp,hilbertPoly\_zero\_left\]

\-\-Considerthecasewherepisnotthezeropolynomial

haveh2:p≠\\neq0→\\rightarrowd≤\\leqp\.rootMultiplicity1→\\rightarrowhilbertPolypd=0:=by

introhphdp

\-\-Expresspasaproductofapolynomial,apowerof\-1,andapowerof\(1\-X\)

rcasesexists\_eq\_pow\_rootMultiplicity\_mul\_and\_not\_dvdphp1with⟨\\langleq,hq1,hq2⟩\\rangle

\-\-Derivetheequalityofpwiththeproductform

haveheq:p=q\*\(\-1\)^p\.rootMultiplicity1\*\(1\-X\)^p\.rootMultiplicity1:=by

simponly\[mul\_assoc,←\\leftarrowmul\_pow,neg\_mul,one\_mul,neg\_sub\]

exacthq1\.trans\(mul\_comm\_\_\)

\-\-SubstitutetheproductformintotheHilbertpolynomialexpressionandsimplify

rw\[heq,←\\leftarrowzero\_addd,←\\leftarrowNat\.sub\_add\_cancelhdp,pow\_add\(1\-X\),←\\leftarrowmul\_assoc,

hilbertPoly\_mul\_one\_sub\_pow\_add,hilbertPoly\]

\-\-Combinebothcasestoconcludetheproof

by\_caseshp:p=0<;\>simp\_all

<;\>simp\_all\[h1,h2,hdp\]

Figure 18:ImProver 2 optimizes a proof for modularity, increasing modularity score \(see[A](https://arxiv.org/html/2605.22885#A1)\) by 2\.Figure[18](https://arxiv.org/html/2605.22885#A6.F18)comes fromMathlib\.RingTheory\.Polynomial\.HilbertPoly, declarationPolynomial\.hilbertPoly\_eq\_zero\_of\_le\_rootMultiplicity\_one\. The modularity score increases from0to22\. The optimized proof factors the originalby\_casesproof into separate claims for the zero and nonzero polynomial cases before recombining them\. The result is longer, but it makes the case structure explicit, which is the behavior targeted by the modularity metric\.

Original \(AlphaProof\)

theoremimo\_2024\_p6

\(IsAquaesulian:\(ℚ\\mathbb\{Q\}→\\toℚ\\mathbb\{Q\}\)→\\toProp\)

\(IsAquaesulian\_def:∀\\forallf,IsAquaesulianf↔\\leftrightarrow

∀\\forallxy,f\(x\+fy\)=fx\+y∨\\veef\(fx\+y\)=x\+fy\):

IsLeast\{\(c:ℤ\\mathbb\{Z\}\)\|∀\\forallf,IsAquaesulianf→\\to\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.Finite∧\\wedge

\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.ncard≤\\leqc\}2:=by

exists@?\_

⋅\\cdot

useλ\\lambdaub=\>ifj:u0=0thenby\_contraλ\\lambdac=\>?\_else?\_

⋅\\cdot

suffices:\(\{J\|∃\\existsk,uk\+u\(\-k\)=J\}\)⊆\\subseteq\{0\}

⋅\\cdotsimp\_all\[this\.antisymm\]

rintro\-⟨\\langlea,rfl⟩\\rangle

contrapose\!c

simp\_all

suffices:\{U\|∃\\existsexamples6:ℚ\\mathbb\{Q\},uexamples6\+u\(\-examples6\)=U\}⊆\\subseteq\{0,\(u\(a:Rat\)\+\(u<\|@@↑\\uparrow\(\(\(\-a\)\)\)\)\)\}\.\.

⋅\\cdotconstructor

⋅\\cdotexact\(Set\.toFinite\(\_\)\)\.subset\(bysimpausingthis\)

⋅\\cdotexact\(Set\.ncard\_le\_ncard\(bysimpausingthis\)\)\.trans\(Set\.ncard\_pair\(Ne\.symm\(↑\\uparrow\(\(c\)\)\)\)\)\.le

rintro\-⟨\\langlehz,rfl⟩\\rangle

inductionb@hza

⋅\\cdot

have:=b\(\-a\)$hz\+ua

have:=bhzhz

simp\_all\[add\_comm\]

have:=b\(\-hz\)\(hz\+u↑\\uparrow\(hz\)\)

simp\_all\[add\_assoc,C\]

inductionthis

⋅\\cdot

simp\_all

have:=bhz\(hz\+\(ua\+u\(\-a\)\)\)

have:=b\(hz\+\(ua\+u\(\-a\)\)\)$hz\+\(ua\+u\(\-a\)\)

use\.inr$by\_contra$byhint

have:=bhz$hz\+\(uhz\+u\(\-hz\)\)

casesb\(hz\+\(uhz\+u\(\-hz\)\)\)$hz\+\(uhz\+u\(\-hz\)\)with\|\_=\>hint

have:=b\(\-hz\)\(uhz\+a\)

have:=b$\-a

specializethis\(uhz\+a\)

simp\_all\[←\\leftarrowadd\_assoc\]

have:=b0

have:=b

specializebaa

simp\_all\[add\_comm\]

have:=\(this<\|\-a\)\(↑\\uparrowa\+\(\(\(ua\)\)\):\(↑\\uparrow\_:\(\(\(\_\)\)\)\)\)\.\.

simp\_all\[add\_assoc\]

casesthis

⋅\\cdot

simp\_all

contrapose\!IsAquaesulian\_def

simp\_all

exfalso

have:=thisa\(a\+\(uhz\+u\(\-hz\)\)\)

simp\_all\[Ne\.symm,Bool\]

have:=⟨\\langle∀\\forallcongr\_argG,\_⟩\\rangle\(a\+\(uhz\+u\(\-hz\)\)\)$a\+\(u↑\\uparrowhz\+u↑\\uparrow\(\-hz\)\)

simp\_all

have:=thisa\(a\+\(ua\+u\(\-a\)\)\)

cases⟨\\langleforallJdS,\_⟩\\rangle\(a\+\(ua\+u\(\-a\)\)\)\(a\+\(ua\+u↑\\uparrow\(\-a\)\)\)with\|\_=\>hint

simp\_all

casesb00with\|\_=\>exactabsurd\(b0$\(0\+\(1\*\(@\(u↑\\uparrow\.\(\(0\)\)\)\)\)\)^01:↑\\uparrow\(\(\_\)\)\)\(id$\(by\(cases\(b\(u0\)\(\(u0\)\)\)with\|\_=\>continuity\)\)\)

rintroKV

specializeV$λ\\lambdaN=\>\-N\+2\*Int\.ceilN

specialize\(V$\(IsAquaesulian\_def\_\)\.mpr\_\)

⋅\\cdotsimp\_rw\[←\\leftarroweq\_sub\_iff\_add\_eq’\]

ring\_nf

usemod\_cast@?\_

norm\_num\[<\-add\_mul,Int\.ceil\_eq\_iff\]

useλ\\lambdacK=\>\(em\_\)\.imp\(⟨\\langlebylinarith\[Int\.ceil\_lt\_add\_onec,Int\.le\_ceilK\],\.⟩\\rangle\)\(byrepeatusebylinarith\[\.,Int\.le\_ceilc,or,Int\.ceil\_lt\_add\_one$K\]\)

simp\_all\[Int\.ceil\_neg,←\\leftarrowadd\_assoc\]

ImProver 2 \(modularity\-optimized\)

theoremimo\_2024\_p6

\(IsAquaesulian:\(ℚ\\mathbb\{Q\}→\\toℚ\\mathbb\{Q\}\)→\\toProp\)

\(IsAquaesulian\_def:∀\\forallf,IsAquaesulianf↔\\leftrightarrow

∀\\forallxy,f\(x\+fy\)=fx\+y∨\\veef\(fx\+y\)=x\+fy\):

IsLeast\{\(c:ℤ\\mathbb\{Z\}\)\|∀\\forallf,IsAquaesulianf→\\to\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.Finite∧\\wedge

\{\(fr\+f\(\-r\)\)\|\(r:ℚ\\mathbb\{Q\}\)\}\.ncard≤\\leqc\}2:=by

exists@?\_

⋅\\cdotuseλ\\lambdaub=\>ifj:u0=0thenby\_contraλ\\lambdac=\>?\_else?\_

⋅\\cdotsufficesh\_zero\_image:\(\{J\|∃\\existsk,uk\+u\(\-k\)=J\}\)⊆\\subseteq\{0\}

⋅\\cdotsimp\_all\[h\_zero\_image\.antisymm\]

rintro\-⟨\\langlea,rfl⟩\\rangle

contrapose\!c

simp\_all

sufficesh\_two\_values:

\{U\|∃\\existsexamples6:ℚ\\mathbb\{Q\},uexamples6\+u\(\-examples6\)=U\}⊆\\subseteq

\{0,\(u\(a:Rat\)\+\(u<\|@@↑\\uparrow\(\(\(\-a\)\)\)\)\)\}\.\.

⋅\\cdotconstructor

⋅\\cdotexact\(Set\.toFinite\(\_\)\)\.subset\(bysimpausingh\_two\_values\)

⋅\\cdotexact\(Set\.ncard\_le\_ncard\(bysimpausingh\_two\_values\)\)\.trans

\(Set\.ncard\_pair\(Ne\.symm\(↑\\uparrow\(\(c\)\)\)\)\)\.le

rintro\-⟨\\langlehz,rfl⟩\\rangle

inductionb@hza

⋅\\cdothaveh\_step\_i:=b\(\-a\)$hz\+ua

haveh\_diag:=bhzhz

simp\_all\[add\_comm\]

haveh\_step\_iv:=b\(\-hz\)\(hz\+u↑\\uparrow\(hz\)\)

simp\_all\[add\_assoc,C\]

inductionh\_step\_iv

⋅\\cdotsimp\_all

haveh\_shift\_x:=bhz\(hz\+\(ua\+u\(\-a\)\)\)

haveh\_shift\_self:=b\(hz\+\(ua\+u\(\-a\)\)\)$hz\+\(ua\+u\(\-a\)\)

use\.inr$by\_contra$byhint

⋅\\cdothaveh\_zero\_case:=bhz$hz\+\(uhz\+u\(\-hz\)\)

casesb\(hz\+\(uhz\+u\(\-hz\)\)\)$hz\+\(uhz\+u\(\-hz\)\)with\|\_=\>hint

⋅\\cdothaveh\_neg\_x:=b\(\-hz\)\(uhz\+a\)

haveh\_neg\_a\_all:=b$\-a

specializeh\_neg\_a\_all\(uhz\+a\)

simp\_all\[←\\leftarrowadd\_assoc\]

haveh\_zero\_all:=b0

haveh\_all:=b

specializebaa

simp\_all\[add\_comm\]

haveh\_a\_shift:=\(h\_all<\|\-a\)\(↑\\uparrowa\+\(\(\(ua\)\)\):\(↑\\uparrow\_:\(\(\(\_\)\)\)\)\)\.\.

simp\_all\[add\_assoc\]

casesh\_a\_shift

⋅\\cdotsimp\_all

contrapose\!IsAquaesulian\_def

simp\_all

exfalso

haveh\_test\_a:=h\_alla\(a\+\(uhz\+u\(\-hz\)\)\)

simp\_all\[Ne\.symm,Bool\]

haveh\_test\_self:=⟨\\langle∀\\forallcongr\_argG,\_⟩\\rangle\(a\+\(uhz\+u\(\-hz\)\)\)$

a\+\(u↑\\uparrowhz\+u↑\\uparrow\(\-hz\)\)

simp\_all

⋅\\cdothaveh\_test\_a:=h\_alla\(a\+\(ua\+u\(\-a\)\)\)

cases⟨\\langleforallJdS,\_⟩\\rangle\(a\+\(ua\+u\(\-a\)\)\)\(a\+\(ua\+u↑\\uparrow\(\-a\)\)\)with\|\_=\>hint

⋅\\cdotsimp\_all

casesb00with\|\_=\>exactabsurd\(b0$\(0\+\(1\*\(@\(u↑\\uparrow\.\(\(0\)\)\)\)\)\)^01:↑\\uparrow\(\(\_\)\)\)\(id$\(by\(cases\(b\(u0\)\(\(u0\)\)\)with\|\_=\>continuity\)\)\)

rintroKV

specializeV$λ\\lambdaN=\>\-N\+2\*Int\.ceilN

haveh\_model\_aqua:

IsAquaesulian\(λ\\lambdaN:ℚ\\mathbb\{Q\}=\>\-N\+2\*Int\.ceilN\):=by

refine\(IsAquaesulian\_def\_\)\.mpr?\_

simp\_rw\[←\\leftarroweq\_sub\_iff\_add\_eq’\]

ring\_nf

usemod\_cast@?\_

norm\_num\[<\-add\_mul,Int\.ceil\_eq\_iff\]

useλ\\lambdacK=\>\(em\_\)\.imp

Original \(continued\)

suffices:2<=V\.1\.toFinset\.card

⋅\\cdotletM:=V\.1\.toFinset

haveh2nat:2≤\\leq\(\{x\|∃\\existsr:ℚ\\mathbb\{Q\},2\*↑\\uparrow⌈\\lceilr⌉\\rceil\+\-\(2\*↑\\uparrow⌊\\lfloorr⌋\\rfloor\)=x\}:Setℚ\\mathbb\{Q\}\)\.ncard:=by

rwa\[Set\.ncard\_eq\_toFinset\_card\_V\.1\]

haveh2int:\(2:ℤ\\mathbb\{Z\}\)≤\\leq\(\{x\|∃\\existsr:ℚ\\mathbb\{Q\},2\*↑\\uparrow⌈\\lceilr⌉\\rceil\+\-\(2\*↑\\uparrow⌊\\lfloorr⌋\\rfloor\)=x\}:Setℚ\\mathbb\{Q\}\)\.ncard:=by

exact\_mod\_casth2nat

exacth2int\.transV\.2

useFinset\.one\_lt\_card\.2$by

refine⟨\\langle0,V\.1\.mem\_toFinset\.2?\_,2,V\.1\.mem\_toFinset\.2?\_,bynorm\_num⟩\\rangle

⋅\\cdotexact⟨\\langle\-1,bynorm\_num⟩\\rangle

⋅\\cdotexact⟨\\langle\(1/2:ℚ\\mathbb\{Q\}\),bynorm\_num⟩\\rangle

ImProver 2 \(modularity\-optimized; continued\)

\(⟨\\langlebylinarith\[Int\.ceil\_lt\_add\_onec,Int\.le\_ceilK\],\.⟩\\rangle\)

\(byrepeatusebylinarith\[\.,Int\.le\_ceilc,or,Int\.ceil\_lt\_add\_one$K\]\)

specializeVh\_model\_aqua

simp\_all\[Int\.ceil\_neg,←\\leftarrowadd\_assoc\]

haveh\_card\_toFinset:

2<=V\.1\.toFinset\.card:=by

useFinset\.one\_lt\_card\.2$by

refine⟨\\langle0,V\.1\.mem\_toFinset\.2?\_,2,V\.1\.mem\_toFinset\.2?\_,bynorm\_num⟩\\rangle

⋅\\cdotexact⟨\\langle\-1,bynorm\_num⟩\\rangle

⋅\\cdotexact⟨\\langle\(1/2:ℚ\\mathbb\{Q\}\),bynorm\_num⟩\\rangle

haveh\_card\_ncard:

2≤\\leq\(\{x\|∃\\existsr:ℚ\\mathbb\{Q\},2\*↑\\uparrow⌈\\lceilr⌉\\rceil\+\-\(2\*↑\\uparrow⌊\\lfloorr⌋\\rfloor\)=x\}:Setℚ\\mathbb\{Q\}\)\.ncard:=by

rwa\[Set\.ncard\_eq\_toFinset\_card\_V\.1\]

haveh\_card\_int:

\(2:ℤ\\mathbb\{Z\}\)≤\\leq\(\{x\|∃\\existsr:ℚ\\mathbb\{Q\},2\*↑\\uparrow⌈\\lceilr⌉\\rceil\+\-\(2\*↑\\uparrow⌊\\lfloorr⌋\\rfloor\)=x\}:Setℚ\\mathbb\{Q\}\)\.ncard:=by

exact\_mod\_casth\_card\_ncard

exacth\_card\_int\.transV\.2

Figure 19:ImProver 2 optimizes an AlphaProof proof for modularity, increasing modularity score by 3\.Figure[19](https://arxiv.org/html/2605.22885#A6.F19)comes fromAlphaProof\.P6, declarationimo\_2024\_p6\. The score changes from0to33\. The modularity\-optimized version introduces named intermediate claims such ash\_zero\_image,h\_two\_values, andh\_model\_aqua\. These names expose the proof’s main subgoals: bounding the image set, verifying the model function is aquaesulian, and converting cardinality facts back to the final integer bound\.