EvolProver: Advancing Automated theorem proving by Evolving Formalized Problems via Symmetry and Difficulty
Authors: Yuchen Tian
Ruiyuan Huang
WANG XUANWU
Jing Ma
Zengfeng Huang
Ziyang Luo
Hongzhan Lin
Da Zheng
Lun Du
Venue: ICLR 2026 Poster (2026)
Keywords: Formal Theorem Proving
AI4Math
LLM4Math
Automated Theorem Proving
Prover
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Large Language Models (LLMs) for formal theorem proving have shown significant promise, yet they often lack generalizability and are fragile to even minor transformations of problem statements. To address this limitation, we introduce a novel data augmentation pipeline designed to enhance model robustness from two perspectives: symmetry and difficulty. From the symmetry perspective, we propose two complementary methods: **EvolAST**, an Abstract Syntax Tree (AST) based approach that targets syntactic symmetry to generate semantically equivalent problem variants, and **EvolDomain**, which leverages LLMs to address semantic symmetry by translating theorems across mathematical domains. From the difficulty perspective, we propose **EvolDifficulty**, which uses carefully designed evolutionary instructions to guide LLMs in generating new theorems with a wider range of difficulty. We then use the evolved data to train **EvolProver**, a 7B-parameter non-reasoning theorem prover. EvolProver establishes a new state-of-the-art (SOTA) on FormalMATH-Lite with a 53.8\% pass@32 rate, surpassing all models of comparable size, including reasoning-based models. It also sets new SOTA records for non-reasoning models on MiniF2F-Test (69.8\% pass@32), Ineq-Comp-Seed (52.2\% pass@32), and Ineq-Comp-Transformed (34.0\% pass@32). Ablation studies further confirm our data augmentation pipeline's effectiveness across multiple benchmarks.

Published as a conference paper at ICLR 2026
EVOLPROVER: ADVANCING AUTOMATED THEOREM PROVING BY EVOLVING FORMALIZED PROBLEMS VIA SYMMETRY AND DIFFICULTY
Yuchen Tian--211 122x
Ruiyuan Huang Xuanwu Wang'
Jing Ma
Zengfeng Huang Ziyang Luo Hongzhan Lin'
Da Zheng Lun Du 28
'Hong Kong Baptist University
2 Ant Group
Schooo of Data Science, Fudan University
"Shanghai Innovation Institute
ABSTRACT
Large Language Models (LLMs) for formal theorem proving have shown signif- icant promise, yet they often lack generalizability and are fragile to even minor transformations of problem statements. To address this limitation, we introduce a novel data augmentation pipeline designed to enhance model robustness from two perspectives: symmetry and difficulty. From the symmetry perspective, we propose two complementary methods: EvolAST, an Abstract Syntax Tree (AST) based approach that targets syntactic symmetry to generate semantically equivalent problem variants, and EvolDomain, which leverages LLMs to address seman- tic symmetry by translating theorems across mathematical domains. From the difficulty perspective, we propose EvolDifficulty, which uses carefully designed evolution-base based instructions to guide LLMs in generating new theorems with a wider range of difficulty. We then use the evolved data train EvolProver, a 7B 7B-parameter non-reasoning theorem prover. EvolProver establishes a new state- of-the-art (SOTA) on FormalMATH-Litt with 53.8% pass @ 32 rate, surpassing all models of comparable size, including reasoning- models. It also sets new SOTA records for non-reasoning models on -iniF2F-Test (69.8% pass@ mass Ineq- Comp-Seed (52.2% pass @ 32), and Ineq-Comp- Treg--oom-TTaafffmmee Transformed (34.0% pass 32). Ablation studies further confirm our data augmentation pipeline's 's effectiveness across multiple benchmarks.
INTRODUCTION
Large Language Models (LLMs) have demonstrated significant potential in mathematical reasoning, sparking a surge research into their application for formal theorem proving. Formal languages like Lean (Moura & Ullrich, 2021), Coq (Barras et al., 1997), and Isabelle (Paulson, 1994) represent math- ematical proofs as rigorous code implementations. This process demands strict syntactic precision and logical soundness, with every proof requiring compiler verification. While this guarantees the absolute reliability proofs, also creates major bottleneck: the extreme scarcity of high-quality training data. Crafting formal proofs requires deep domain expertise and substantial time, reality that fundamentally conflicts with the data-inted intensive paradigm LLMs.
To address the scarcity for data, the research community has explored various data synthesis methods. For instance, DeepSeek-Prosee Prover (Xin et al., 2024a) attempts to automatically translate a large number of informal natural language problems into formal statements, using model scoring and hypothesis
Equal contribution.
1 The idea of this work was proposed when the first author was an intern at Ant Group before joining HKBU, and the work was completed after he joined HKBU.
1
Work done during internship at Ant Group.
Corresponding authors. Correspondence to: Jing Ma <majing@hkbu.cduu. Da Zheng
<7hengda zheng antm,, homnaagaam.h Lun Du eculun.dl@antgrroug

---

Published as a conference paper at ICLR 2026
EvolDomain
Seed Formal Statement
1
EvolDifficulty
Evolved Problem:
thearem exam (x RR) (h: (x+1)
Evolved Problem: that for any real numbers and y, y xx² equals zero, then must be equal or must equal to -X.
Prove that point the Euclidean plane lies both the unit circle centered at the origin and horizontal axis, then its coordinates must be either (1, 0) or (-1,0).
(x + 1)= 0): :x V
LLM
eorry
LLM
EvolAST(EvolDomain)
theorem Ast_1 (P: EuclideanSpace R (Fin axis: 0 P
Evolved Statement:
Axiom
(h corcll IIII): P [[-1, P
theorem Evol_dm shol_dm([ (P:
Evolved Statement: theorem Evol, df (xy R): y²2=x~2 - =y=xVy=** by sorry
[[1.0] by sorry
EuclideanSpace 3. (Fin 2)) on circle:
1)
(h_ on an_axis: : =
EvolAST (EvolDifficulty)
P = ![1, 0J P ![-1, 0] : by
theorem 2 (x :R)): xx22=y22 Vy sorry
sorry
Axiom
Figure 1: An example of problems evolved by EvolDomain, EvolDifficulty and EvolAST. A seed formal statement evolved parallel by EvolDomain and EvolDifficulty, yielding two new state- ments. Each of these is then further evolved by EvolAST to generate syntactic variants.
rejection mechanism for screening. Gocdel-Prover- V2 (Lin et al., 2025) adopts a scaffolded strategy to generate mathematical problems of appropriate difficulty to provide models with more effective learning signals. Meanwhile, STP (Dong & Ma, 2025) constructs two adversarial roles of a conjecturer and prover that iteratively improve to jointly generate new problems and proofs.
However, line of work has shown that models trained with such synthesized data still lack gener- alizability. For example, Zhao et al. (2025a) noted that minor transformations of a problem, such transforming an inequality of the form f(x) > g(xr) to f(x) + [(v) g(æ) + g(y), degrade the performance of LLMs drastically. Furthermore, other studies (Hao et al., 2025; Huang et al., 2025) have revealed that this fragility is not unique formal reasoning; informal LLMs are also susceptible to minor problem transformations. Motivated by this, we propose a novel data augmentation pipeline improve model generalizability by addressing from two perspectives: symmetry and difficulty.
In mathematics, symmetry means exactly invariance under certain transformations. From the symme- try perspective, the fragility of existing models against minor transformations of problems suggests they fail to learn the underlying symmetry structure of the mathematical problem. To address this, we introduce two complementary methods targeting syntactic and semantic symmetry. The first, EvoLAST, addresses syntactic symmetry using Abstract Syntax Tree (AST). It parses formal statement into an AST, applies equivalence transformations using a library of axioms and theorems, and converts the modified tree back into new statement. This generates semantically identical but syntactically diverse problems. The core strength of EvolAST is its extensibility, as any mathematical equivalence can be encoded as a new transformation rule, allowing for systematic enrichment of the data's structural diversity.
Our second method, EvolDomain, addresses semantic symmetry, where theorem can be rein- terpreted in different domains while preserving its core logic. EvolDomain uses evolution-base instructions guide LLMs in translating theorems across mathematical domains, thereby creating novel and diverse problem statements.
From the difficulty perspective, studies have shown that models trained on data with narrow difficulty range often fail to generalize (Jiang et al., 2023; Parashar et al., 2025). To mitigate this, we propose EvolDifficulty. method that uses carefully designed instructions to evolve existing theorems by adjusting their difficulty. This process creates dataset with much broader difficulty spectrum, which discourages models from relying on shortcuts or mere memorization.
Combining EvolAST, EvolDomain, and EvolDifficulty, we create a comprehensive data augmentation pipeline. Example problems evolved by our pipeline in provided in Figure 1. We apply this pipeline to augment public datasets such STP (Dong & Ma, 2025) and Deepseek-Prover-- 2024a). By training DeepSeek-Prowe Prover- 11.5-Base on this augmented data, we produce our model, EvolProver. EvolProver achieves tfite--f-thhaaas (SOTA) performance multiple benchmarks. Notably, EvolProver is a non non-reasoning (i.e., non-CoT) model. yet it achieves results comparable to, and sometimes surpassing, those of reasoning models. On FormalMATH-L... (Yu al., 2025),
(Xin et al.,
2

---

Published as a conference paper at ICLR 2026
it sets new SOTA with 53.8% pass@32 rate among models of comparable size, including reasoning models. Furthermore, it establishes new SOTA pass @ 32 rates for non-reasoning models of comparable size several benchmarks: 69.8% on MiniF2F-Test (Zheng al., 2021), 52.2% (Zhao et al., 2025a), and 34.0% on Ineg-Comp-Transffrmee 2025a). Ablation studies confirm the efficacy of our pipeline, showing that EvolProver outperforms its counterparts trained on unaugmented or partially augmented data, in some cases by over 10 percentage points.
on
(Zhao et al.,
The main contributions of this work can be summarized as follows:
We propose a novel data augmentation pipeline that improves model generalizability by systematically enhancing formalized data directly from both symmetry and difficulty per- spectives.
We propose EvolAST, highly extensible, AST-based method that generates syntactically diverse yet semantically equivalent problems by leveraging formal axioms and theorems transformation rules. Additionally, we introduce EvolDomain and EvolDifficulty, two LLM-driven methods that enrich training data by translating problems across domains and evolving their difficulty, respectively.
We train and release EvolProver, a powerful non-reasoning theorem prover built on our aug- mented data. EvolProver achieves state-of-the-art performance across multiple benchmarks, outperforming all comparable models on FormalMATH-LLite and setting new records for non-reasoning models on others.
RELATED WORKS
Formal Provers. Numerous LLMe-bsed formal provers (Ji et al., 2025; Zhang et al., 2025; Shang et al., 2025) have emerged after the advent of ChatGPT, including reasoning-based models like DeepSeck-Provets
(Ren et al., 2025), non-reasoning models like STP (Dong & Ma, 2025), and tree-search models like BFSS-Pover-V1 (Xin al., 2025a) & BFS--Pooer-VV (Xin et al., 2025b). for non-rensoning models, which offer significant
Our work focuses on advancing the computational efficiency.
Data Augmentation in Mathematical Reasoning, The critical need for large-scale, high-quality training data has spurred significant research into automated methods for mathematical problem generation. Prominent approaches in informal mathematics include MetaMath (Yu et al., 2024), which bootstraps new data by rewriting existing questions from multiple perspectives like rephrasing and backward reasoning. Similarly, WizardMath (Luo et al., 2025a) adapts the Evol-Instruct frame- work (Luo et al., 2025b; Xu et al., 2024) to systematically generate problems of varying complexity. Another work. PromptCoT (Zhao et al., 2025b), focuses on synthesizing complex problems by emulating the design process of human experts, grounding the generation in core mathematical concepts and logical structures. In the context of formal mathematies, STP (Dong & Ma, 2025) uses a single L.M that alternates between a "conjecturer" and a "prover" in a self-play loop, thereby synthesizing new formal conjectures and proofs from limited seed data. Ineq-Comp (Zhao al., 2025a) starts from simple inequalities and applies small but systematic algebraic transformations. such as duplicating variables and adding or multiplying inequalities, or performing substitutions like squaring and taking square roots, to construct families of more structurally complex composite inequalities. Inspired by both these informal and formal data- aughmmtatgttnno pipelines, we introduce ExolDomain and EvolDifficclly.. These methods also utilize L.Mss but specifically focus on the evolution of formal mathematical statements to enhance their complexity and domain coverage, thereby increasing the diversity of the training data.
While these approaches expand the range and depth of generated problems, they also expose an inherent weakness of LLM-based evolution: the inevitable introduction of syntactic semantic errors. To mitigate this issue, we propose EvolAST. EvoLAST leverages the programmatic features of the Lean 4 proof assistant to perform rewrites directly at the Abstract Syntax Tree (AST) level. This approach ensures that all generated formal statements are syntactically correct and semantically equivalent, effectively increasing data diversity and precision.
3

---

Published as a conference paper at ICLR 2026
Existing Verified
Formal Statements
theorem thm ( b (h,
Informal Formal Statements
s b b 100) (h, j
99 (b % 10)) (h, : 2
5)) b 18 by sorry
Verification
Evolve
EvolAST
Evolution Strategy
to Check Syntax
Extracted ASTs from formalized statements
58a Extracted AST
EvolDomain
Lewn Geraer
Occonstruction Abstraction
Stap2. Analogy Trarsfer
Correct Syntax one time according to Errors
6 688
Step3. Instantiation Packaging
EvolDifficulty
688
Utilize LLM Check Consistency Correctness Difficulty
Predefined Rules
Adjun Logical Structurn
Adjust Depth
theorem thm aug (jbMM (h
Adjust Abstraction
2 (5+ b) (b,
Adjust Constraints
> bJ (h (b
10) :-b= 18:=
Adjart Paramebera
Delete
sorry
Figure 2: The workflow of our data augmentation pipeline comprises three phases: EvolDomain and EvolDifficulyy, Verification, and EvoLAST.
Robustness of LLMs in Mathematical Reasoning. Recent work has highlighted that LLMs lack robustness against small perturbations in mathematical problems, such as variable renaming or adding noise. For instance, the PutnamGAP benchmark (Hao al., 2025) tests equivalence-preste preseeeingg variants and shows average accuracy declines of 3- 10%. Similarly, MATH-P-Hard (Huang et al., 2025) introduces structural shifts, causing performance drops of 10-25% in models like ol-mini.
While this issue is recognized in informal mathematics, the robustness of LLMs in formal reasoning systems like Lean and Coq remains largely underexplored. Built from systematically composed inequalities, the Ineq-Comy benchmark (Zhao et al., 2025a) was developed to address this gap by measuring prover's performance drop between original problems and their perturbed counterparts.
3 METHOD
Our methodology is centered around a multi-stage data augmentation pipeline, as illustrated in Figure 2. First, we leverage LLMs to expand existing formal statements through two evolution-basee processes:
EvolDomain, for cross-domain translation, and EvolDifficulty, for complexity adjustment. After rigorous verification stage, further diversify the data's syntactic structure using EvolAST, a deterministic AST-based transformation method. Finally, we train our model, EvolProver, on this augmented dataset. To control the instability introduced each stage, we that the LLM-driven steps (omoiDomain, EvolDifficulty) behave like exponential magnification (x - exp(x)): since they based on LLMs. they may introduce significant and unpredictable changes, and the propagation of such instability can be likened to an exponential function where small initial perturbation may grow into exp(x). In contrast, EvolAST, as a deterministic, syntax- -basad transformation, introduces much smaller instability; its effect is more similar to a linear function, effectively turning r into 2r. Executing the LLM-based stages first and then applying the syntactic transformation (a (c-eep(x)) - exp(x)) avoids prematurely amplifying noise. Keeping the overall instability at a moderate level is crucial, because overly unstable problems become hard to prove, which in turn prevents from obtaining enough valid training instances to support effective data augmentation strategy. This procedure allows us to both enrich the diversity of the data and maintain a sufficient amount of training data. The following sections detail each component of this pipeline.
4

---

Published as a conference paper at ICLR 2026
3.1 EVOLDOMAIN AND EVOLDIEFICULTY
Proven formal statements, with their inherent semantic and syntactic correctness, serve as ideal seeds for data generation. Our work mainly builds upon two open-source datasets, Srepseek-Proverr V and STP-Lean, which often lack natural language descriptions. We therefore evolve these formal statements directly by instructing an LLM generate new, related theorems. This approach leverages the logical structure embedded in the formal language itself as a basis for creative generation, bypassing the need for natural language intermediaries.
EvolDomain. EvolDomain leverages an LLM to translate formal statement into new mathematical domains. This process involves three main steps: 1) abstracting the statement's 's logical skeleton, 2) identifying analogous concept in target domain, and 3) instantiating based on this analogy.
concrete proposition
Formally, let this process be function F. Given source statement Sffomal and target domain D, (selected from a predefined list LD = (D1, Dz..... Da }). F guides an LLM to first extract the statement's 's abstract logical skeleton. Based this skeleton, the model identifies structurally similar concept in Dm and uses it to construct a new proposition. The output is a pair consisting of a natural language description, Pi, and a new formal statement, Sformal, This can be formally represented as: F(Stormal D.. (Stormal P.).
To maximize the exploration of logical connections across domains, our prompt further guides the LLM simultaneously transfer and instantiate the core logical skeleton into 5 distinct new domains. Therefore, the final output of a single function call is a set of pairs spanning multiple domains, with each pair containing new formal statement and its corresponding natural language description. Prompt templates and examples can be found in Appendix A.3.
EvolDifficulty EvolDifficulty leverages an LLM to adjust formal statement's 's difficulty, thereby creating dataset with broad difficulty spectrum. We denote this process by the function E. The process, E, is guided by carefully designed evolution strategies. Based on expert consultation, designed five core evolution strategies, S = (s...... $5 (1) Adjusting Logical Structure, (2) Adjusting Mathematical Depth, (3) Adjusting Abstraction, (4) Adjusting Constraints, and (5) Adjusting Parameters. Given a formal statement Stormal the function applies strategy 8y. S with an evolution direction 8 E [+1,-1] (for increasing or decreasing difficulty, respectively) to instruct
an LLM to generate new pair of new formal statement Stormal and its natural language description P.. This can be formally represented as E(f.ormal 5kk 6) (Stormal ,.).
By systematically applying this framework, EvolDifficulty enables fine-grained control over dataset difficulty, generating problems with smooth gradient that enriches the dataset's hierarchical structure. Prompt templates and examples can be found in Appendix A.4.
Verification. We employ a stringent two-stage verification pipeline ensure data quality. First, each generated statement Syformal is validated for syntactic integrity using the Lean compiler. Statements that fail are given a single LLM-based repair attempt before being discarded. Second, all syntactically valid pairs (S(ormal, P?) undergo semantic evaluation by an LL-M-based judge. The judge assesses three aspects: consistency between the formal and natural language versions, propositional correctness, and difficulty appropriateness. This dual-filter mechanism, combining deterministic compilation with semantic judgment, ensures that only syntactically sound and semantically coherent data populates our final dataset. Prompt templates can be found in Appendix A.5.
3.2 EVOLAST
EvolAST is founded on the principle that formal language statements, structured code, can be parsed into Abstract Syntax Tree (AST). This allows us to bypass non-deterministic models and instead apply deterministic set of rewriting rules based established axioms and theorems, guaranteeing semantic equivalence.
We formalize this process function A. EvolAST implements an extensible set of rewriting rules (currently rules), R = (ri..... .7.) where each rule т corresponds to a specific logical equivalence: (1) Hypothesis Reordering, (2) Commutativity, (3) Associativity, (4) Distributivity, (5)
5

---

Published as a conference paper at ICLR 2026
De Morgan's Laws, (6) Operand Swapping for Symmetric Relations, and (7) Dual Relation Conver- sion. Given an input statement Sfurmal the function first parses it into an AST. It then recursively traverses the tree, applying any applicable rule тı R at each node with predefined probability p. Finally, the modified AST recompiled into new formal statement Stormal The process can be formally represented as A( .p) Stormall
We provide an example in Appendix A.6.
Since all transformations are based strict logical equivalences, EvolAST generates syntactically diverse data while ensuring semantic correctness, thus eliminating the need for further verification. The framework is highly extensible, any known mathematical logical equivalence can be encoded as a new rewriting rule.
3.3 TRAINING EVOI,PROVER
We train our final model, EvolProver, by fine-tuning DeepSee\Prover-II.5--B (Xin et al., 2024b) on our augmented dataset. DeepSeekProver- V1.5-Base is currently the strongest model pretrained purely large-scale formal theorem prrvving data without chain-of-thought supervision, making it particularly well suited for our synthetic data and our goal of enhancing fast, non-reasoning provers. The training process consists of two stages: Supervised Fine-Tuning (SFT) and Reinforcement Learning (RL). Detailed information on dataset curation and training algorithms can be found in Appendix A.I.
For comparison and ablation studies, we also trained several other models. This includes a baseline model, EvolProver-Bate which was trained exclusively the original, unaugmented public data. We also prepared series of specialized models for our comprehensive ablation experiments, with details provided in Appendix A.2.
EXPERIMENTS
4.1
BASELINES
Existing formal provers are broadly categorized into three types: non-reasoning, reasoning, and tree-search models.
Non-reasoning models generate proofs end-to-end without an intermediate thought process. Key examples include SeepSeek-Prover V2 (non-CoT) (Ren et al., 2025), Goedel Provee--Poove-SFT (Lin et al., 2025), and STP (Dong Ma, 2025).
Reasoning models employ a chain-of- -f-thoughtt process generate proofs, where the reasoning process often significantly longer than the final proof. Key examples are DeepSeek PeepSek-Prrver-- Prover- V2 (CoT) (Ren et al., 2025), Moonshot's 's Kimi-Pre Limi-Prover-Paee Prover-Preview (Wang et al., 2025a) and Kimi-Prover (Wang et al., 2025b), and Sroedel-Prover- V2 (Lin et al., 2025). Notably, DeepSeck-Prover- and non-reasoning mode. While generally higher performing, reasoning models demand substantial computational resources due to their chain-of-thowd of-thought approach (e.g., more than 6000 tokens per proof vs. less than 700 for non-reasoning models). This focus token efficiency has spurred recent wave of interest in fast, non-reasoning models, such as Claude 4's Non-thinking mode (Anthropic, 2025) and Frokk-Code-Fast- (xAI, 2025).
has both reasoning
Tree-search models represent an intermediate proof state as a node in a search tree and use a model assign heuristic scores guide the search order. Key examples include BFS-Prover (Xin al., 2025a), DeepSeek-Provers
RMaxTS (Xin et al., 2024b), and Me.mm..M..-SStPProree (Wu
al., 2024).
For our comparative analysis, we report the performance metrics published by the original authors ensure consistency and avoid discrepancies from our own re-evaluations.
4.2 RESULTS
FormalMATH (Yu et al., 2025) is broad dataset of formal theorems. We follow standard practice and evaluate its 425-problem subset, FormalMATH--itee, as other problems in the full dataset were

---

Published as a conference paper at ICLR 2026
Table Comparison with SOTA 7B-size models the FormalMATH--ice dataset; means increase in absolute performance over the ablation model EvolProver-Base Average Token Length means the average number of output tokens across the benchmark. We do not report average token length for tree-search models, as this metric is not directly comparable with other model types.
Models
Average Token Length
Sample Budget
FormalMATH
Reasoning Models
DeepSeek-Prover V
4804.6
51.76%
Kimina-Prover-PPee Perover-Preview
6097.7
32
48.94%
Tree-Search Models
MicmLLMM.--SSepPrroee
N/A
1
3200
7.87%
BFS-Prover
N/A
1 3200
27.19%
Con-Reasoning Models
DeepSeek-Proved (e.c--11.55555 1.5-SFT
115.9
32
40.40%
DeepSeck-Prover-V Pr.ver--....-...
163.4
32
47.98%
Goedel-Provar-SFT
458.4
32
46.70%
STP
186.8
32
48.59%
Sra.--Pooroee-----oo------ BvolProver-Base(Uuus)))
394.5
32
50.35 %
629.8
32
44.71 %
EvolProver(Ours)
653.7
32
53.86 %
used in training. Problems within FormalMATH-Lite were held out and used exclusively for final evaluation.
The results summarized in Table 1. EvolProver achieves new SOTA of 53.86% among models of comparable size, surpassing the previous best 51.76%. Notably, our non-reasoning model outperforms top reasoning models like DeepSeek-Proved V2 and Piii--rrvver--eieeee Furthermore, EvolProver outperforms its baseline, EvolProver-Base by 9.15 percentage points, demonstrating the significant impact of our data augmentation pipeline.
MiniF2F (Zheng et al., 2021) is standard benchmark comprising 488 problems from mathematics competitions. Following common practice, report results on its 244--r4bleee test set, MiniF2F- Test. The results are presented in Figure 3. EvolProver achieves a pass @ 32 rate of 69.80% on MiniF2F-Test, establishing a new SOTA performance among non-reasoning models of comparable size. Notably, this performance is comparable to, and in some cases exceeds, that of reasoning models, despite using significantly fewer tokens (a nearly 10-fold reduction in token consumption). Due to the construction of the training data, the content generated by EvolProver, in addition to the proof, also includes a restatement of the problem, while further analysis is placed in section A.8, which makes its outputs slightly longer than those of the other non-chain-of ttotthhutht models.
Ineq-Coue Comp (Zhao et al., 2025a) is benchmark designed to evaluate the robustness of formal provers against minor problem perturbations. It contains 75 seed problems from Olympiad-leve inequalities and 150 corresponding transformed variants. Each seed problem is systematically altered through simple operations(e.g.) algebraic rewrites, variable duplication) to create two transformed variants. While humans can easily solve these transformed problems, formal provers often struggle with them if they solve the original. model's 's robustness is measured by the ratio of its performance on transformed problems to its performance on the seed problems, for which a higher ratio indicates greater robustness.
Our results are presented in Table 2. EvolProver again sets a new SOTA for non-reasoning models on all three metrics (seed, transformed, and ratio), outperforming the next-best non-reasoning model by a significant margin. Its performance is also comparable to that of top reasoning models. Notably, our data augmentation pipeline leads to substantial boost in robustness: EvolProver's robustness ratio is 30.74 percentage points higher than that of EvolProver-Bass demonstrating the effectiveness of our approach.
ANALYSIS
Evolution Strategy. EvolDifficulty and EvolDomain employ a general LLM to directly evolve formalized mathematical theorems. This approach addresses the inherent complexity of mathematical
7

---

Published as a conference paper at ICLR 2026
Non-CoT
CoT
Kinine ParnillB
59. (5. volPowee))
Pase Roitet
Goodal Prover
(2. wowProver-Baaseeeeo
Seep V1.66R
WvalProver-ce -aaa
50
DoepSeos Prover V1.5 SFT
40
Average Takan Longth
Awerage Takan Longth
Figure 3: Comparison with SOTA models on the MiniF2F-Tess dataset. Pass Rate means pass @ 32 success rate. Average token length is the average number of tokens generated by models across the benchmark. We categorize models as Non-Can Non-CoT(non reasoning) and CoT(reasoning)
Table 2: Comparison with SOTA 7B-size models on the Ineq-Comp Benchmark; Pass means pass @ 32 rate for reasoning models and non reasoosnnnng models, and means x 3200 pass rate for tree-search models. means increase in absolute performance over the ablation model EvolProver- Base.
Models
Pass on Seed
Pass on Transformed
Pass Ratio
Reasoning Models
PeepSeck-Prover-V.. (COT)
66.23%
44.53%
67.23%
Prreeee-rrver--rreviee
50.06%
27.58%
55.09%
Tree-Search Models
DeepSeek-Prover V1.5 (RL + RMaxTS)
42.66%
14.83 %
34.76 % 16.6 %
IntemL.M2.5-StepPProw
25.59%
3.44 %
Reasonis Models
DeepSeek- Proverovveevee V1.5 (RL)
34.40%
6.68%
19.42%
43, 43.46%
14.54%
33.47%
22-7B-non-Co
56. 56.00%
27.33%
48. 48.90%
EvolProver-Base (Ours)
43.26%
14.89 %
34.43% %
EvolProver (Ours)
52.20 c 8.94%)
34.02 % 19.13%)
65.17% %6 30.74%)
formalization(Lu et al., 2025; Li et al., 2025), task traditionally reliant specialized models trained to convert natural language problems into formal expressions. However, the direct application of general-purpose LLMS for this purpose remains relatively unexplored, leaving their comparative advantages and limitations as an open question.
To validate strategy of directly evolving formal statements, compare it against common alternative: evolving Natural Language (NL) problems first and then formalizing them. We designed controlled experiment with four branches:
EvolDomain & EvolDifficulty (Ours): Directly evolves new formal statements from existing ones.
Formalization-Formaaiizz Evolves NL problems, then formalizes them using a specialized model
Pormalization-LLMMeeee Evolves NL problems, then formalizes them using general-purpose LLM (Gemini-2.5-Pro) in zero-shot setting.
Formalization-LLLL
The same as above, but a few-shot setting.
Starting with 400 seed problems, we generated an equal number of candidates using each method and passed them through stringent verification pipeline. The number of successfully verified
8

---

Published as a conference paper at ICLR 2026
Comparison Evolution Methods
Methods
Tormalication- Formalizer
Formalization- LLM 2emm-shat
Formalization LLM few shot
Evolifficitt
210
661
Count
300
Method
Figure 4: Comparison of the number of candidates passing verification for four evolution methods. Our EvolDomain & EvolDifticulty performs best.
statements for each method is shown in Figure 4. Our direct evolution approach significantly outperforms all NL-based methods, confirming its superiority. The final candidate count can exceed 400 each seed may yield multiple valid variants. Additionally, quality of 1,63 1,634 data with EvolDomain and EvolDifficulty using DeepSeek- V3.1 Among them, 496 statements failed verification, corresponding semantic failure rate of 30.35%.
directly evaluated the semantic
Domain Diversity. Here, analyze how framework improves domain diversity and how this enhancement translates to performance gains. Figure illustrates the effect of EvolDomain on sample of 200 seed problems. The initial distribution is heavily skewed. with domains like Algebra dominating while others like Calculus are absent. After applying EvolDomain, the dataset becomes significantly more balanced: the share of over-represented domains is reduced, and previously missing categories are introduced. The domains for both sets were classified by DeepSeek-V3 and human-verified.
This improved diversity directly leads to better model performance across various domains, as detailed Table 3. Comparing EvolProver against the EvolProver-Baue bascline, our full model achieves gains across most categories. Critically, it makes breakthrough in Calculus, solving problems where the baseline solved These results confirm that our strategy not only enriches domain diversity but also enhances the model's 'ss overall mathematical capabilities.
Similarity. Additionally, we investigate whether the evolution process leads to the training data containing more samples similar the test sets. To this end, we conduct analysis the MiniF2F- Test, FormalMATH- and Ineq-Comp test sets. We use each test sample as query and employ the saate-oftthe-aee embedding model @wwen--Embedding 8B retrieve its top-I most similar sample
Domain Distibbtion 57.55
Domain Distribution
Algebra: 20.1%
Theory: Discrate Mathematics 10.0%
Number Theory:
Sequences Series 15.4%
Calculus: 3.5%
Distrete Matheratics: 34.3%
Sequences
Geometry: 7.2%
Geametry. 2.0%
Calculus: 6.8%
Precalculus: 1.0%
Differentiatien: 5.2%
Differentiation: 0.0%
Multivariable Calicllus: 0.0%
Others: 3.1%,
Integral: 0.0%
Precalculus: 2.3%
Appliad Mathematica: 0.0%
Integrat Applied Matheraatis:: 1.8%
Others: o. 8%%.
Evolution Distribution
Evolution. Distribution
Figure Comparison of Mathematical Domain Distribution Before and After EvoiDomain.

---

Published as a conference paper at ICLR 2026
Table Number of proved problems FormalMATHH-Liee benchmark in different domains under 32 generation trials. EvolProver improves upon EvolProver- across most domains.
Domain
EvolProver-Base
EvolProver
Total
Algebra
121
141 (+20)
235
Applied Mathematics
28
33 (+5)
Number Theory
16
(+7)
45
Precalculus
15 (+1)
23
Geometry
7
(+1)
17
Discrete Mathematics
2
5 (+3)
25
Calculus
0
3 (+3)
Multivariabll Calculus
2
(-)
Others
0
0 (-) 23
Table 4: Ablation experiment results on the FormalMATH-Lice benchmark, the MiniF2F- benchmark, and the Ineq-Comp benchmark. All results are pass@32 rate. Superscripts denote the training data used: superscript' for Public dataset only; superscript for Public dataset + EvolDomain EvolDifficulty augmentation; superscript for Full augmentation including Public dataset, EvolDomain & EvolDifficulty, and EvoIAST. SeaProvvr-Ablationn trained through a sole SFT stage. EvolProver- Base, EvolProver-Ablation RL and EvolProver are trained through SFT stage and an RL stage.
and Evoler-SFT are
Ineq-Comp (Seed)
Ineq-Comy (Transformed)
Ineq-Comp (Ratio)
Models
ForMalMATH
MiniF2F
EvolProver-Baad Base
44.71%
52.05%
43.26%
14.89%
34.43%
EvelProver-Ablation
50.35%
65.16%
49.79%
29.19%
58.62%
EvolProver-SFT 0+1+2
51.53%
66.39%
49.82%
30.35%
60.19%
ExolPrower-AAbltionn-R
51.98%
68.22%
50.36%
33.05%
65.62%
EvolProver
53.96% %
69.80%
52.20 %
34.02%
65.17% %
from our final training data. These paired theorems are then evaluated by DeepSeek-V3. for human- like similarity assessment. We instruct the model to score each pair on a scale from to 10, where 1 denotes "completely dissimilar" and 10 denotes "semantically identical." The evaluation results show that the average similarity score of these pairs is about 3.48, indicating that even among the most syntactically and semantically similar samples between the training and test sets, the overall similarity remains quite limited. Further details are provided in Appendix A.7.
Ablation Experiments. To further validate the effectiveness of our proposed methods, we conduct series of comprehensive ablation studies. The results presented in Table 4. These experiments isolate the impact of each component and demonstrate that they provide consistent benefits across multiple benchmarks and at various training stages. In addition, we analyze the mathematical domains of the problems in the FormalMATH-Lite benchmark based on these ablation experiments. Experimental details are provided in Appendix A.2.
CONCLUSION AND FUTURE WORK
In this paper, we introduced a highly-extensibe data augmentation pipeline with three methods: EvolDomain, EvolDifficulty, and EvolAST, designed to improve model generalizability from semantic and syntactic perspectives. Our resulting model, EvolProver, achieves new SOTA results on several key benchmarks, notably surpassing all comparable models on FormalMATH-Lite. For future work, we plan to enhance EvolProver's s reasoning capabilities by incorporating synthetically generated Chain-of-Thouu data into its training.
10

---

Published as a conference paper at ICLR 2026
REPRODUCIBILITY STATEMENT
We are strongly committed to the reproducibility of our work. Our EvolAST method is designed to be highly extensible, and encourage the community contribute by expanding its set of applicable axioms and theorems.
ACKNOWLEDGMENT
This work was supported by Ant Group Research Intern Program, and National Natural Science Foundation of China Young Scientists Fund (No. 62206233).
REFERENCES
Authropic. Introducing claude 4, May 2025. URL http://ss//ww.aatttoootcccc////s Accessed: 2025-07-28.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, -han-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, and et al. The Coq Proof Assistant Reference Manual: Version 6.1. Inria, 1997. Version 6.1.
Chuxue Cao, Mengze Li, Juntao Dai, Jinluan Yang, Zijian Zhao, Shengyu Zhang, Weijie Shi, Chengzhong Liu, Sirui Han, and Yike Guo. Towards advanced mathematical reasoning for Ilms via first-order logic theorem proving, 2025. URL https: http:///axvvvvvooo htrrg/bbs2006... 17106 17104.
Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, and Yike Guo. Pushing the boundaries of natural reasoning: Interleaved bonus from formal-logic verification, 2026. URL 22642.
DeepSeek-AL Deepseek-v3 technical report, 2025. URL httth:://aaaiiii wwtpiiv..orgbbb//24//
Kefan Dong and Tengyu Ma. Stp: Self-play Ilm theorem provers with iterative conjecturing and proving. arXiv preprint vrXiv:2502.00212. 2025.
Yuren Hao, Xiang Wan, and Chengxiang Zhai. investigation of robustness of Ilms mathe- matical reasoning: Benchmarking with mathermatically-cquivvaae transformation of advanced mathematical problems, 2025. URL httpps://arat http://aaxvvv.orr/////////// 08833.
Kaixuan Huang, Jiacheng Guo, Zihao Li, Xiang Ji, Jiawei Ge. Wenzhe Li, Yingqing Guo, Tianle Cai, Hui Yuan, Runzhe Wang. Yue Wu, Ming Yin, Shange Tang. Yangsibo Huang, Chi Jin, Xinyun Chen, Chiyuan Zhang, and Mengdi Wang. Math-perturb: Benchmarking Ilms' math reasoning abilities against hard perturbations, 2025. URL hntps://aaxx org/abs http/////2500 2502. 06453.
Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai. Leanahell- Verifier-integrated reasoning for formal theorem proving via reinforcement learning. arXiv preprint arXiv:2507.0nm 08649, 2025.
Xueying Jiang, Jiaxing Huang, Sheng Jin, and Shijian Lu. Domain generalization via balancing training difficulty and model capability, 2023. URL
00844.
Sirui Li, Wangyue Lu, Xiaorui Shi, Ke Weng, Haozhe Sun, Minghe Yu, Tiancheng Zhang, Ge Yu, Hengyu Liu, and Lun Du. Msc-1800 A benchmark for automated formal theorem proving from mathematical subject classification, 2025. URL htt.:/tpss//axxi..orr//aa/////// 28222
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Scaling formal theorem proving with scaffolded
Jiawei Ge, Jingruo Sun, et data synthesis and self-correction. arXiv preprint arXiv:2508.0300 2025.
Wangyue Lu, Lun Du, Sirui Li. Ke Weng, Haozhe Sun, Hengyu Liu, Minghe Yu, Tiancheng Zhang, and Ge Yu. Automated formalization via conceptual retrieval -ageeveeeeemeeeted Ilms, 2025, URL www.aaawww..oog......aa/aaaaa 06931.

---

Published as a conference paper at ICLR 2026
Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, Yansong Tang, and Dongmei Zhang. Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct, 2025a. URL http:://arxiv.rrg/bb///Be 09583..
Jinghao Luo, Yuchen Tian, Chuxue Cao, Ziyang Luo, Hongzhan Lin, Kaixin Li, Chuyi Kong, Ruichao Yang. and Jing Ma. From storage to experience: A survey on the evolution of Ilm agent memory mechanisms. Preprints, January 2026. doi: 220944//prepiims22200........ org/10. 20944/preprints2222666 00000206610661..... 8618.v2.
URL
https://doi.
Ziyang Luo, Can Xu, Pu Zhao, Qingfeng Sun, Xiubo Geng, Wenxiang Hu, Chongyang Tao, Jing Ma, Qingwei Lin, and Daxin Jiang. Wizardcoder: Empowering code large language models with evol-instruct, 2025b. URL
/rg.//////////////// 08568.
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction CADE 28, pp. 625-635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-55
Shubham Parashar, Shurui Gui, Xiner Li, Hongyi Ling, Sushil Vemuri, Blake Olson, Eric Li, Yu Zhang, James Caverlee, Dileep Kalathil, and Shuiwang Ji. Curriculum reinforcement learning from easy to hard tasks improves IIm reasoning, 2025. URL 06632.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 Lecture Notes in Computer Science. Springer Berlin, Heidelberg, 1994. ISBN 978-3-540-58244-1. doi: 10.1007/ 3-540-58244-0.
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-tee Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.2181. 2025.
Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hu Chen, Jie Yan, and Xiangyu Zhang. dhepfun-prove preview: Let's think and verify step by step. arXiv preprint arXiv:2557.20115 2025.
Yuchen Tian, Weixiang Yan, Qian Yang, Xuandong Zhao, Qian Chen, Wen Wang. Ziyang Luo, Lei Ma. and Dawn Song. Codehalu: Investigating code hallucinations 1lms via execution-based verification, 2025. URL https:
//gg//bb//25555 00253.
Haiming Wang. Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung. Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Preyfus-Schhiiee Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang. Zhengying Liu, and Jia Li. Kimina-prove preview: Towards large formal reasoning models with reinforcement learning. 2025a. URL https: //axivi wog.orggaaao.. abt 2504. 11354.
Haiming Wang. Mert Unsal, Xiaohan Lin, Mantas Baksys. Junqi Liu, Marco Dos Santos, Flood Sung. Marina Vinyes, Zhenzhe Ying. Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Preyfus-Schmitt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang. Zhengying Liu, and Jia Li. Kimina-prover: Applying test-time rl search large formal reasoning models. Hugging Face htt//kiiiaaaaovveee
Community Blog. 2025b. URL https: / http//uuggnngfffeee
Zijian Wu, Suozhi Huang. Zhejian Zhou, Huaiyuan Ying. Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2.55stepprre Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024. URL http:///axxx//aaaaaaae
15700.
12

---

Published as a conference paper at ICLR 2026
XAI. Grok code fast 1. http:://x.a//neessgrrror-ooo---. August 2025. Accessed: 2025- 08-26.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover, Advancing theorem proving in Ilms through large-scale synthetic data. arXiv preprini arXiv:2405. /4333, 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang. Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-provers 5: Hamnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024b.
Ran Xin, Chenguang Xi, Jie Yang. Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for 1im-ased automatic theorem proving, 2025a. URL https://arxiv org/ abs/
aww.ab////.. 2502. 03438.
Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, and Xia Xiao. Scaling up multi-turn off-policy rl and multi-agent tree search for Ilm step-provers, 2025b. URL /ttpps:/arriiie http:/awwiv.r..r/a//////e/ra// org/abs/2509 06493.
Can Xu, Qingfeng Sun, Kai Zheng, Xiubo Geng, Pu Zhao, Jiazhan Feng, Chongyang Tao, Qingwei Lin, and Daxin Jiang. Wizardlm: Empowering large pre-trained language models follow complex instructions. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, 2024. URL https: httpt: htttps://opeerrvieew..e Forum?id=CfXh93NN
Weixiang Yan, Yuchen Tian, Yunzhe Li, Qian Chen, and Wen Wang. Codetransocean: A comprehen- sive multilingual benchmark for code translation, 2023, URL https: 04951.
Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models, 2024. URL https://arxiv, wrg./bb/////....o./ 12284.
Zhouliang Yu, Ruotian Peng. Keyi Ding, Yizhe Li, Zhongyuan Peng. Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, al. Formalmath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint arXiv:2505.02735, 2025.
Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. ceanabell-prover Posttraining scaling in formal reasoning. arXiv preprint orXiv:2504.06122 2025.
Haoyu Zhao, Yihan Geng, Shange Tang, Yong Lin, Bohan Lyu, Hongzhou Lin, Chi Jin, and Sanjeev Arora. Ineq-comp:
Benchmarking human- intuitive compositional reasoning in automated theorem proving on inequalities. arXiv preprint arXiv:2505. 12680, 2025a.
Xueliang Zhao, Wei Wu, Jian Guan, and Lingpeng Kong. Promptcot: Synthesizing olympiad-level problems for mathematical reasoning in large language models, 2025b. URL attps://arxxt org/abs/2503. 02324.
Da Zheng, Lun Du, Junwei Su, Yuchen Tian, Yuqi Zhu, Jintian Zhang, Lanning Wei, Ningyu Zhang, and Huajun Chen. Knowledge augmented complex problem solving with large language models: A survey, 2025. URL http::://aaxiii.rrg/////////// org. 2505. 03418.
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematies. arXiv preprint arXi::2109.00// 10, 2021.
13

---

Published as a conference paper at ICLR 2026
A APPENDIX
A.1 DETAILS OF TRAINING EVOLPROVER
Data Curation. Our data curation process follows multi-stage funnel. We begin with a seed pool of approximately 3.3 million verified formal statements aggregated from four sources: DeepSeek- Prover-V1, STP-Iean, MiniF2F-Valid and FormalMATH-AII (excluding the FormalMATH-Lite subset).
From this pool, we sample 70k statements for evolution. These initial 70k samples are carefully curated from our four sources. Three of the -eeesetss--eSSSSee--PPe- Prover-V1, FormalMATH--Al (ex- cluding FormalMATH-Lite), and MiniF2F-Valiin containing just over 30,000 theorems, and we include all theorems from these valuable sources in synthesis pool. The fourth source, STP-Ican, is much larger synthetic dataset with 3.26 million theorems; to prevent this synthetic data from dominating the more curated sources and to avoid excessive computational costs, first filter out theorems originating from ma mathlib ib and then perform a weighted sampling over the remainder to select an additional 30,000+ examples, guided by the importance weights provided by the STP--lean authors. The number of sampled examples is chosen to be comparable to the total size of the other weal-world datasets combined, yielding a high-quality and diverse seed set of 70k theorems in a cost-effective manner, balancing valuable real-world problems with broader set of synthetic examples. These are processed by our EvolDomain and EvolDifficulty methods using Gemini-2.5-PP and DeepSeek-RI R1, which then undergo a verification process to yield 57.4k high-quality (statement, description) pairs. This verification first involves a syntax check using the Lean 4 compiler; if the compiler finds a syntax error, we use DeepSeek-V3 V3 (DeepSeck-AI. 2025) to repair it, after which DeepSeek-V V3 performs final semantic check. Next, we apply EvolAST to this set for syntactic diversification, expanding it to approximately 96.7k entries (as a single statement generate multiple AST variants). Finally, generate proofs for each statement. 1B and Goedel-Provve--22--1
are high-quality but relatively small, collectively
as expert models, we generate 50 proof candidates per statement and retain only those that pass Lean 4 compiler verification. After removing duplicates, this process results in a final training dataset of 39.2k unique (statement, proof) pairs. Thus, our 39. 2k training data are synthesized from this carefully curated 70k- 70k-theorem seed set. To prevent data leakage, we ensure that the initial states of all theorem statements in our data are different from those in the tested benchmarks.
Using PerSSeee-Prove--222
Token Cost. Our data construction can be divided into four stages: EvolDomain & EvolDifficulty, Verification process, EvolAST, and Proof synthesis. We counted the token cost for each stage as follows:
Stage
Token Consumption
Problem synthesis (EvolDomain & EvolDifficulty) Verification process
893M
506M
EvolAST Proof synthesis
0
11B
Supervised Fine Tuning. We fine-tune the Beeeeeek-Prov----...
model using full-parameter
supervised fine-tuning (SFT). Our training data includes approximately 3.3M theorems with proofs from public datasets and 39.2K theorems with proofs from the augmented datasets. The model is trained for one epoch with the AdamW optimizer. We set the initial learning rate to 1.0 x 10-5 and decay using cosine scheduler with 5% warmup ratio. All sequences are truncated a maximum length of 4096 tokens, and use global batch size of 32.
Reinforcement Learning. Following the Supervised Fine-Tuning (SFT) stage, we further enhance the model's performance by applying Reinforcement Learning (RL) to the SFT checkpoint. For RL training. For RL training, we use augmented data (39.2K) and additionally incorporate FormalMATH- All (excluding FormalMATH-Lite) and MiniF2F- Valid into our training data. We employ a standard binary reward: for each problem. the model receives a reward of if the generated Lean proof is correct, and 0 otherwise. This RL. fine-tuning process produces the final EvolProver.
14

---

Published as a conference paper at ICLR 2026
Table 5: Domain-wise performance of EvolProver variants,
Domain
EvolProver Base EvolProver Ablation SFT EvolProver SFT EvolProver Ablation RL EvolProver
Algebra
121
133
134
133
141
Applied Mathematics
28
30
32
32
33
Number Theory
21
23
23
23
Precalculus
15
15
15
Goometry
Discrete Mathematics
3
Calculus
2
Multiarrable Calculus
2
2
Others
0
RL Training Details To improve training efficacy, curate the RL training dataset by filtering problems based on the pass@ I success rate of the SFT checkpoint. We include only problems where pass@1 1/2. This selection strategy ensures that the training set is challenging yet solvable for our model. The filtered dataset contains 2,718 problems. We initialize both the actor and critic models with the weights from the SFT checkpoint and train them using Proximal Policy Optimization (PPO). The training runs for 10 epochs with batch size of 256, a constant actor learning rate of 1.0 10 6 a constant critic learning rate of 1.0 x 10m5, a clip ratio of 0.2, and KL divergence loss coefficient of 0.001.
A.2 ABLATION EXPERIMENTS
A.2.1 ABLATION MODEL TRAINING
To precisely evaluate the contribution each component, we trained series of ablation models under controlled conditions. All training hyperparameters were kept identical across corresponding stages. The models are:
EvolProver-Base Our baseline, trained on the original, unaugmented public dataset through both SFT and RL stages.
ExolProver-ADaationnS:::: Trained data augmented only by EvolDomain and EvolDiffi- culty, and only undergoes the SFT stage.
CrolProver-Ablation-ee Same data as above (EvoiDomain and EvolDifficulty only), but undergoes the full SFT and RL training process. This model directly isolates the impact of EvolAST when compared to the final EvolProver.
EvolProver-SFT: The checkpoint of our final model after being trained on the fully aug- mented dataset (including EvolAST) for the SFT stage only.
We did not create an "EvoLAST-only" model, as EvolAST operates on the output of EvolDomain and EvolDifficulty, making such an experiment logically infeasible.
A.2.2 ABLATION EXPERIMENT RESULTS
The results of our ablation experiments, presented in Table 4, lead to two key conclusions. First, data augmentation provides a substantial boost, with even the partially augmented models (Ablation- SFT/RL) drastically outperforming the EvolProver Base model across all benchmarks, often by more than 10%. Second, the EvolAST method consistently yields further improvements across all benchmarks. In the SFT stage, EvolProver-SFT (with EvolAST) surpasses EvolProver Peeeroover-blatiooo-. (without EvolAST), Similarly, the RL stage, the final EvolProver outperforms EvolProver-Ablation RL. This demonstrates the value of the EvolAST method in both training phases.
To better understand how each augmentation component affects performance across mathematical domains, we conduct fine-grained analysis and report the results in Table 5. This breakdown allows us to examine the domain-specific behaviors of different model variants and how they interact with data scale and difficulty. The detailed analysis is as follows:
For EvolProver-Ablate Ablation-SFFT which retains only EvolDomain and EvolDifficulty, perfor- mance improves over EvolProver-Baan Base in almost all domains. The relative gains differ
15

---

Published as a conference paper at ICLR 2026
across domains and correlate with data scale. In long-tail domains with relatively sparse training data, the main improvements are associated with EvolDomain: by performing cross- domain semantic evolution, it transfers structural patterns from high high-resource domains and effectively increases coverage in low-resource domains. high-resource domains where the base model already captures the main solution patterns, EvolDiffieuly contributes more prominenty: by broadening the difficulty distribution of training problems, it encourages the model to handle a wider range of problem difficulty. Overall, these results indicate that EvolDomain primarily mitigates data scarcity in low-resource domains, while EvolDifficulty mainly enhances robustness varying difficulty levels in high-resouree domains, and the two components play complementary roles across different data scales.
EvolProver-SFT is obtained by further incorporating EvolAST on top of EvolProver- Ablation-SIFT. Relative to Ablation-SFT,, which uses only EvolDomain and EvolDifficulty, EvolProver-SFT yields small but consistent additional gains in domains with larger pro- portion of symbolic reasoning, such as algebra, number theory, and applied mathematics (for example, Algebra improves from 133 to 134, Applied Mathematics from 30 to 32, and Number Theory from 21 to 23), while performance other domains remains essentially unchanged. This pattern suggests that EvolAST does not primarily introduce new semantic content. Instead, by generating multiple equivalent structured representations for the same reasoning process, EvolAST strengthens the model'ss ability handle different surface forms with the same underlying meaning, leading to additional generalization benefits in high-resource domains that already have substantial sample size and semantic diversity.
EvolProver-Ablation-RI is produced by applying reinforcement learning top of ProlProver-Ablation- using data generated by EvolDomain and EvolDifficulty. Com- pared with EvoIProver-SFT, performance in high-resource domains (such Algebra, Ap- plied Mathematics, and Number Theory) remains largely stable, whereas additional gains srgger-seacch-space domains (for example, Discrete
appear in sparser, more difficult, Mathematics increases from 3 to 5 and Calculus from 2 to 3). These observations indicate that, under data distribution shaped by cross-domain coverage and difficulty evolution, reinforcement learning can make fuller use of the evolved samples through exploratory optimization, particularly in domains where search and exploration are more challenging.
The final EvolProver model performs reinforcement learning the full dataset that includes all three augmentations: EvolAST, EvolDomain, and EvolDifficulty. Relative to EvolProver- Ablation-RL, EvolProver achieves further improvements in high-resource domains such as Algebra (from 133 to 141) and Applied Mathematics (from 32 to 33), while preserving the gains already observed in Discrete Mathematics (5) and Calculus (3). Taken together, these results support the view that the three augmentation components act along complementary axes domain coverage, difficulty distribution, and structural diversity and that combining them within both supervised fine-tuning and reinforcement learning leads to more robust and broadly improved domain-wise wise performance.
16

---

Published as a conference paper at ICLR 2026
A.3
DETAILS FOR EVOLDOMAIN
A.3.1 PROMPT TEMPLATE
Formal problems can precisely extract the universal logical skeleton of a mathematical pCo et al., 2025; 2026; Zheng et al., 2025). Our strategy leverages this by transferring that structure to new domains to systematically create rigorous new problems. Our preset domains cover a range of topics from high school competition problems to undergraduate-level subjects. The prompt template format of EvoiDomain as follow:
Prompt Template for EvolDimain
Your task is to start with a given Lean 4 formalized problem and follow the strategy below to formulate problem in different mathematical domain.
### Transformation Strategy
Step Deconstruction & Abstraction
Identify the original statement's abstract logical skeleton by isolating its core components. This involves recognizing the underlying mathematical objects, the essential operations being performed, and the fundamental relationship being asserted.
Step 2. Analogy & Transfer
Find parallel structure in new mathematical domain by identifying analogous sequence objects in the list below.
["Algebra", "Number Theory", "Integral", "Precalculus", "Differentiation" "Multivariable Calculus", "Sequences Series", "Applied Mathematics", "Discrete Mathematics", "Geome- try". "Calculus", "Other"] Then, translate the original operations and relations into concepts that are natural within this new context.
Step 3. Instantiation Packaging
Formulate a new, concrete problem by applying the transferred structure and opera- tions to the analogous objects. Package this proposition into clear natural language description and a rigorous formal statement.
Evolved variants should follow the following requirements:
Each variant should be mathematically rigorous and meaningful
2. Each variant should be syntax correct and a valid Lean 4 statement Each variant should differ from the original mathematical domain
4. Each variant should follow the same output format as "### Example Variant Format"
### Example Variant Format:
NL Description
Prove that
Formal Statement
by sorry
Domain
Target Domain in the list
Please provide 3-5 variants following the strategies and requirements above, based on original statement.
17

---

Published as a conference paper at ICLR 2026
### Original Formal Statement
"lean4
{Original Formal Statement)
### Evolution Results (3-5 variants in other mathematical domains)
A.3.2 CASE STUDY
We select an example of EvolDomain from the evolved dataset. The original Lean 4 statement is as follows:
Original Lean 4 Statement (Number Theory)
theorem Bean_workbook_11 12211 (m,, n Z) (h_1 sorry
2xm
3m3 3 by
The evolved Lean 4 statement and its corresponding natural language description are as follows:
Evolved Statement and its corresponding Natural Language Question (Geometry)
Evolved Formal Statement:
theorem wttee_poitss__aaalloooe Q) 0) dist
EuclideanSpace R (Fin 2)) (h (2 (Q P)) dist P R
by sorry
Natural Language Question:
Consider three points 'P", "Q", and "R" in plane. If the vector from to "R" added twice the vector from "p" to "Q" results the zero vector, prove that the squared distance from "P" to "Q" is not equal to the squared distance from "p" to "R" minus 15.
Evolved Statement and corresponding Natural Language Question (Integral)
Evolved Formal Statement:
theorem integral_ variiann__
(f + R)
(hf ContinuousOn ICe 1))
(hg ContinuousOn g Icc 1))
(h_f_nonneg
th_f_not_zere E Set. 1, f x 2 0)
Set.Icc 0 1, f # 0)
(h_1 V Set.Icc 0 1, x f + x=
in (0).. (f 33 f in (0)..1, (g x)x3 15 by sorry
Natural Language Question:
Prove that for any two real-valued continuous functions, " and "g", defined
interval '[o, 13", if is nonnnega not identically zero, and if 22 f(x) g(x) 0- for all "x" in [Q. 1]", then the integral of -f(x) "3"
over [[O 1] is not equal to the integral of "g(x) over "[O 1]" minus 15.
A.4 DETAILS FOR EVOLDIFFICULTY
To generate problems of varying difficulty, we define a set of evolution strategics through deliber- ation and screening by team of mathematies experts. These strategies fall into two categories:
18

---

Published as a conference paper at ICLR 2026
upward (to increase difficulty) and downward (to decrease difficulty), each with specific methods for implementation.
A.4.1 UPWARDEVOLUTIOO
The prompt tempalte for upward evolution is as follows:
Prompt Template for EvolDifficulty (Increase Difficulty)
Your task is to evolve a given formal statement into several, more complex formal statements, according to the provided strategies and requirements. For each new formal statement, you must provide its corresponding natural language meaning.
### Difficulty Enhancement Strategy
Your objective is to (strategy) for the original statement.
First, understand the core concept and structure of the original formal statement. Identify its key logical components, such as variables, propositions, logical operators, quantifiers, conditions, and the overall scope. Then, you can select from range of strategies, including but not limited to the following, to enhance difficulty: {Specific Methods}
### Evolution Requirements
Evolved variants should follow the following requirements:
Each variant must represent a genuine enhancement its proof's logic and difficulty, not just increase in superficial complexity.
2. Each variant should be mathematically rigorous and meaningful
Each variant should be syntax correct and valid Lean 4 statement
4.
Each variant should be different from the original statement and other variants
Each variant should follow the same output format as "### Example Variant Format".
### Example Variant Format:
"L. Description
Prove that
Formal Statement
by sorry
Please provide 3-5 variants following the strategies and requirements.
### Original Formal Statement
lean4
(Original Formal Statement]
### Evolution Results (3-5 variants with increasing difficulty)
The strategies and specific methods are as follows:
Strategics and Specific Methods (Increase Difficulty)
Complicate the Logical Structure
problem that increases the nesting depth and layers of the original problem's 's propositional logic.
(1) Construet
(2) Construct problem by introducing logical system with complex dependencies
between its components.
(3) Construct a problem whose internal structure is obscured by multiple layers of
19

---

Published as a conference paper at ICLR 2026
non-obvious equivalent transformations.
Increase the Mathematical Depth
(1) Construct a new problem that relies on deeper theoretical framework.
(2) Construct a new problem that requires longer, but logically similar, chain of reasoning to solve.
(3) Construct a new problem that positions the original problem as critical sub-problem or lemma within its proof.
3. Elevate Abstraction and Generalization
(1) Construct a new problem by elevating and generalizing a specific instance or special case from the original problem into universal proposition that must be proven.
(2) Construct new problem that adds stricter conditions, requiring reasoning and verification under them.
(3) Construct a new problem whose proof requires the fusion of concepts or tools from different knowledge domains.
Intensify Constraints and Precision
(1) Construct new problem that increases complexity by establishing critical boundaries or singularities within the problem's 's domain.
(2) Construct new problem that adds specific, strong constraints, requiring the discovery of an optimal solution or an extremal state.
(3) Construct new problem with heightened rigor requirements, making it necessary to provide a strict argument for the existence, uniqueness, or enumeration of the solution(s).
5. Add Parametric and Analytical Complexity
(1) Construct new problem that broadens the hypothesis space and increases analytical complexity by introducing or adjusting explicit parameters.
(2) Construct new problem whose internal structure spans both discrete and continuous forms, requiring a transformation between them (e.g., the limit relationship between sum and an integral) to be solved.
A.4.2 DOWNWARDEVOLLTION
The prompt template for downward evolution is as follows:
Prompt Template for EvolDifficulty (Decrease Difficulty)
Your task to evolve a given formal statement into several, simpler formal statements, according the provided strategies and requirements. For each new formal statement, you must provide its corresponding natural language meaning.
### Difficulty Reduction Strategy
Your objective is to (strategy) for the original statement.
First, understand the core concept and structure of the original formal statement. Identify its key logical components, such as variables, propositions, logical operators, quantifiers, conditions, and the overall scope. Then, you can select from range of strategies, including but not limited to the following, reduce difficulty: (Specific Methods}
...
### Evolution Requirements
Evolved variants should follow the following requirements:
Each variant must represent a genuine simplification of its proof's logic and structure, not
just cosmetic rephrasing.
2. Each variant should be mathematically rigorous and meanigful
Each variant should be syntax correct and valid Lean 4 statement
20

---

Published as a conference paper at ICLR 2026
4. Each variant should be different from the original statement and other variants
5. Each variant should follow the same output format as "#### Example Variant Format".
### Example Variant Format:
NL Description
Prove that...
Formal Statement
= by sorry
Please provide 3-5 variants following the strategies and requirements.
### Original Formal Statement
lean4
[Original Formal Statement]
### Evolution Results (3-5 variants with decreasing difficulty)
The strategies and specific methods are as follows:
Strategies and Specific Methods (Decrease Difficulty)
1. Simplify the Logical Structure
(I) Construct a new problem that decreases the nesting depth and layers of the proposition's logic.
(2) Construct new problem containing logical system with weaker or no dependencies
between its components.
(3) Construct a new problem whose internal structure is transparent, solvable through direct
logical relations rather than non-obvious transformations.
Reduce the Mathematical Depth
(1) Construct a new problem that relies on more elementary theoretical framework.
(2) Construct a new problem that only requires completing the initial steps or the final conclusion of the original problem's longer reasoning chain.
(3) Construct a new problem by isolating key lemma or an intermediate step from the original problem's 's proof and setting the sole objective.
3. Reduce Abstraction and Specialize
(1) Construct a new problem by taking a general or abstract proposition and creating a specific, concrete instance of be solved verified.
(2) Construct a new problem that replaces abstract symbols and variables with concrete numerical values tangible examples to lower the barrier understanding.
(3) Construct a new problem by reformulating it so that it can be solved using concepts and tools from single, self-contained knowledge domain, avoiding interdisciplinary fusion.
Loosen Constraints and Precision
(1) Construct new problem by restricting its domain to regular cases, excluding critical boundaries or singularities.
(2) Construct
problem that requires finding any feasible solution rather than optimal or extremal one.
(3) Construct new problem that asks for single conerete example of solution, rather than
a rigorous proof its existence, uniqueness, or enumeration.
5. Reduce Parametric and Analytical Complexity
(1) Construct new problem that reduces the dimension of analysis by reducing the
21

---

Published as a conference paper at ICLR 2026
number of variables required address the problem by simplifying complex functional relationship between parameters to a linear one.
A.4.3 CASE STUDY
We select two examples of EvolDifficulty from evolved dataset. The original Lean statement for upward evolution is as follows:
Original Lean 4 Statement for Upward Evolution
theorem 1ean_workbookk37422 (n N) 133
11* 12" 12" (2*n+1) := by sorry
The evolved Lean 4 statement and its corresponding natural language description are follows:
Evolved Statement and corresponding Natural Language Question (Inerease Difficulty)
Evolved Formal Statement:
theorem variant_1 (n:N) 133 Nat.ged (n+2()+2) 12" (2sn+1)) (11" ((n+1)+2) 12" (2*(++1)+1) := by sorry
Natural Language Question:
Prove that any natural number n, the greatest common divisor of (1*())))
4 12" 12" (2*n+1) and 11 ((*+1)+)++) 12 (2*((2++))+1) is divisible by 133.
Evolved Statement and its corresponding Natural Language Question (Increase Difficulty)
Evolved Formal Statement:
def u_seq N -
8 => 133
1 => 3059
k + 2 155 * s_seq (k 1) 1584 s_seq k
theorem variant_2
133 u_seq by sorry
Natural Language Question:
integer sequence u defined by 133, 3059, and the recurrence
relation (_(n+ 155 u_(n+1> 1584 u.n for all n 2 0. Prove that every term u_n of the sequence is divisible by 133.
The original Lean 4 statement for downward evolution is as follows:
Original Lean 4 Statement for Downward Evolution
theorem workbookkk 21498 (a b R) (ha 0 < a) (hb 0 < b) (a + b) / Real. sqrt b + b Real. by sorry
(a + b) 2
22

---

Published as a conference paper at ICLR 2026
The evolved Lean 4 statement and its corresponding natural language description follows:
Evolved Statement and its corresponding Natural Language Question (Decrease Difficulty)
Evolved Formal Statement:
theorem variant_ (a, b. RR) (ha S a) (hb 0 < b) (Real.sqrt a + Rqal.sqrt
b) 2 (a + b) = by sorry
Natural Language Question:
Prove that for any non-negative real numbers "a" and "b", the square of the sum of their square reats is less than or equal to twice their sum.
Evolved Statement and its corresponding Natural Language Question (Decrease Difficulty)
Evolved Formal Statement:
theorem variant_2 (a, b IR) (ha a) (hb b) (a b) / 2 2 Real. sqrt (a
b) by sorry
Natural Language Question:
Prove that Ari thmetic Mean Geomerrii Mean (AM-GM) inequality for two positive
real numbers and "b", which states that their arithmetic mean greater than or equal to their geometric mean.
A.5 DETAILS FOR VERIFICATION
The prompt template to judge consistency between natural language problem and formal statement is as follows:
Prompt Template Judge Consistency
You will be provided with a Natural Language Description and Formal Statement. Please judge if they are consistent, and provide specific analysis:
Natural Language Description:
Problem
[Natural Language Description}
Formal Statement:
lean4
[Formal Statement]
For your response, please follow this example format:
# **Consistency Analysis:**
anallsis
Your detailed analysis
**Judee *e
jjudge
Consistent or Inconsistent
Now, please provide your formal answer:
23

---

Published as a conference paper at ICLR 2026
The prompt template to judge mathematical correctness of formal statements and natural language problem is as follows:
Prompt Template Judge Correctness
You will be provided with a Natural Language Description and a Formal Statement. Please judge if the mathematical statement is correct, and provide specific analysis:
Natural Language Description:
Problem
(original nl}
Formal Statement:
lean4
[correct formal statement]
Please analyze the mathematical correctness by considering:
1. Whether the problem is provable (can be proven disproven) Whether the problem statement is well-formed and meaningful
3. Whether there any logical contradictions or inconsistencies
For your response, please follow this example format:
** Matthmmatical Correctness Analysis:*#
analysis
Your detailed analysis
**Judge Result:**
judge
Correct Incorrect
Now, please provide your formal answer:
The prompt template for filtering out low-difficulty problems is as follows:
Prompt Template for Filtering Out Low-diffieulty Problems
You will be provided with Natural Language Description and Formal Statement, Your task is to classify the difficulty of problem in Lean 4:
Natural Language Description:
Problem
[Natural Language Description)
Formal Statement:
>> *elnn
[Formal Statement]
Please analyze the problem and determine if it Low-difficulty. Here are the criteria for Low-difficulty problem:
1. Simple calculations
Simple algebraic manipulations
3. Solving single variable linear equations (by just 1-step calculation) Inequalities proved by an easy sum-of-squue -f-suuurssssss technique
24

---

Published as a conference paper at ICLR 2026
Conversely, the following types of problems should NOT be classified as Low-difficult:
1. Inequality proving with the square root (might be more complex)
More complex inequalities, limits, and integrals
3. Problems dealing with integers (more related to number theory)
Problems involving higher order roots, complex numbers, matrices, polynomials, group, finite-uum, functional equations (since these might shed lights on other hard problems)
For your response, please follow this example format:
**Difficltyy Analysis:**
analysis
Your detailed analysis
**Judge Result:**
Is Low-difficulty:
"judge
Yes or No
Now, please provide your formal answer:
Prompt template for fixing compilation errors in a formal statement is as follows:
Prompt Template for Correcting Formal Statement
Your task is to fix the code based the errors and provide corrected version. Please also provide a detailed analysis of the changes you made. You will be provided with an incorrect Lean4 code snippet and list of corresponding emrors.
Incorrect Lean4 Code:
Ican4
incorrect lean4 code
Error List:
errors
errors
Please modify the incorrect Lean 4 code according to the following requirements: 1.The corrected statement must be syntactically valid and well-typed according to Lean4 rules.
2he correction should maintain the original mathematical meaning that the user was likely trying to express in the statement. 3.The corrected Lean code must end with :: by sorry'.
For your response, please follow this example format: **Modification Analysis**
analysis
Your detailed analysis
* **Corrected Lean4 Code**
lean4
Your corrected Lean4 code
Now, please provide your formal answer:
25

---

Published as a conference paper at ICLR 2026
A.6 CASE STUDY FOR EVOLAST
EvolAST is an approach that integrates code features(Tian et al., 2025; Yan et al., 2023; Luo et al., 2026) with mathematical reasoning, making it highly suitable for formal reasoning tasks in Lean4 code generation. We select an example of EvolAST from evolved dataset. The original Lean statement as follows:
Original Lean 4 Statement
theorem evolved thm (x, :y:R) (h_0 0 y 4) (h_1 y) (h_2 x'3 y 3555) 2 y 233 := by sorry
The evolved Lean 4 statement is as follows:
Evolved Statement
Evolved Formal Statement:
theorem evolved. hoolved_thm_atte thn_auged (x, R) (h_1 x) (h_2 : 3555 x'3 y'3) (h_0 :
* x) 233 = y + 2 := by sorry
A.7 DETAILS OF SIMILARITY EVALUATION
We report here the full prompt template used for the LLM-based similarity assessment.
Prompt Template for Similarity Evaluation
Your task is to evaluate whether the two given formal math statements similar, not just looking similar or involving overlapping mathematical concepts. Please analyze both statements carefully, focusing
The overall structure the statements (e.g., setup, sequence of steps, logical flow)
2. The specific mathematical operations reasoning paths required,
3. The wording and presentation style,
Whether one statement appears be trivial rephrasing or numerical variant of the other.
Provide a similarity score from to 10, where:
1 completely different statements,
10 semantically identical statements.
Here are provided statements:
Statement1:
(statement1) }
Statement2:
{statement2]
Format your response as:
<reason>Reason for your score</reason>
<score>Your score(1-10)</score>
A.8 ANALYSIS OUTPUT LENGTH
Compared to other non-reasoning models, EvolProver exhibits higher average token consumption, primarily due to the design of its idtruction-tuning stage. In this stage, the model trained to repeat the problem statement (including both the formal statement and its corresponding natural language semantic annotation) before generating the proof. contrast, some other non-COT models, such SeepSeck-Provers V1.5 and Consequently, a non-reasonin segment (the repeated problem statement) is included in EvolProver's outputs and is counted in its token usage.
trained directly produce the proof.
26

---

Published as a conference paper at ICLR 2026
Benchmark FormalMATH-lite
Average Token Length
407.3
Minif2f
440.8
Table 6: Average proof-only token length of EvolProver after removing the problem restatement.
Model EvolProver-Ban Average Token Length
Tactic Steps
113.75
EvolProver
129.05
10
Table 7: Average token length and tactic steps of EvolProver and EvolProver- Base on the subset of commonly solved problems.
To quantify this effect, we additionally compute the token length for the proof-only portion of EvolProver after removing the problem restatement. The results are shown Table
We believe that the token length of the output containing only the proof is on the same scale as that of other non-COT models. Additionally, we measured the output length and the number of executed tactic steps on the subset of problems solved by both EvolProver and its baseline. We consider tactic steps to be good representation of the verified proof length some extent. The results are shown in Table 7.
As we can see, EvolProver has slightly higher values in both Average Token Length and tactic steps compared to ExolProver-Base. We carefully examined their proofs and selected representative example for comparison:
Representative Lean 4 proofs of EvolProver- Base and EvolProver
Proof of EvolProver-Base
theorem example_base (x (hx
(h 11:1
18
x
by
field_simp
linarith
--
Proof of EvolProver theorem example_evelved [x } (hx 0) (h / + 18 x)
have by
6 := by
have : 1 / x
9
:= by linarith
have : 1 / x 1 / : by norm_num at
have h x 6 := by
have h field_simp at h nlinarith
0 := hx
exact exact
We found that the response from EvolProver- Base is more intuitive, with a direct approach and lower readability, while EvolProver's response more ceasoning-basee habitually showing the conditions and providing a clear proof. However, this results in a longer output.
A.9 USE OF LARGE LANGUAGE MODELS
We utilized Large Language Models (LLMs) solely to refine the language and improve the clarity of this manuscript.
27


Reviews:
[{"review_id": "RImCn1oncv", "reviewer": "Reviewer_uSHo", "summary": "This paper introduces EvolProver, a 7B parameter non-reasoning LEAN theorem prover model. The model is fine-tuned using data generated from a new data augmentation pipeline. The pipeline consists of three components:\n\n1. **EvolDomain**: Uses LLMs to reformulate the existing problem into different mathematical domains.\n2. **EvolDifficulty**. Uses LLMs to adjust the difficulty of the theorem.\n3. **EvolAST**: Applies syntactical rewrites using a small amount of equivalence rules.\n\nEach transformed problem is filtered via a Lean syntactic check and an LLM semantic check. The pipeline is applied to existing theorem datasets, producing a larger and more diverse dataset used to fine-tune DeepSeek-Prover-V1.5. The resulting model, EvolProver, achieves strong performance outperforming both non-reasoning and some reasoning models.", "questions": "1. What specifically distinguishes EvolDomain/EvolDifficulty from prior prompt-based data synthesis?\n2. How often do EvolDomain/EvolDifficulty produce invalid or semantically incorrect statements before filtering?\n3. The verification pipeline appears to be computationally expensive. What is the computational cost of running the full pipeline (LLM generation + filtering + AST evolution + proof synthesis)?", "limitations": "", "rating": 4, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The paper empirically demonstrates that diversified training data can improve robustness of formal theorem provers. The multi-stage verification (Lean compilation + LLM judging) appears carefully constructed, and the ablation study highlights the contribution of each augmentation component. Improvements are reported on several benchmark datasets (FormalMATH-Lite, MiniF2F-Test, and Ineq-Comp).  The paper’s focus on token-efficient, non-reasoning proving is practically important and timely, given the inference-time and cost problem of chain-of-thought systems.", "weaknesses": "My main concern is the novelty of the proposed data augmentation method. The individual techniques used in the pipeline appear to be adaptations of well-known ideas rather than new contributions. Using LLM prompting to evolve instructions or problems (EvolDomain, EvolDifficulty) closely resembles approaches such as WizardMath or MetaMath. The final model architecture and training recipe (SFT + RL) seem to follow existing pipelines from e.g. DeepSeek-Prover.\n\nReproducibility and community impact are constrained by unclear release plans: code, datasets, and model checkpoints appear contingent on institutional approval with no firm timeline or open-model replication, making it difficult for others to verify and build upon the work.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "a0thwGgCOa", "reviewer": "Reviewer_wPuw", "summary": "This paper presents EvolProver, a formal-reasoning LLM fine-tuned on a synthetically expanded dataset constructed through three evolution mechanisms: \n\n(1) EvolDomain, which performs cross-domain statement translation via LLMs;  \n(2) EvolDifficulty, which adjusts statement complexity; and  \n(3) EvolAST, which applies symbolic abstract-syntax-tree (AST) rewriting rules such as commutativity and De Morgan transformations to generate logically equivalent variants.  \n\nThe resulting dataset, comprising roughly 39 k verified (statement, proof) pairs in Lean 4, is used to SFT and RL-train a DeepSeek-Prover-V1.5-Base model. EvolProver achieves new state-of-the-art results on several formal benchmarks including FormalMATH-Lite, MiniF2F-Test, and Ineq-Comp, demonstrating the potential of AST-based symbolic augmentation to improve verifiable reasoning.", "questions": "1. Could the authors provide token-length and proof-length statistics restricted to the intersection of solved problems between EvolProver and EvolProver-Base?\n\t2.\tCan the authors further clarify how they ensured no data leakage between training and test dataset? A quantitative similarity or embedding-based overlap metric would help.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1.  The integration of symbolic AST transformations into the data-generation pipeline is novel and convincing. EvolAST guarantees semantic correctness and diversifies syntax without requiring additional verification.\n2. MThe paper clearly outlines each augmentation stage and the verification loop, with Lean 4 compiler checks for both syntax and semantics.\n3. Consistent and substantial improvements across benchmarksindicate that the augmented data meaningfully enhances formal reasoning ability.", "weaknesses": "1. Data contamination analysis: While the authors mention ensuring non-overlapping “initial states,” this safeguard is underspecified. It remains unclear whether evolved statements might still share logical content or minor transformations with the test set. A more thorough contamination study—quantifying overlap at the theorem or syntactic-similarity level—would strengthen the empirical claims.\n2. Lack of output-length analysis: Table 1 reports that EvolProver generates substantially longer outputs than comparable non-reasoning models, yet the paper provides no interpretation. It is unclear whether performance gains arise from genuinely better reasoning or simply more verbose exploration, which turns the model into a \"semi-reasoning\" model.\n    - I would appreciate it a follow-up would measure output length (or verified proof length) on the subset of problems solved by both EvolProver and its baseline, to see whether the improvement correlates with verbosity or genuine efficiency.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "3hVwPf0Zq6", "reviewer": "Reviewer_7CuZ", "summary": "The paper presents a data augmentation pipeline aimed at improving the robustness and generalization of large language models (LLMs) for formal theorem proving. The proposed system combines three key modules:\n\n* EvolAST – syntactic augmentation using Abstract Syntax Tree-based transformations that preserve semantics while changing structure;\n\n* EvolDomain – semantic augmentation by translating theorems across mathematical domains (e.g., geometry ↔ algebra) using LLMs;\n\n* EvolDifficulty – difficulty modulation via evolutionary instructions to generate problems of varying complexity.\n\nAfter automated verification, the augmented data is used to train EvolProver, a 7B-parameter non-reasoning model that achieves new SOTA performance on multiple formal math benchmarks (e.g., FormalMATH-Lite, MiniF2F, Ineq-Comp). Ablations confirm each augmentation’s benefit. The approach focuses on data diversity rather than architectural changes.", "questions": "Addressing the questions mentioned in the weakness points should be enough.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Practical and well-motivated. They address a real problem on the fragility and poor generalization of theorem-proving LLMs, and the strategy they use (data-centric improvements) is simple but effective, much easier than building a reasoning model in practice.\n\n2. Systematic pipeline design. The decomposition into syntactic (EvolAST), semantic (EvolDomain), and difficulty-based (EvolDifficulty) augmentations is both intuitive and well-structured.\n\n3. Results are good. The model achieves consistent SOTA performance across diverse benchmarks, including non-reasoning categories where size-matched baselines are surpassed. They can achieve even pretty close performance compared to the SOTA reasoning model baselines. Ablations studies convince us into believing that the pipeline really helps, rather than overfitting to artifacts.", "weaknesses": "1. The paper remains more empirical than theoretical, as there's no deeper analysis of why the augmentations help, or how they relate to reasoning robustness.\n\n2. There comes concerns on whether or not the framework relies on LLM-generated data too much. EvolDomain and EvolDifficulty both depend on LLM quality, thus risk subtle semantic drift or spurious logic, which might not be fully detected by verification.\n\n3. Only benchmarks with formal Lean-style problems are tested, how robust the framework is when generalizing to other theorem systems, or other symbolic reasoning datasets?\n\n4. The term \"evolutionary\" may be overstated a little bit?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Yi1HUb58GZ", "reviewer": "Reviewer_RmgK", "summary": "This paper proposes three data augmentation methods for formal mathematics statements based on symmetry and difficulty. EvolAST: apply seven prewritten transformation rules at random on the theorem’s AST to produce logically equivalent variants; EvolDomain: translate problems across different domains while preserving their core logic, guided by evolutionary instructions for the LLM to perform the conversions; EvolDifficulty: use an LLM with instructions to adjust the difficulty of existing theorems and generate statements at varying difficulty levels. Using this pipeline to augment public datasets (e.g., STP and DeepSeek Prover V1) and training on DeepSeek Prover V1.5 base, the authors build EvolProver. Experiments show strong performance the proposed model among non-CoT 7B ATP models.", "questions": "1. Can the three proposed augmentation methods be applied to chain-of-thought reasoning models? What obstacles might arise from directly applying them to CoT-style reasoning models? The paper claims that current provers are fragile to even minor transformations of problem statements — does this fragility persist in contemporary reasoning provers like Deepseek Prover v2 or Geodel Prover v2?\n\n2. Line 142 states that EvolAST is introduced \"to mitigate this issue (the inevitable introduction of syntactic or semantic errors),\" yet Figure 2 places the EvolAST process after EvolDomain and EvolDifficulty. This ordering seems odd: errors can propagate, so a theorem that becomes semantically incorrect (e.g., unprovable) after EvolDomain or EvolDifficulty would not be fixed by applying EvolAST afterward. Please provide further explanation for this pipeline ordering and clarify how EvolAST mitigates syntactic/semantic errors introduced by earlier stages.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1. The proposed EvolAST method is novel: it leverages Lean 4 features in an intuitive and effective way. The results in Table 2 on the Ineq-Comp dataset show that this augmentation can substantially mitigate non-CoT provers’ fragility to the specific form of a statement.\n\n2. From Figure 5, the EvolDomain approach appears to significantly alleviate the concentration of formal-statement datasets in algebra and number theory. This may be valuable for improving ATP generalization across different mathematical domains.\n\n3. The ablation study is thorough. Table 4 presents multiple combinations of SFT, RL, and different augmentation methods, providing useful insight into which components are effective. The comparison between directly augmenting formal data and the more traditional approach of augmenting natural-language data first and then translating it is also a useful addition.\n\n4. Figures and tables are clear and easy to understand, and the paper is well written overall.", "weaknesses": "1. Choice of an old base model and non-CoT approach, which appears unnecessary and hard to justify. The paper trains EvolProver on a non-CoT DeepSeek V1.5 7B model. The three proposed data-augmentation methods should in principle be directly applicable to CoT-style models (e.g., DeepSeek Prover v2 or Goedel Prover v2), so restricting experiments to a non-CoT, relatively old base model limits the relevance of the work given that much of the recent ATP community has shifted to CoT-capable reasoning models. EvolProver’s performance is still substantially weaker than contemporary reasoning models. The authors should further explain why they chose a non‑CoT model and an older base model.\n2. Small amount of synthesized data and no cost analysis. The amount of augmented/synthesized data is relatively small and the paper does not discuss the cost of data synthesis. Line 653 states that the pool of publicly available datasets used is 3.3 million examples, but only 39.2k examples were synthesized (Line 665). The authors do not explain the roughly two-order-of-magnitude gap (e.g., due to cost or filtering?), nor do they provide analysis of synthesis cost, token usage, or API expenses.\n3. Missing proportions of original vs. augmented data in SFT and RL. The paper does not report the ratio of original to augmented examples during supervised fine-tuning (SFT) and reinforcement learning (RL), which hurts reproducibility. Given the large disparity in size between the original and augmented datasets, the mixing ratio is an important experimental detail and should be provided.\n4. Minor writing and presentation issues (do not affect readability but should be fixed to improve manuscript quality)\n\n- Line 124: missing space before a citation.\n- Lines 143, 153, 227: inconsistent capitalization of “Lean4” vs. “Lean 4”; terms should be made consistent.\n- Table 4 and Table 5 appear to contain the same content and may be duplicated.\n- Related work: the survey of data-augmentation methods focuses on informal mathematics; the authors should also cover data-augmentation methods specific to formal mathematics. (eg., STP and Ineq-Comp)\n\n##", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1Kzx8nfbYL", "reviewer": "Reviewer_fmUh", "summary": "This paper presents EvolProver, a 7B-parameter non-reasoning theorem prover enhanced through a novel data augmentation pipeline that addresses both symmetry and difficulty aspects of formalized mathematical problems. The pipeline consists of three complementary methods: EvolAST for syntactic symmetry transformation, EvolDomain for cross-domain semantic symmetry, and EvolDifficulty for generating problems with varying difficulty levels. Experimental results demonstrate that EvolProver achieves good performance on multiple benchmarks, including FormalMATH-Lite (53.8% pass@32), MiniF2F-Test (69.8% pass@32), and Ineq-Comp datasets, outperforming comparable non-reasoning models and even some reasoning-based models while using significantly fewer tokens.", "questions": "1. Why wasn't DeepSeek-Prover-V2-7B-non-CoT included in the comparisons for FormalMATH and Ineq-Comp benchmarks, given its strong performance on MiniF2F-Test? Including these comparisons would provide a more comprehensive evaluation of EvolProver's capabilities across different benchmarks.​\n2. The example shown in Figure 1 appears to involve relatively minor tactic changes in Lean that may not significantly affect the proof difficulty. Could you provide more case studies demonstrating specific instances where the augmented dataset enabled EvolProver to solve problems that the baseline model (EvolProver-Base) or other state-of-the-art models could not solve?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "1. The proposed data augmentation pipeline demonstrates a novel and systematic approach to improving model generalizability by addressing both syntactic and semantic symmetry, as well as difficulty variation, which is a comprehensive solution to the fragility issue in formal theorem proving.​\n2. The ablation studies and controlled experiments effectively validate the contribution of each component in the pipeline, showing consistent performance improvements across multiple benchmarks and training stages.", "weaknesses": "1. The performance advantage of EvolProver over DeepSeek-Prover-V2-7B-non-CoT on MiniF2F-Test is relatively modest (69.8% vs 68.0±0.5%), while DeepSeek-Prover-V2-7B-non-CoT uses fewer average tokens, raising questions about the practical significance of the improvement.​\n2. The case study in Figure 1 does not clearly demonstrate how the augmented dataset helps solve problems that were previously unsolvable, making it difficult to assess the qualitative impact of the data augmentation.​\n3. The ablation experiments do not include a detailed analysis of how each component contributes to performance on different mathematical domains, which would help understand the specific strengths of each augmentation method.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)