Let's Explore Step by Step: Generating Provable Formal Statements with Deductive Exploration
Authors: Qi Liu
Kangjie Bao
Yue Yang
Xinhao Zheng
Renqiu Xia
Qinxiang Cao
Junchi Yan
Venue: ICLR 2026 Poster (2026)
Keywords: large language model
math
formal theorem proving
problem generation
automated conjecturing
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We proposed a whole-process verifiable data synthesis framework for mathematical reasoning, and a data bootstrapping method for the framework.

Abstract: Mathematical problem synthesis shows promise in resolving data exhaustion, contamination, and leakage for AI training and evaluation. Despite enormous efforts,
an **expressiveness-validity-complexity trilemma** remains an open question. Existing methods either lack whole-process verifiability, are constrained to a particular domain, or are bounded by external models.
This paper breaks the trilemma by proposing the framework of **DExploration** _(**D**eductive **Exploration**)_, which formulates problem synthesis as a step-by-step exploration process instead of one-shot generation. Agents are equipped with three simple yet powerful atomic actions: _introducing_ variables/hypotheses, _deducing_ new facts, and _submitting_ derived facts. The entire exploration process is formally verified by Lean 4, which encompasses most mathematical domains up to the research level.
Once a conclusion is submitted, the framework outputs a formal statement with guaranteed provability, reducing the need for external models.
To bootstrap training data for DExploration, we propose **Exploratory Transformation** to distill exploration trajectories from existing large-scale theorem-proving data. It rewrites formal proofs into a deductive style, parses dependencies among variables, hypotheses, and proof steps, then reassembles them into exploration trajectories by a topological order.
Experiments validate the effectiveness and efficiency of our methods, achieving an improved success rate ($40.70\\% \mapsto 54.52\\%$), reduced token cost ($52.9\text{K} \mapsto 8.8\text{K}, 83\\%\downarrow$), broader complexity and difficulty distributions, and Pareto optimality.
In $2726$ valid generations, three state-of-the-art provers fail on $60$ (Pass@4) and $8$ (Pass@64).

Published as a conference paper at ICLR 2026
LET'S EXPLORE STEP BY STEP: GENERATING PROV- ABLE FORMAL STATEMENTS WITH DEDUCTIVE EX- PLORATION
Qi Liu, Kangjie Bao, Yue Yang, Xinhao Zheng, Renqiu Xia, Qinxiang Cao, Junchi Yan" School of Computer Science & School of Artificial Intelligence, Shanghai Jiao Tong University Shanghai Innovation Institute {purewhi te, yanjunchi wtwpunchhh/jjuuueuuuuuuuu
https://githube http://cww....eeeiieeeeoo///////
ABSTRACT
Mathematical problem synthesis shows promise in resolving data exhaustion, con- tamination, and leakage for Al training and evaluation. Despite enormous ef- forts, parressieees--aliiiiyy--ommppp
trilemma remains open ques- tion. Existing methods either lack whole-process verifiability, are constrained particular domain, or bounded external models. This paper breaks the trilemma by proposing the framework of DExploration (Deductive Explo- ration), which formulates problem synthesis as step-by bte- exploration process instead of one-shot generation. Agents are equipped with three simple yet pow- erful atomic actions: introducing variables/hypotheees, deducing new facts, and submitring derived facts. The entire exploration process is formally verified by Lean which encompasses most mathematical domains up the research level. Once conclusion is submitted, the framework outputs formal statement with guaranteed provability, reducing the need for external models. To bootstrap train- ing data for DExploration, we propose Exploratory Transformation to distill ex- ploration trajectories from existing large-scale theorem-provine data. rewrites formal proof's into a deductive style, parses dependencies among variables, hy- potheses, and proof steps, then reassembles them into exploration trajectories by topological order. Experiments validate the effectiveness and efficiency of our methods, achieving an improved success rate (40.70% 70% + 54.52%), reduced token cost (52.9K 8.8K, 83% 4), broader complexity and difficulty distributions, and Pareto optimality. In 2726 valid generations, three state-of-the-as provers fail on 60 (Pass@4) 4) and (Pass 64).
A mathematical problem should be difficult in order to entice us, yet not completely inaccessible, lest mock at our efforts.
David Hilbert, Mathematical Problems
INTRODUCTION
State-of-the-art large language models (LLMs) demonstrate super-human reasoning capabili-
ties (OpenAl et al.] 2024a DeepSeek-AT et al.) 2025).
especially mathematical reasoning (Trinh)
al. [0224] Huang& Yang 2025 Chen et al. 2025
However, current evaluation pipelines suffer
Choi et al. 2025), leakage (Xu et al.) (2024) and static complexity (Zhu et al. (023)) LLM training is rapidly approaching the exhaustion of
Trom data contamination (Golchin & Surdeanu 2024
numan-generatee data (Villalobos et al. 2024 Yang et al., 2026). To continue pushing the bound-
aries of Al reasoning, there growing need for scalably generating fresh, valid, and complex problems challenging evaluation benchmarks and high-quality training data (Team) 2025b).
Recent advances in mathematical problem synthesis show promise in addressing this need. How- ever, existing methods suffer from a critical trilemma (Li al. 2024b) across three core desiderata:
"Corresponding author. This work was in part supported by Scientific Research Innovation Capability Support Project for Young Faculty (U40) of the Ministry of Education of China, SRICSPYT-222025019,

---

Published as a conference paper at ICLR 2026
expressiveness (covering diverse mathematical domains), validity (generating provable and non- contradictory problems), and complexity (producing challenges that push Al limits). LLM-only methods (Luo et al. 2023 Tang et al., 2024 Zhao al. (025) synthesize questions and generate/- filter answers using LLMs, which is error-prone. L.LMs' capacity also limits the difficulty of the problems they generate. Domain-specific methods (Zhu al.) 2023 TTinh al.] [024] [L et al.
2024b, Zhang et al. 2025) leverage deterministic algorithms to guarantee validity at the sacrifice of broad expressiveness. Formal-based methods combine LLMs and the Lean 4 environment (Moura & Ullric (021), which spans up to research-level mathematics and can formally verify statement- proof pairs. These methods fall into two lines: conjecture-prove methods (Poesia al., [024] Dong & Ma 2025) directly generate formal statements and invoke LLM-based provers to attempt proofs: Autoformalizer-base
methods (Huang et al. 2024; Leang et al. 2025) first synthesize in- formal problems and solutions, then autoformalize them into formal statements and proofs. Both paradigms inherit the diversity of LLMs and the expressiveness and verifiability of Lean. However, incorrect autoformalization undermines validity (Leang et al. 2025). The capabilities of autoformal- izers and provers bound the complexity of synthesized problems. If the problems are too complex, formalizing or proving may easily fail, thus limiting the generation of truly challenging problems.
We propose DExploration (Deductive Exploration) to break through the complexity limit while maintaining expressiveness and verifiability. Instead of generating statements in one shot, agents explore the mathematical world step by step, with each move grounded in Lean. It supports three simple yet powerful atomic actions: introducing new variables or hypotheses, deducing new facts based on known context, and submitting any discovered fact as the conclusion. When a conclusion submitted, we reconstruct a formal statement by concatenating the introduced hypotheses and the submitted fact. Then, a proof is extracted from the exploration trajectory, ensuring the provability of the formal statement and reducing the need for external LLMs.
As novel framework, DExploration faces severe scarcity of training data. We propose exploratory transformation to transform statement-prow pairs of existing theorem-proving data into explo- ration trajectories. Given a statement-proof pair, we first transform the proof into deductive manner (i.e., step-by-step logical inferences from hypotheses to conclusion). Next, we construct a depen- dency graph whose nodes are context variables and deductive steps, and whose edges represent the dependencies among them. We traverse the graph, following a topological order, and prefer- ring deeper and deductive nodes. This traversal distills mathematical exploration intuitions into an exploration trajectory. Based on these data, we train the DExplorer agent as a proof-of cof-ccecept......
Experiments validate the effectiveness and efficiency of our methods. DExplorer demonstrates sig- nificantly higher success rate (40.70% + 54.52%), magnitude of reduced token cost (> 52.9K r 8.8K, 83% J). and better diversity (Rouge-I. 0.186 - 0.173). For formal reasoning, our generated problems exhibit greater complexity (Top-500 complexity 1231 + 1374). For informal reason- ing, our problems are more difficult (Top-500 difficulty 0.16 + 0.05). Our methods also achieve Pareto optimality in terms of success rate. SOTA provers, including Goedel-Proverr V2-8B (Lin al. 2025). DeepSeek- Procek--Proee--ee V2-7B (Ren et al. 2025), and 2025a), fail to prove 60 statements (Pass @ 4) and 8 (Pass @64) in total 2726 valid generated state- ments. This highlights the potential of our methods to push the boundaries of formal reasoners.
--B (Wang et al.,
Ablation studies validate the necessity of our enhancements. Ablating DExploration, the resulting Conjecture-Provee system yields on-par performance compared to the strongest baseline. Ablating exploratory transformation results in a significantly lower success rate (64.18% + 52.10% with on-par average token cost (8841 + 8800). The distribution of complexity also shifts downward (515 + 470 overall and 1374 + 1193 for the T0p-500).
In short, this paper aims to synthesize provable formal statements, benefiting both formal and in- formal reasoning. We identify the synthesis methods and locate one of its root causes: dependency on external models for autoformal- ization or proof. The contributions of our work are summarized follows.
trilemma in existing problem
1. DExploration (Deductive Exploration), a Lean based framework for Mhole-process verifiable step-by-step exploration. The progressive exploration process enables unified generation of for- mal statements and proofs, ensuring the provability of generated statements and reducing the need for external provers. (Sec. 4.1
2

---

Published as a conference paper at ICLR 2026
2. Exploratory transformation, pipeline to bootstrap initial training data for the DExplorer agent. A formal statement proof pair is rewritten into deductive style, then parsed into a de- pendency graph, and finally reassembled into exploration trajectory. (Sec. 4.2
3. Extensive comparative experiments and ablation studies validate the effectiveness and efficiency of our methods. DExplorer demonstrates all-round improvements over baselines and ablations re- garding formal reasoning, informal reasoning, efficiency, diversity, and Pareto-optimality. (Sec. 5)
RELATED WORKS
Trading off among the expressiveness-vaidiii -ooplityy trilemma, existing literature mathe- matical problem synthesis can be divided into three categories.
LLM-based Methods. Early pioneers in this category augment seed datasets (e.g., GSM8K) by prompting LLMs. WizardMath (Luo et al.] 2023) uses Evol-Instruct to rewrite seed problems with different complexity or topic. MetaMath (Yu et al. 2023) augments problems by strategies includ- ing rephrasing, backward reasoning, and self-verification. AugGSM8K (Li et al., (022a) applies various augmentation methods on GSM8K. [Zhu al.) (2024) proposes augment problems with a probing-judging multi-agent framework. Recent literature generates new problems and validates them with strong reasoners. MathScale (Tang et al., 2024 prompts LLMs to generate new prob- lems conditioned on topics and knowledge points in seed datasets. ScaleQuest (Ding et al. 2025) fine-tunes an LLM to model the distribution of problems and samples from PromptCoT (Zhao et al. 2025) trains an I.MM to generate both the rationales of problem construction and problems. While possessing the expressiveness of natural language, these methods face validity challenges due to error-prone LLM operations. The capability of quality evaluators bounds the quality of generated problems (Stroebl et al. 2024). Our methods differ by grounding the entire problem generation process in formal verification environments ensure correctness.
Domain-Speccfic Methods. This literature introduces Komain-speccife symbolic methods to en- hance validity. Val (Zhu et al. 2003) focuses several template tasks and generates by sampling on a directed acyclic graph. iZhang et al. 2025) generates statements for two TCS problems. Trinh al. (2024); Fu al. (2025) focuses on geometry. Aygün et al. (202)); Puzis al. (2006) focuses on first-order logic. Li et al. (2024b) pioneers to formalize and augment problems in the SMTTLIB language, then back-translate to natural language. Our methods are based on the Lean 4 (Moura & Ullrich 202T) theorem-proving environment, whose expressiveness covers up to research-level mathematics (mathlib Community 2020).
Formal-based Methods. These methods introduce formal theorem proving (FTP) for problem syn- thesis. One earlier line is Autoformalizer-baseee
methods. MUSTARD (Huang et al.. 2024) first generates problem and a proof in natural language, then autoformalizes them into Lean 3 for verification. Leang et al. (2025) follows this paradigm and further proposes iterative autoformal- ization to mitigate formalization error. Another line is Conjecture-Provee methods, which directly generate formal statements and then attempt to generate their proofs. Poesia et al. (2024) samples conjectures from LLM conditioned on target difficulty. STP (Dong & Ma 2025 augments seed theorems conditioned on a related lemma. QDTSynth (Wang et al., 2025b) augments seed theo- rems by tacties. LeanConjecturer (Onda al. 2025 synthesizes new statements based on seed files from Mathlib (mathlib Community| 2020). These works do not guarantee the validity of gen- erated statements and require expensive L.M calls generate formal proofs. Other works augment human-written Lean 4 proofs by symbolic equivalent/anteccdent mutation (Wu et al. (2024) or for- ward reasoning (Rotella al. 2025). Our methods differ in that we model problem generation as series of ane-grained LLM driven exploration steps in verified mathematics, thereby avoiding error- troo-prone autoformalization (Laang al. (025) and reducing the need for proof generators.
PRELIMINARY
Lean 4 (Moura & Ullrich 2021 provides a theorem-proving environment that checks the correct- ness of statement-pres pairs. It is based on the which views mathematical statements types, similar to types in Python. A proof usually refers to tactic-style proof. which consists of a sequence of tactics (like shell commands) that guide the Lean kernel prove the statement. Examples of such statement-proof pairs be found in Appendix H
isomorphism (Howard et al. 1980),
3

---

Published as a conference paper at ICLR 2026
3) Arteforeallsr--eee band Pered Proit
Pans/ Pall
(d) Exploratery Transformation (Oars)
(6) Autoo Aurtofomallinn related
tafirmal Spert
asseple (% TD) N
Inforeal Se @ Enfirred Asteer
Delactive Stey I
Forred Starowart
Parmel Free
Steg in
Inferred Preblem
Nordodariive Stop
in sorry
(o.2) Auteforradiar--Pooe
Sen-dadactive Stop
(b) Conyecture-
Foreal Stutensen
28 Formal Preof
Pamd
hail
(6 23 Depandency Andlysis
Bowniting 3 Beckehee-styye Freof
Proveer
NEN
DokocineStep
bodkcinettep in
Goijecturer
Nenv dedusidesti Seip
Action
6 Farmal Shatement
Neo deductiv Supp.
(c) DEspleration
Seamt caried fen
scact
(Cuns)
Dedacthe Presf
(1.3) Explenotery Reossenlling
Exploration Trajectory
Intodate TTi Introdace
(Sep)) Dalace (Stpp)
Pass/
lendda (wy Tal Deloce (Sep)) Defixe Blepp. Introdase Do. To.
annodan TVl Deduce (Sup)) Sebmat (bo)
Figure/ 1: Pipelines of baselines (a.1, a.2, b), our DExploration (c), and exploratory transformation (d). Instead of directly synthesizing problems, DExploration supports agents in verifiably exploring the mathematical world step-by-step and submitting derived conclusions as problems. Exploratory transformation distills exploration trajectories from transforming theorem-proving data by (d.1) rewriting a formal proof into deductive-style, (d.2) constructing dependency graph for conditions and proof steps, and (d.3) traversing the graph to reassemble an exploration trajectory.
Whole-Proof Generation. Given a formal statement, most state-of-the-ar provers (Wang et al., 2025a Ren et al., 2025 Lin et al. 2025) model proof generation as rejective sampling: repeatedly sample a whole proof candidate conditioned on the statement until the proof passes Lean typecheck.
Tactic-Style Proving, Notably, Lean supports writing proofs incrementally.
maintains a proof state initialized with the statement to prove. A proof state consists of finite set of proof goals (things that we should prove) {T, + ),)=_1 where the local context I is an ordered list of declarations (a list of given information), the target U, is a type (the conclusion to prove). A declaration can either be an assumption (z T) (declaring a variable or assuming a hypothesis) or definition (z := t T)).
Tactics create, modify, close proof goals. When all proof goals are closed, the proving succeeds.
4 METHOD
Approaches for mathematical problem posing can be divided into two directions (iiverr 1994 Li-
jedahl & Cail 202T): Backward constructs or rewrites problems from particular knowledge points or seed problems. Forward is more genuinely discovering intriguing conclusions by exploring and investigating the mathematical world (Polya) 2021 Ernest et al. 2016: Elgrably & Leikin (02I).
Inspired by forward posing, this section introduces DExploration (Deductive Exploration), a Lean- based framework where agents verifiably explore the math world step-by- and discover facts to synthesize problems. To bootstrap a DExplorer agent, exploratory transformation is proposed to distill exploration trajectories from existing formal statement-pros pairs.
4.1 FRAMEWORK: DEXPLORATION
DExploration formulates mathematical exploration as a deterministic Markov Decision Process.
States. We maintain an exploration state S. = (T,, A.) S, where the introduced context T [v. T is an ordered list of all introduced variables and hypotheses; and the deduced context A, = [h, H.)) is an ordered list of all derived intermediate facts. So is initialized as (I]-
Actions. To enable active exploration, three basic but powerful actions should be supported:
Introduce(v: (T,
: A) (T [[ T)], A). Add new variable or hypothesis (v T) to T.
4

---

Published as a conference paper at ICLR 2026
Deduce(h: H) (T, [hh H))). Deduce fact H based introduced variables, hypotheses, and previously derived facts. It should propose the assertion and prove Po H. Submit(h: [1' A) = r + H. Submit the fact H as the target conclusion, reconstruct statement I H and its proof, and end the episode.
Implementation. We concretize DExploration in Lean 4 (Moura & Ullrich] 2021). The union of the introduced context I and the deduced context A corresponds Lean's 's proof state (ToA False). To differentiate from A, the introduced context I' is also maintained externally.
Actions are implemented using tactics. Introduce(v : T) is concretized with obtain (w. 3(v: T). True := sorry, which introduces free variable hypothesis (v 7) without actual proof. The placeholder (-: True) then removed to avoid context rot. The name of the introduced variable should not contradict with existing variables. Care should be taken to avoid introducing a hypothesis (u 7) that leads to a contradiction. If I o [e 7] False holds, anything I' ju T + U follows. We add an explosion check after introducing hypothesis: execute light- weighte heuristic to prove False. it succeeds, the introducing step is rejected.
Striet implementation of Deduce(h H) only allows the have-tactie, which proposes and proves one hypothesis H. For stronger expressiveness and affinity to traditional theoren-proving, we relax the restriction to deductive tactics, which covers tactics that 1) does not create extra goals, only modifies the current goal; 2) does not modify the target of the goal; 3) does not modify variables (in the Type universe) in local context. For example, have and apply at are deductive tactics, while constructor and apply y are not. More discussions can be found in Appendix A
Submit(h: H) implemented externally. The output statement I H is guaranteed to be provable. A corresponding proof can be reconstructed by concatenating all deducing steps and transforming the submission step into an exact tactic. Proofs and discussions can be found in Appendix
Therefore, DExploration enables whole-process verified math exploration and unified generation of statements and proofs, reducing the need for extra provers. However, LLM-based agents for DExploration face extreme scarcity of training data.
4.2
DATA BOOTSTRAPPING: EXPLORATORY TRANSFORMATION
To construct training data for DExploration, we distill human creativity and intuition from existing large-scale theorem- prrvving data. We propose exploratory transformation to transform off-the-sheiff statement-pres pairs into exploration trajectories, which consists of three main steps: deductive rewriting, dependency analysis, and exploratory reassembling.
Deductive Rewriting. Given a statement- proof pair (T + U, [s.] where r = [(:: Vo) we first transform the proof [s into a deductive-style proof. Suppose the first non-deductive tactic is sx < k < m). we obtain series of deducing tactics [si]ick- The remaining tactics are wrapped into two deductive tactic: s-2 == have by := by [<issm. and 8_1 exact hy. Then, deductive tactics [silisk o [s-2, 8-1] forms deductive proof.
Dependency Analysis. We further analyze the relations among variables in I and deductive steps [s.] A variable (v T) in I' depends another (v' T') if o' occurs in T. Deductive steps manipulate the context of the proof goal. Therefore, a step uses variables (x;) == ((") Tk)) in its execution and creates V+ (s:) {(VE Th mm ] depends on all variables in Tnv_. Moreover, all subsequent steps sy that V_(s,) n V (s.) * depends on because removing s; from [su]A<s makes sj fail to execute. As visualized in Fig. d.2)), the dependency relations form
directed acyclic graph (DAG) where each node represents a variable in I' or a deductive step, each edge represents a dependency.
Exploratory Reassembling, During exploration, a mathematician prefers to derive as many con- clusions as possible, and only introduce new hypotheses when necessary (Elgrably & Leikin 202T). We distill this depth-preferrnce by reassembling nodes in the dependency graph into an exploration trajectory. Let dep(s) denote the set of nodes that node s depends on. The reasoning depth of is
max d(s') + Eddep)))
dep(s) s) *
d(s)
0
dep(s) 0
5

---

Published as a conference paper at ICLR 2026
Formally, d(s) represents the level of topological generation for Intuitively. d(s) reflects the depth of exploration: s can be reached from basic hypotheses with d(ss)-immes reasoning. We conduct a topological sort on the dependency graph while prioritizing available nodes that 1) have the highest reasoning depth, and 2) are not introducing steps. To obtain an exploration trajectory from the traver- sal path, substitute all nodes of context variables (v T) with introducing steps Introduce(r: T), and replace all nodes of deductive tactic with deducing steps s.
EXPERIMENT
This section validates the effectiveness and efficiency of the proposed methods. Sec. 5.1 introduces comparative and ablative methods for evaluation. Sec. 5.2 details the evaluation settings. Sec. 5.3 reports and analyzes the experiment results. All experiments share identical training recipe and sampling parameters, as detailed in Appendix Prompt templates are in Appendix G Lean 4 envi- ronment details are in Appendix Details for benchmarking informal reasoning are in Appendix
5.1 EVALUATED METHODS
Two main paradigms, Autoformalizer stronger baseline, Autoformalizer- Prover,, by chaining SOTA informal problem synthesis methods, autoformalizers, and provers. For ablation, Conjecturer- Provver shares the training dataset with DEx- plorer while ablating DExploration. DExplorer (Staged) ablates the exploratory transformation by forcing the exploration to follow the order of introducing, deducing, and submitting.
and Conjecturer- are evaluated. We form a
Autoformalizer-basee methods (Huang al. alist L.MSs to generate informal problems and proofs conditioned on randomly sampled math con- cepts. Then, they prompt LLMs autoformalize the informal data into formal code. We adopt pub- lished data from MUSTARD (Huang et al. 2024), which consists of 28,316 Lean 3 files generated by GPT-4 (OpenAl al. 2024b), where 5,866 are typechecked. We utilize Mathport (Teanprover- 2024)) community, 2024) to migrate them to Lean 4, yielding 3,794 formal statement- pairs.
2024 Leang et al. 2025 (Fig. Ia. prompt gener-
Autoformalizer-Prowee methods (Fig. D (a. first synthesize an informal question-answw pair, call an autoformalizer to formalize it into a formal statement, and then call LLM provers to gen- erate proofs. We adopt published data from ScaleQuest-Math (Ding et al. 2025). PromptCoT- DS, and PromptCoT-QwQ (Zhao et al., (025)) as the informal data source. We adopt Kimina- Autoformalizer-7B (Wang et al. 2025a) as the autoformalizer. Three SOTA LLM provers: Goedel-
Prover-V2-8B (Lin et al. 2025). SeepSeek-Provers Prover-V2-BBB (CoT mode) (Ren et al. 2025), and Privina-rooer-DDsttlll
(Wang et al. 2025a) are invoked to generate at most N, = 4 proof candi- dates. If at least one passes Lean typecheck, the statement is proven.
Conjecturer-Prover methods (Poesia et al. 2024 Dong & Ma 2025) (Fig. [(b) use an LLM conjecturer generate formal statements, and call provers to prove. For fair comparison, fine-tuned the conjecture from Goedel-Prover-- V2-8B (Lin et al.) 2025) using the proven formal statements NuminaMath-Lean (Wang et al. 2025a). Generated conjectures are proven using the identical prover settings to the Autoformalizer-P Prover experiment. Compared with DExplorer, Conjecturer-Provee Prover directly generates the entire formal statement while sharing the same training set and base model. Therefore, it also works as an ablation of DExploration.
DExplorer. (Fig. c)) We apply exploratory transformation on the NuminaMath- (Wang al., 2025a) dataset, obtaining 39,509 exploration trajectories to fine-tune Moodell-rrveer V2-8B (Lin
et al. 2025) as the agent. In each episode, the agent generates at most N, = 80 steps.
DExplorer (Staged). Based on DExplorer, we restricted the exploration to be staged: the agent first generates a series of introducing steps. Once generates the first deducing step. it then constrained to only generate deducing or submitting steps. We keep the step limit N, 80. This experiment ablates the exploratory transformation by disabling interleaved deducing and introducing.
5.2 EVALUATION SETTING
For all methods excluding MUSTARD, we run 5, 000 episodes to generate formal statements and proofs. For MUSTARD, all 3794 formal statement-proof pairs participate in the evaluation. The

---

Published as a conference paper at ICLR 2026
DEcolord
Valid stetement Irequency
Generatennt
(Staged)
Difiiclity (i-Diffiuut
Conuduus/rrar
Calakn Queek Froof Qureetinn
25
Propptstas
Intractable for External Provers
20
homptc:T-00Q
15
MUSTA1D
D-300
300-600
600-900
900+
Complexity Range
Figure 2: Frequency of valid statement across complexity ranges, normalized to total generations. The portion of informalized difficulty (lower is more difficult). DExplorer outperforms all baselines in generating difficult state- ments (2 300 complexity or S 0.75 item difficulty).
-olivig questions and proof questions is colored with item
number of output tokens during generation is recorded. For fair comparisons of proof lengths, valid statements in MUSTARD and methods are re-proven using identical prover settings to those in the Autoformalizer-PPee Prover experiment.
Moreover, check the contradiction and validity of each statement. A statement I + U is tradictory if r o [hu : U] F False holde" Intuitively, this occurs when conditions are mutually contradictory. A valid statement is proven and not contradictory. We first attempt prove the sat- istiability [] ar, True with the three provers. each generating one proof candidate. If proven, the original statement is not contradictory. Otherwise, we try directly proving the contradiction T o [hu : U] + False with the three provers, each tries 4 times. If proven, the original statement contradictory. Otherwise, weighted explosion check in DExploration, use 1) Aesop (Limperg & From 2023), heuristic automation, and 2) SeepSeck-Prover-Ve
viewed (but not guaranteed) as not contradictory. For the light-
(Non-CoT mode) (Ren et al. 2025 to sample 1 proof.
We also explore possibilities to facilitate informal math reasoning. With 5-shot prompting DeepSeek-Vi (DeepSeek-AT, 2024), all valid formal statements are categorized and informal- ized into problem-solving questions proof questions in natural language. We uniformly sample 100 informalized wooleem-solving questions and invited human experts for a quality check. 97 incorrect due misformulating existence proof problems
of them are correct, while only as problem-solving questions. We then evaluate the difficulty of the synthesized problem-solvin questions with broad spectrum of open-source models, including Qwen3-8B (Team) (025b), Phi- 4-mini-instruct (Microsoft et al. (2025), OLMo-2-1124-77 IB-Instruct-vO.3 (Jiang et al.) (2023)
(OLMo et al. (2024). Mistral- 3.2-----..------sss (Grattafiori al.] (024), and Llama- 3. Instruutt (Grattafiori et al. 2024).
5.3
RESULTS AND DISCUSSIONS
5.3.1
MAIN RESULTS
The overall experiment results are summarized in Tab. [ Case studies of generated statements of DExploration can be found in Appendix We mainly evaluate the methods regarding the following aspects. Rubrics- -based evaluation of mathematical value is in Appendix [ where DExploration shows superior top-500 scores and on-par overall averages with best baselines.
Formal Reasoning. The complexity of formal statements measured with proof lengths (Huang 2024) (w/o comments and whitespaces). DExplorer demonstrates a clear advantage over baselines on the average complexity of top-500 statements (Cplx. 500). However, PromptCoT- QwQ and PromptCoT-DS show higher overall average complexity. We break down the generation frequency over complexity ranges in Fig. 2 which demonstrates that our method outperforms all baselines and ablations in generating problems with > 300 complexity. ScaleQuest generates the most problems in the 00, 300) complexity range, followed by our methods. Notably, 60 statements
Otherwise, either T + U does not hold (unprovable) or T Fal se holds. In the latter case, the conclusion U doubtful since Fa + A holds for any assertion A (explosion principle)

---

Published as a conference paper at ICLR 2026
Table 1: Comparative and ablative experiment results. [AlI.Proven, Crrovvn,Contr..V.... Valid.. Intract.): numbers of {all proven / contradictory / valid valid and unprovable by external provers) generated statements; To- ken Cost: average output token numbers for each valid statements. {- / >> indicates (missing underesti- mated); /Cplx.500,Cplo
{Top--500 / Overall) average complexity (i.c., proof length) of valid statements; (Diff.500, ):ft.): (Top-500/ Overall) average item difficulty of informalized problem-solving questions (lower is more difficult); Rouge-L: the Rouge-I. scores of informalized questions and answers (lower is more diverse).
Bold numbers emphasize best values; Underlined numbers emphasize second-best values.
Method
All
Proven]
Contra.
Valid
Intract.
Token Cost
Cplc.500)
Cpls.]
DitL.500)
Diir]
Rouge-L L..
MUSTARD
28316
3794
119
0.202
PrompiCoT-QQQQ
5000
1189
729
1024
172,927
1231
721
0.30
0.45
0.187
Pr
5000
678
927
457
441,758
786
786
0.40
0.40
0.186
ScaleQuest-Mathh
2369
1591
2005
52,915
217
0.76
0,220
Conjecture Prover
5000
1389
1817
1164
187,126
10/2"
578
0.51
0.52
0.174
DEsplorer (Staged)
5000
2605
269 1919
2340-1176
50
8,800 ca35e
1193.
470.
0.09 am
a.47
0.173 am
DExplover
5000
3209
497.10x
2726
8,841
1374
515
0.05
-144
0.47
0.173 Au93
(2.20% valid statements) generated by our methods have cc-complexity, i.e., not proven by any of the SOTA provers. We further evaluate all the provers with Pass@64. 8 of the statements (0.29% valid statements) remain intractable. This demonstrates our method's potential to surpass existing provers and uncover more challenging conjectures while ensuring provability.
Informal Reasoning. We use item difficulty (Crocker & Algina 1986), i.e., the proportion of LLMs who answer a question correctly (Pass@ 1), to measure the difficulty of each informalized problem-solving question. Due to space limitations, we report the average difficulty of the top-500 most difficult questions and overall questions in Tab. [ Appendix B details the performance of all evaluated models. Our top 500 problems are harder than AIME24, and the overall problems are more difficult than MATH500. Difficulty shares similar trends with complexity. The top-500 difficult problems of DExplorer are significantly harder than baselines (0.05 vs. 0.16). However, the overall problems are slightly easier than PromptCoT-QuQ and PromptCoT-DDS (0.45 and 0.40 vs. 0.47). As visualized in Fig. 2 among all complexity groups, our method generates more difficult problems (colored red) than any baselines and ablations. The seemingly easier overall difficulty is due to our method's capability to generate simple problems.
Diversity. Following Huang et al. 2024), we compute ROUGE-L 2004) on the informalized questions, answers, and solutions to measure the diversity of generation. For each experiment, we compute the average pair-wise ROUGE-L scores over 400 uniformly sampled data points. We report the average results from independent runs, resulting in a standard deviation of S 0.003 for each method. All methods' Rouge-L, scores are below 0.25, indicating high generation diversity. Our methods consistently demonstrate lower Rouge-L (higher diversity) than baselines (0.173 vs. 0.186 for PrompiCoT-DS), Although fine-tuned from the same model on the same datasets, DExplorer is slightly more diverse than Conjecturer- Prover (0.173 vs. 0.174). This improvement may be explained by the fact that Conjecturer-Proot generates fewer high-complex and difficult statements, as demonstrated in Fig.
Efficiency. We measure generation efficiency by proven rate, contradictory rate, and success rate (the portion of proven, contradictory, and valid statements among all generated ones), and token cosr(the average number of generated tokens for each valid statement). DExplorer still demon- strates a drastically higher proven rate (64.18% vs. 47.38% of ScaleQuest-Math) and success rate (54.52% vs. 40.70% of ScaleQuest-Math), lower contradictory rate (9.94% vs. 14.58% of CompptCoT-QQQ) with magnitude-lower token cost (8.8K vs. 187K of Conjecturer-Provert No- tably, the reported cost of MUSTARD does not include the cost of generating informal problems, informal proofs, and autoformalization. The reported costs of PromptCoT-QwQQ PromptCoT-DSS and ScaleQuest-Mare also do not include the cost of generating informal question-anse -answer pairs. Therefore, the actual cost of the basclines is significantly higher than the reported cost. As shown in Fig. 2 the generated statements of our method span a wide spectrum of complexity and difficulty, whereas ScaleQuest-Mar -ath and MUSTARD concentrate on generating easier problems, PromptCoT- DS and PromptCoT-Qwe focus on harder problems. DExplorer generates more difficult problems than baselines and ablations.
Pareto-Optine Oateet-Optimality. By adjusting the step limit N, among {4, 16, 32, 80} of DExplorer and the proof limit Np among (1,2, 4, 8, 12) for prover-based methods, we further investigate the perfor-
8

---

Published as a conference paper at ICLR 2026
Success Rate (96)
FremprCat
40
TrungCCol US
Success
Carjesture Prover
20
DEbaien (Staed!
BExp
1500
Itam Difficuity (- Difffcuk) Complexity
1000
500
1.00
0.00
10a
10
10 Total Token Cost
10
10
Figure 3: Results of cost-controlled experiments. (a) Success rate across total token costs. (b)
Distribution of formal statements' complexity across total token costs. Widths are proportionally scaled to the success rate. (c) Distribution of informal problem-solving questions' item difficulty across total token costs. Lower indicates more difficult. Widths are proportionally scaled to number of valid statements.
mance of different methods under different computational budgets. The success rate curves total token costs are visualized in Fig. 3a), where DExplorer demonstrates pareto-optimality com- pared with all baselines. Even under an unfair comparison, where the token costs of baseline meth- ods are significantly underestimated, DExplorer requires orders of magnitude lower computational cost to reach the same level of success rate: 0.13x that of ScaleQuest- PromptCo'T and Conjecturer-Proott Prover. The distribution of complexity to formal methods and difficulty to informal methods across different total token costs shown in Fig. 3b) and Fig. 3(c), respec- tively. DExplorer shows strong cost-effectiveness over all baselines by generating more samples at all complexity levels, except ScaleQuest-Maii The distribution of ScaleQuest-Math concentrates on simpler statements with complexity 500 item difficulty > 0.75. Ours is more balanced and generates more than any baseline for complexity > 500 or item difficulty < 0.25 (harder), with a 0.09x of Conjecturer-Prover With increasing total cost, our methods exhibit clear distribu- tion shifts towards more complex and difficult problems, which are discussed Appendix C and illustrated in Fig.
and < 0.1 that of
Ablation. Comparisons to Conjecturer-Prover shows all-around superiority of DExplorer, includ- ing higher proving rate 731.78% + 64.18%), lower contradictory rate (36.34% + 9.94%), higher success rate (23.28% + 54.52%), lower token cost (187K + 8.8K). more complex generations (Fig. . lower average item difficulty (0.52 + 0.47, lower is more difficult). and lower Rouge-L (0.174 + 073, lower is more diverse). and better cost-effectiveeess (Fig. 3()) Note that Conjecturer-Prove and DExplorer are fine-tuned using the same model, dataset, and hyperparam- eters. This ablation suggests that the advantages of DExplorer are not attributed to the dataset but to the reasoning architecture. By decomposing mathematical conjecturing into step-by-step explo- ration, the logical gaps between conditions and conclusions narrowed, and the requirement of external provers is eliminated.
Ablative experiments of the DExplorer (Staged), which restricts the DExplorer to staged exploration, also show inferior or on-par performance compared to the original method across all aspects. How- ever, as in Fig. a)) in an extremely low budget scenario where the total cost 106.5 (step limit N, < 8), the ablation slightly outperforms the main method on success rate. This may be explained by the fact that staged exploration prefers shallower exploration since it prohibits introducing new variables and hypotheses upon deduction.

---

Published as a conference paper at ICLR 2026
CONCLUSION
This paper aims to synthesize provable formal statements with efficiency, complexity, difficulty, and diversity. We identify expressiveness-valine methods and locate one root cause: reliance on external reasoners. To break the trilemma, we pro- pose end-to-end verified framework. DExploration (Deductive Exploration). Instead of directly synthesizing problems, DExploration enables agents to explore the mathematical world and discover intriguing conclusions by supporting three atomic actions: introducing, deducing, and submitting- Once a conclusion is submitted, a provable statement is constructed by composing the introduced conditions and the submitted conclusion. We design Exploratory Transformation address data scarcity by transforming existing statement-pree proof pairs into exploration processes. Comparisons to strong baselines and thorough ablations validate the effectiveness and efficiency of our methods.
trilemma in existing problem synthesis
REPRODUCIBILITY STATEMENT
Our research aims to extend the applications of formal theorem proving to broader domains by proposing framework for effectively and efficiently synthesizing provable formal statements, as well as data bootstrapping method based on abundant theorem-pie pereeingrovviggg data. We appreciate and affirm the value of reproducibility in scientific research and therefore summarize the details of meth- ods, data, models, and experiments as follows:
The Lean dependencies and environment settings are detailed in Appendix F
The training recipe, inference hyperparameters, and generating settings are detailed Ap-
pendix [
Details about benchmarking informal reasoning, including the evaluated models, the evaluation toolkit, the pipeline for quality check, human evaluation result, and detailed evaluation results are in Appendix [B]
The Prompt templates for DExplorer, conjecturer, informalization, and informal reasoning are in
Appendix G
Evaluated methods and evaluating setting is detailed in Sec. 5.2
Moreover, will upload all generated statements and evaluation results as supplementary materi- als. Code, data, and models will be available after acceptance.
REFERENCES
Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A pachine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. arXiv preprint 24t.:24110.642999 2024.
Eser Aygün, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup. and Shibl Mourad. Learning to prove from synthetic theorems. arXiv preprint arXiv:2006. 1259, 2020.
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie. Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang. Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying. Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang. Ge Zhang, Tianyun Zhao Jianqiu Zhao, Yichi Zhou, and Thomas Han- wen Zhu. Seed-prover: Deep and broad reasoning for automated theorem proving, 2025. URL
https://arxti org. abs 2507. 23726
Hyeong Kyu Choi, Maxim Khanov, Hongxin Wei, and Yixuan Li. How contaminated is your bench- mark? quantifying dataset leakage in large language models with kemel divergence, 2025. URL.
https::/arxiss org. abs / 2502. 00678
XTuner Contributors. Xtuner: A toolkit for efficiently fine-tuning Ilm. htttss://ggthhbeee com/ InternLM/xtuner 2023.
Linda Crocker and James Algina. Introduction classical and modern test theory. ERIC, 1986.
10

---

Published as a conference paper at ICLR 2026
DeepSeek-AL. Deepscek-v3 technical report, 2024. 19437
URLLttto:///rxii.orr//bb////
DeepSeek-AL. Deepseek-v3.2-exg Boosting cong--onnextt with deepseek sparse attention, 2025.
DeLpSeek-AL, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang. Xingkai Yu, Yu Wu, F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei Feng. Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai Dai, Deli Chen, Dongjie Ji, Erhang Li, Fangyun Lin, Fucong Dai, Fuli Luo, Guangbo Hao, Guanting Chen, Guowei Li, H. Zhang. Han Bao, Hanwei Xu, Haocheng Wang. Honghui Ding, Huajian Xin, Huazuo Gao, Hui Qu, Hui Li, Jianzhong Guo, Jiashi Li, Jiawei Wang, Jingchang Chen, Jingyang Yuan, Junjie Qiu, Junlong Li, J. I.. Cai, Jiaqi Ni, Jian Liang, Jin Chen, Kai Dong, Kai Hu, Kaige Gao, Kang Guan, Kexin Huang, Kuai Yu, Lean Wang. Lecong Zhang, Liang Zhao, Litong Wang. Liyue Zhang, Lei Xu, Leyi Xia, Mingchuan Zhang, Minghua Zhang, Minghui Tang. Meng Li, Miaojun Wang, Mingming Li, Ning Tian, Panpan Huang, Peng Zhang, Qiancheng Wang, Qinyu Chen, Qiushi Du, Ruiqi Ge, Ruisong Zhang, Ruizhe Pan, Runji Wang, R. J. Chen, R. L. Jin, Ruyi Chen, Shanghao Lu, Shangyan Zhou, Shanhuang Chen, Shengfeng Ye, Shiyu Wang. Shuiping Yu, Shunfeng Zhou, Shuting Pan, S. S. Li, Shuang Zhou, Shaoqing Wu, Shengfeng Ye, Tao Yun, Tian Pei, Tianyu Sun, T. Wang. Wangding Zeng, Wanjia Zhao, Wen Liu, Wenfeng Liang. Wenjun Gao, Wenqin Yu, Wentao Zhang, W. L. Xiao, Wei An, Xiaodong Liu, Xiaohan Wang, Xiaokang Chen, Xiaotao Nie, Xin Cheng, Xin Liu, Xin Xie, Xingchao Liu, Xinyu Yang, Xinyuan Li, Xuecheng Su. Xuheng Lin, X. Q. Li, Xiangyue Jin, Xiaojin Shen, Xi- aosha Chen, Xiaowen Sun, Xiaoxiang Wang, Xinnan Song, Xinyi Zhou, Xianzu Wang, Xinxia Shan, Y. K. Li, Y. Q. Wang. Y. X. Wei, Yang Zhang, Yanhong Xu, Yao Li, Yao Zhao, Yaofeng Sun, Yaohui Wang, Yi Yu, Yichao Zhang. Yifan Shi, Yiliang Xiong, Ying He, Yishi Piao, Yisong Wang, Yixuan Tan, Yiyang Ma, Yiyuan Liu, Yongqiang Guo, Yuan Ou, Yuduan Wang, Yue Gong, Yuheng Zou, Yujia He, Yunfan Xiong, Yuxiang Luo, Yuxiang You, Yuxuan Liu, Yuyang Zhou, Y. X. Zhu, Yanhong Xu, Yanping Huang, Yaohui Li, Yi Zheng, Yuchen Zhu, Yunxian Ma, Ying Tang, Yukun Zha, Yuting Yan, Z. Z. Ren, Zehui Ren, Zhangli Sha. Zhe Fu, Zhean Xu, Zhenda Xie, Zhengyan Zhang, Zhewen Hao, Zhicheng Ma, Zhigang Yan, Zhiyu Wu, Zihui Gu, Zijia Zhu, Zijun Liu, Zilin Li, Ziwei Xie, Ziyang Song, Zizheng Pan, Zhen Huang, Zhipeng Xu, Zhongyu Zhang, and Zhen Zhang. Deepseek-rl: Incentivizing reasoning capability in llms via reinforce- ment learning, 2025. URL //axxiis:///xxv....t org/ /ww.////1... 12948
Yuyang Ding, Xinyu Shi, Xiaobo Liang, Juntao Li, Zhaopeng Tu, Qiaoming Zhu, and Min Zhang- Unleashing LLM reasoning capability via scalable question synthesis from scratch. In Wanx- iang Che. Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (eds.). Pro- ceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Vol- 1-414-13488 13438, Vienna, Austria, July 2025. Association for Com- putational Linguistics. ISBN 979- 19176-251-0.
ume 1: Long Pupers), pp. 13414
doi: 10. 111558/v12022..acc 658. URL 20w.g/2222...om long. 6587)
Kefan Dong and Tengyu Ma. Stp: Self-play IIm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.000211 2025.
Haim Elgrably and Roza Leikin. Creativity function of problem-solving expertise: Posing new problems through investigations. 1DM-Mathematics Education, 53(4):891-904, 2021.
Paul Ernest, Ole Skovsmose, Jean Paul Van Bendegem, Maria Bicudo, Roger Miarka, Ladislav Kvasz, and Regina Moeller. The philosophy of mathematics education. Springer Nature, 2016.
Daocheng Fu, Zijun Chen, Renqiu Xia, Qi Liu, Yuan Feng, Hongbin Zhou, Renrui Zhang, Shiyang Feng, Peng Gao, Junchi Yan, et al. Trustgeogen: Scalable and formal-verified data engine for trustworthy multi-moda geometric problem solving. arXiv preprint ar 25X4 2025.
Shahriar Golchin and Mihai Surdeanu. Time travel in lmms: Tracing data contamination in large language models, 2024. URL
wargg/abs.. abs/ 20...00493
Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan,
11

---

Published as a conference paper at ICLR 2026
Anirudh Goyal, Anthony Hartshom, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Ko- renev, Arthur Hinsvark. Arun Rao, Aston Zhang, Aurelien Rodriguez, Austen Gregerson, Ava Spataru, Baptiste Roziere, Bethany Biron, Binh Tang, Bobbie Chern, Charlotte Caucheteux, Chaya Nayak, Chloe Bi, Chris Marra, Chris McConnell, Christian Keller, Christophe Touret, Chunyang Wu, Corinne Wong. Cristian Canton Ferrer, Cyrus Nikolaidis, Damien Allonsius, Daniel Song, Danielle Pintz, Danny Livshits, Danny Wyatt, David Esiobu, Dhruv Choudhary, Dhruv Mahajan, Diego Garcia-Olano, Diego Perino, Dieuwke Hupkes, Egor Lakomkin, Ehab AlBadawy, Elina Lobanova, Emily Dinan, Eric Michael Smith, Filip Radenovic, Francisco Guzmán, Frank Zhang, Gabriel Synnaeve, Gabrielle Lee. Georgia Lewis Anderson, Govind That- tai, Graeme Nail, Gregoire Mialon, Guan Pang. Guillem Cucurell, Hailey Nguyen, Hannah Kore- vaar, Hu Xu, Hugo Touvron, Iliyan Zarov, Imanol Arrieta Ibarra, Isabel Kloumann, Ishan Misra, Ivan Eytimov, Jack Zhang, Jade Copet, Jaewon Lee, Jan Geffert, Jana Vranes, Jason Park, Jay Ma- hadeokar, Ject Shah, Jelmer van der Linde, Jennifer Billock, Jenny Hong, Jenya Lec, Jeremy Fu, Jianfeng Chi, Jianyu Huang, Jiawen Liu, Jie Wang, Jiecao Yu, Joanna Bitton, Joe Spisak, Jong- soo Park, Joseph Rocca, Joshua Johnstun, Joshua Saxe, Junteng Jia, Kalyan Vasuden Alwala, Karthik Prasad, Kartikeya Upasani, Kate Plawiak, Ke Li, Kenneth Heafield, Kevin Stone, Khalid El-Arini, Krithika Iyer, Kshitiz Malik, Kuenley Chiu, Kunal Bhalla, Kushal Lakhotia, Lauren Rantala-Yeary, Laurens van der Maaten, Lawrence Chen, Liang Tan, Liz Jenkins, Louis Martin, Lovish Madaan, Lubo Malo, Lukas Blecher, Lukas Landzaat, Luke de Oliveira, Madeline Muzzi, Mahesh Pasupuleti, Mannat Singh, Manohar Paluri, Marcin Kardas, Maria Tsimpoukelli, Mathew Oldham, Mathicu Rita. Maya Pavlova, Melanie Kambadur, Mike Lewis, Min Si, Mitesh Ku- mar Singh, Mona Hassan, Naman Goyal, Narjes Torabi, Nikolay Bashlykov, Nikolay Bogoy- chev, Niladri Chatterji, Ning Zhang. Olivier Duchenne, Onur Çelebi, Patrick Alrassy, Pengchuan Zhang, Pengwei Li, Petar Vasic. Peter Weng, Prajjwal Bhargava, Pratik Dubal, Praveen Krishnan, Punit Singh Koura, Puxin Xu, Qing He, Qingxiao Dong, Ragavan Srinivasan, Raj Ganapathy, Ra- mon Calderer, Ricardo Silveira Cabral, Robert Stojnic, Roberta Raileanu, Rohan Maheswari, Ro- hit Girdhar, Rohit Patel, Romain Sauvestre, Ronnie Polidoro, Roshan Sumbaly, Ross Taylor, Ruan Silva, Rui Hou, Rui Wang, Saghar Hosseini, Sahana Chennabasappa, Sanjay Singh, Sean Bell, Seohyun Sonia Kim, Sergey Edunov, Shaoliang Nie, Sharan Narang, Sharath Raparthy, Sheng Shen, Shengye Wan, Shruti Bhosale, Shun Zhang, Simon Vandenhende, Soumya Batra, Spencer Whitman, Sten Sootla Stephane Collot, Suchin Gururangan, Sydney Borodinsky, Tamar Herman, Tara Fowler, Tarek Sheasha, Thomas Georgiou, Thomas Scialom, Tobias Speckbacher, Todor Mi- haylov, Tong Xiao, Ujjwal Karn, Vedanuj Goswami, Vibhor Gupta, Vignesh Ramanathan, Viktor Kerkez, Vincent Gonguet, Virginie Do. Vish Vogeti, Vítor Albiero, Vladan Petrovic, Weiwei Chu, Wenhan Xiong, Wenyin Fu, Whitney Meers, Xavier Martinet, Xiaodong Wang. Xiaofang Wang, Xiaoqing Ellen Tan, Xide Xia, Xinfeng Xie, Xuchao Jia, Xuewei Wang. Yaelle Gold- schlag, Yashesh Gaur, Yasmine Babaei, Yi Wen, Yiwen Song. Yuchen Zhang, Yue Li, Yuning Mao, Zacharie Delpierre Coudert, Zheng Yan, Zhengxing Chen, Zoe Papakipos, Aaditya Singh, Aayushi Srivastava, Abha Jain, Adam Kelsey, Adam Shajnfeld, Adithya Gangidi. Adolfo Victoria, Ahuva Goldstand, Ajay Menon, Ajay Sharma, Alex Boesenberg, Alexei Baevski, Allie Feinstein, Amanda Kallet, Amit Sangani, Amos Teo, Anam Yunus, Andrei Lupu, Andres Alvarado, An- drew Caples, Andrew Gu, Andrew Ho, Andrew Poulton, Andrew Ryan, Ankit Ramchandani, An- nie Dong, Annie Franco, Anuj Goyal, Aparajita Saraf, Arkabandhu Chowdhury, Ashley Gabriel, Ashwin Bharambe, Assaf Eisenman, Azadeh Yazdan, Beau James, Ben Maurer, Benjamin Leon- hardi, Bernie Huang. Beth Loyd, Beto De Paola. Bhargavi Paranjape, Bing Liu, Bo Wu, Boyu Ni, Braden Hancock, Bram Wasti, Brandon Spence, Brani Stojkovic. Brian Gamido, Britt Mon- talvo, Carl Parker, Carly Burton, Catalina Mejia, Ce Liu, Changhan Wang, Changkyu Kim, Chao Zhou, Chester Hu, Ching-Hsiang Chu, Chris Cai, Chris Tindal, Christoph Feichtenhofer, Cynthia Gao, Damon Civin, Dana Beaty. Daniel Kreymer, Daniel Li, David Adkins, David Xu, Davide Testuggine, Delia David, Devi Parikh, Diana Liskovich, Didem Foss, Dingkang Wang, Due Le, Dustin Holland, Edward Dowling, Eissa Jamil, Elaine Montgomery, Eleonora Presani, Emily Hahn, Emily Wood, Tuan-TuanLee Le, Erik Brinkman, Esteban Arcaute, Evan Dunbar, Evan Smoth- ers, Fei Sun, Felix Kreuk, Feng Tian, Filippos Kokkinos, Firat Ozgenel, Francesco Caggioni, Frank Kanayet, Frank Seide, Gabriela Medina Florez, Gabriella Schwarz, Gada Badeer, Georgia Swee, Gil Halpern, Grant Herman, Grigory Sizov, Guangyi, Zhang, Guna Lakshminarayanan, Hakan Inan, Hamid Shojanazeri, Han Zou, Hannah Wang, Hanwen Zha, Haroun Habeeb, Harri- son Rudolph, Helen Suk, Henry Aspegren, Hunter Goldman, Hongyuan Zhan, Ibrahim Damlaj, Igor Molybog. Igor Tufanov, Ilias Leontiadis, Irina- Veliche, Itai Gat, Jake Weissman, James Geboski, James Kohli, Janice Lam, Japhet Asher, -aptiitt Gaya, Jeff Mareus, Jeff Tang, Jen-
12

---

Published as a conference paper at ICLR 2026
nifer Chan, Jenny Zhen, Jeremy Reizenstein, Jeremy Teboul, Jessica Zhong, Jian Jin, Jingyi Yang, Joe Cummings, Jon Carvill. Jon Shepard, Jonathan McPhie, Jonathan Torres, Josh Ginsburg, Jun- jie Wang. Kai Wu, Kam Hou U, Karan Saxena, Kartikay Khandelwal, Katayoun Zand, Kathy Matosich, Kaushik Veeraraghavan, Kelly Michelena, Keqian Li, Kiran Jagadeesh, Kun Huang, Kunal Chawla, Kyle Huang, Lailin Chen, Lakshya Garg, Lavender A, Leandro Silva, Lee Bell, Lei Zhang. Liangpeng Guo, Licheng Yu, Liron Moshkovich, Luca Wehrstedt, Madian Khabsa, Manav Avalani, Manish Bhatt, Martynas Mankus, Matan Hasson, Matthew Lennie, Matthias Reso, Maxim Groshev, Maxim Naumov, Maya Lathi, Meghan Keneally, Miao Liu, Michael L. Seltzer, Michal Valko, Michelle Restrepo, Mihir Patel, Mik Vyatskov, Mikayel Samvelyan, Mike Clark, Mike Macey, Mike Wang, Miquel Jubert Hermoso, Mo Metanat, Mohammad Rastegari, Munish Bansal, Nandhini Santhanam, Natascha Parks, Natasha White, Navyata Bawa, Nayan Singhal, Nick Egebo, Nicolas Usunier, Nikhil Mehta, Nikolay Pavlovich Laptev, Ning Dong, Norman Cheng, Oleg Chernoguz, Olivia Hart, Omkar Salpekar. Ozlem Kalinli, Parkin Kent, Parth Parckh, Paul Saab, Pavan Balaji. Pedro Rittner, Philip Bontrager, Pierre Roux, Piotr Dollar, Polina Zvyagina, Prashant Ratanchandani, Pritish Yuvraj, Qian Liang, Rachad Alao, Rachel Ro- driguez, Rafi Ayub, Raghotham Murthy, Raghu Nayani, Rahul Mitra, Rangaprabhu Parthasarathy, Raymond Li, Rebekkah Hogan, Robin Battey, Rocky Wang. Russ Howes, Ruty Rinott, Sachin Mehta, Sachin Siby. Sai Jayesh Bondu, Samyak Datta, Sara Chugh, Sara Hunt, Sargun Dhillon, Sasha Sidorov. Satadru Pan. Saurabh Mahajan, Saurabh Verma, Seiji Yamamoto, Sharadh Ra- maswamy. Shaun Lindsay. Shaun Lindsay, Sheng Feng. Shenghao Lin, Shengxin Cindy Zha, Shishir Patil, Shiva Shankar. Shuqiang Zhang, Shuqiang Zhang, Sinong Wang, Sneha Agarwal, Soji Sajuyighe, Soumith Chintala, Stephanie Max, Stephen Chen, Steve Kehoe, Steve Satter- field, Sudarshan Govindaprasad, Sumit Gupta, Summer Deng, Sungmin Cho, Sunny Virk, Suraj Subramanian, Sy Choudhury, Sydney Goldman, Tal Remez, Tamar Glaser, Tamara Best, Thilo Koehler, Thomas Robinson, Tianhe Li, Tianjun Zhang, Tim Matthews, Timothy Chou, Tzook Shaked, Varun Vontimitta, Victoria Ajayi, Victoria Montanez, Vijai Mohan, Vinay Satish Ku- mar, Vishal Mangla, Vlad Ionescu, Vlad Poenaru, Vlad Tiberiu Mihailescu, Vladimir Ivanov, Wei Li, Wenchen Wang, Wenwen Jiang. Wes Bouaziz, Will Constable, Xiaocheng Tang, Xiao- jian Wu, Xiaolan Wang, Xilun Wu, Xinbo Gao, Yaniv Kleinman, Yanjun Chen, Ye Hu, Ye Jia, Ye Qi, Yenda Li, Yilin Zhang, Ying Zhang, Yossi Adi, Youngjin Nam, Yu, Wang, Yu Zhao, Yuchen Hao, Yundi Qian, Yunlu Li, Yuzi He, Zach Rait, Zachary DeVito, Zef Rosnbrick, Zhao- duo Wen, Zhenyu Yang. Zhiwei Zhao, and Zhiyu Ma. The llama 3 herd of models, 2024. URL pettps://arxxr org/ wwwgg//b///aae /oo.////0000 21783
William A Howard et al. The formulae-as-tyee tssttssttssyyytyys notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 14:479-490 1980.
Yichen Huang and Lin F. Yang. Gemini 2.5 pro capable of winning gold at imo 2025, 2025, URL aaw.vv..vvv...////a//aaa/aaaaav. 2ttg//b/225000 15855
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. Mustard: Mastering uniform synthesis of theorem and proof data. arXiv preprint 2tX.::2402.08957 2024.
Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chap- lot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix, and William El Sayed. Mistral 7b, 2023. URL https:
//arxiv.org/abs//21100 06825
Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng. Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention, 2023. URL. htt.tttts:///// /ttp/v/iivvvv/////vv///eeeeaaaav org/ absg///b///// 2309. 06180 80
Joshua Ong Jun Leang, Giwon Hong, Wenda Li, and Shay B Cohen. Theorem prover as a judge for synthetic data generation. arXiv preprint vrXiv:2502.13137 2025.
lcanprover-oommunity Mathport is a tool for porting lean3 projects to lean4, 2024. URL http:: //withub..com//eanprr.tt communt by bt/mathportttttttttoooooo Accessed: 2024-11-22.
13

---

Published as a conference paper at ICLR 2026
Chengpeng Li, Zheng Yuan, Hongyi Yuan, Guanting Dong, Keming Lu, Jiancan Wu, Chuanqi Tan, Xiang Wang, and Chang Zhou. Query and response augmentation cannot help out-of- domain math reasoning generalization, 2024a.
net.:/...eeeeeeeeeeeeeeeeee forum?
Td=Nihk66bzz
Yang Li, Zhichen Dong, Yuhan Sun, Weixun Wang. Shaopan Xiong, Yijia Luo, Jiashun Liu, Han Lu, Jiamang Wang, Wenbo Su, et al. Attention illuminates IIm reasoning: The geelan-and-annhhe rhythm enables fine-grainet policy optimization. arXiv preprint arXiv:2510.13354 2025a.
Yang Li, Jiale Ma. Yebin Yang, Qitian Wu, Hongyuan Zha, and Junchi Yan. Generative modeling reinvents supervised learning: Label repurposing with predictive consistency learning, In Forty- second International Conference on Machine Learning. 2025b.
Zenan Li, Zhi Zhou, Yuan Yao, Xian Zhang, Yu-Feng Li, Chun Cao, Fan Yang, and Xiaoxing Ma.
Neuro-symbolic data generation for math reasoning. Advances in Neural Information Processing Systems, 17:23488-23511 2024b.
Peter Liljedahl and Jinfa Cai. Empirical research on problem solving and problem posing: A look at the state of the art. ZDM-Mahhemttiss Education, 53(4):723-735, 2021.
Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pp. 253-266, New York, NY, USA, 2023. Association for Computing Machin- ery. ISBN 9798400700262.
doi: 10.1145/3573105.335 3557666... URL https:://o..org/////
05 3575677
Chin-Yew Lin. Rouge: A package for automatic evaluation of summaries. In Text summarization branches out, pp. 74-11, 2004.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung. Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang. Hongzhou Lin, Yejin Choi, Dançi Chen, Sanjeev Arora, and Chi Jin. Goedel-prec predel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025. URL httptt::
//arxiv. org abs/ 2508 03613
Chris Yuhao Liu, Liang Zeng, Yuzhen Xiao, Jujie He, Jiacai Liu, Chaojie Wang, Rui Yan, Wei Shen, Fuxiang Zhang, Jiacheng Xu, Yang Liu, and Yahui Zhou. Skywork- Scaling preference data curation via human-ai synergy. arXiv preprint arXiv:2507.01355. 2025.
Rujiao Long, Yang Li, Xingyao Zhang, Weixun Wang, Tianqiajiin Lin, Xi Zhao, Yuchi Xu, Wenbo Su, Junchi Yan, and Bo Zheng. Reasoning palette: Modulating reasoning via latent contextual- ization for controllable exploration for (v) lms. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, 2026.
Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qing- wei Lin, Shifeng Chen, and Dongmei Zhang. Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.0955 2023.
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367-381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 978 9781450370999 doi: 10.1145/ 3372885.337382 URL httphhtttt// http::///ooo.rg//o..o/oo 01t...111/133118.1111 2372888888338883
Microsoft, AbdeIrahman Abouclenin, Atabak Ashfaq, Adam Atkinson, Hany Awadalla, Nguyen Bach, Jianmin Bao, Alon Benhaim, Martin Cai, Vishrav Chaudhary, Congcong Chen, Dong Chen, Dongdong Chen, Junkun Chen, Weizhu Chen, Yen-Chun Chen, Yi ling Chen, Qi Dai, Xiyang Dai, Ruchao Fan, Mei Gao, Min Gao, Amit Garg, Abhishek Goswami, Junheng Hao, Amr Hendy, Yuxuan Hu, Xin Jin, Mahmoud Khademi, Dongwoo Kim, Young Jin Kim. Gina Lee, Jinyu Li, Yunsheng Li, Chen Liang. Xihui Lin, Zeqi Lin, Mengehen Liu, Yang Liu, Gilsinia Lopez, Chong Luo, Piyush Madan, Vadim Mazalov, Arindam Mitra, Ali Mousavi, Anh Nguyen, Jing Pan, Daniel Perez-Becd Becker, Jacob Platin, Thomas Portet, Kai Qiu, Bo Ren. Liliang Ren, Sambuddha Roy, Ning Shang, Yelong Shen, Saksham Singhal, Subhojit Som, Xia Song, Tetyana Sych, Praneetha
14

---

Published as a conference paper at ICLR 2026
Vaddamanu, Shuohang Wang, Yiming Wang, Zhenghao Wang. Haibin Wu, Haoran Xu, Weijian Xu, Yifan Yang, Ziyi Yang. Donghan Yu, Ishmam Zabir, Jianwen Zhang, Li Lyna Zhang, Yunan Zhang, and Xiren Zhou. Phi-4-mini technical report: Compact yet powerful multimodal language models via mixture-of- loras, 2025. URL CtILhhtps:// http::///axww..oo//poo/./o
Leonardo de Moura and Sebastian Ulrrich. The lean 4 theorem prover and programming language. In Automated Deduction-CAle 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
Team OLMo, Pete Walsh, Luca Soldaini, Dirk Groeneveld, Kyle Lo, Shane Arora, Akshita Bha- gia, Yuling Gu. Shengyi Huang, Matt Jordan, Nathan Lambert, Dustin Schwenk, Oyvind Tafjord, Taira Anderson, David Atkinson, Faeze Brahman, Christopher Clark, Pradeep Dasigi, Nouha Dziri, Michal Guerquin, Hamish Ivison, Pang Wei Koh, Jiacheng Liu, Saumya Malik, William Merrill, Lester James V. Miranda, Jacob Morrison, Tyler Murray, Crystal Nam, Valentina Py- atkin, Aman Rangapur, Michael Schmitz, Sam Skjonsberg, David Wadden, Christopher Wilhelm, Michael Wilson, Luke Zettlemoyer, Ali Farhadi, Noah A. Smith, and Hannaneh Hajishirzi. 2 olmo 2 furious. 2024. URL https: wrw.a. org/ abs 2501. 0066
Naoto Onda, Kazumi Kasaura, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, and Sho Sonoda. Leanconjecturee: Automatic generation of mathematical conjectures for theorem proving, 2025.
URL httpttsss///xxi...o.m
org/ /t..a////50 22005
OpenAl, Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, Ally Bennett, Ananya Kumar, Andre Saraiva, Andrea Vallone, Andrew Duberstein, Andrew Kondrich, Andrey Mishchenko, Andy Applebaum, Angela Jiang, Ashvin Nair, Barret Zoph. Behrooz Ghor- bani, Ben Rossen, Benjamin Sokolowsky, Boaz Barak, Bob McGrew, Borys Minaiev, Botao Hao, Bowen Baker, Brandon Houghton, Brandon McKinzie, Brydon Eastman, Camillo Lugaresi, Cary Bassin, Cary Hudson, Chak Ming Li, Charles de Bourcy, Chelsea Voss, Chen Shen, Chong Zhang, Chris Koch, Chris Orsinger, Christopher Hesse, Claudia Fischer, Clive Chan, Dan Roberts, Daniel Kappler, Daniel Levy, Daniel Selsam, David Dohan, David Farhi, David Mely, David Robinson, Dimitris Tsipras, Doug Li, Dragos Oprica, Eben Freeman, Eddie Zhang, Edmund Wong, Eliz- abeth Prochl, Enoch Cheung, Eric Mitchell, Eric Wallace, Erik Ritter. Evan Mays, Fan Wang, Felipe Petroski Such, Filippo Raso, Florencia Leoni, Foivos Tsimpourlas, Francis Song, Fred von Lohmann, Freddie Sulit, Geoff Salmon, Giambattista Parascandolo, Gildas Chabot, Grace Zhao, Greg Brockman, Guillaume Leclere, Hadi Salman, Haiming Bao, Hao Sheng, Hart An- drin, Hessam Bagherinezhad, Hongyu Ren, Hunter Lightman, Hyung Won Chung, Ian Kivlichan, Ian O'Connell, Ian Osband, Ignasi Clavera Gilaberte, Ilge Akkaya, Ilya Kostrikov, Ilya Sutskever, Irina Kofman, Jakub Pachocki, James Lennon, Jason Wei, Jean Harb, Jerry Twore, Jiacheng Feng, Jiahui Yu, Jiayi Weng, Jie Tang, Jieqi Yu, Joaquin Quiñonero Candela, Joe Palermo, Joel Parish, Johannes Heidecke, John Hallman, John Rizzo, Jonathan Gordon, Jonathan Uesato, Jonathan Ward, Joost Huizinga, Julie Wang, Kai Chen, Kai Xiao, Karan Singhal, Karina Nguyen, Karl Cobbe, Katy Shi, Kayla Wood, Kendra Rimbach, Keren Gu-Lemberg, Kevin Liu, Kevin Lu, Kevin Stone, Kevin Yu, Lama Ahmad, Lauren Yang. Leo Liu, Leon Maksin, Leyton Ho, Liam Fedus, Lilian Weng, Linden Li, Lindsay McCallum, Lindsey Held, Lorenz Kuhn, Lukas Kon- draciuk, Lukasz Kaiser, Luke Metz, Madelaine Boyd, Maja Trebacz, Manas Joglekar, Mark Chen, Marko Tintor, Mason Meyer, Matt Jones, Matt Kaufer, Max Schwarzer, Meghan Shah, Mehmet Yatbaz, Melody Y. Guan, Mengyuan Xu, Mengyuan Yan. Mia Glaese, Mianna Chen, Michael Lampe, Michael Malek, Michele Wang, Michelle Fradin, Mike McClay, Mikhail Pavlov, Miles Wang, Mingxuan Wang. Mira Murati, Mo Bavarian, Mostafa Rohaninejad, Nat McAleese, Neil Chowdhury, Neil Chowdhury, Nick Ryder, Nikolas Tezak, Noam Brown, Ofir Nachum, Oleg Boiko, Oleg Murk, Olivia Watkins, Patrick Chao, Paul Ashbourne, Pavel Izmailov, Peter Zhokhov, Rachel Dias, Rahul Arora, Randall Lin, Rapha Gontijo Lopes, Raz Gaon, Reah Miyara, Reimar Leike, Renny Hwang, Rhythm Garg, Robin Brown, Roshan James, Rui Shu, Ryan Cheu, Ryan Greene, Saachi Jain, Sam Altman, Sam Toizer, Sam Toyer, Samuel Miserendino, Sandhini Agar- wal, Santiago Hernandez. Sasha Baker, Scott McKinney, Scottie Yan, Shengjia Zhao, Shengli Hu, Shibani Santurkar, Shraman Ray Chaudhuri, Shuyuan Zhang, Siyuan Fu, Spencer Papay, Steph Lin, Suchir Balaji, Suvansh Sanjeev, Szymon Sidor, Tal Broda, Aidan Clark, Tao Wang. Tay- lor Gordon, Ted Sanders, Tejal Patwardhan, Thibault Sottiaux, Thomas Degry, Thomas Dimson,
15

---

Published as a conference paper at ICLR 2026
Tianhao Zheng, Timur Garipov, Tom Stasi, Trapit Bansal, Trevor Creech, Troy Peterson, Tyna Eloundou, Valerie Qi, Vineet Kosaraju, Vinnie Monaco. Vitchyr Pong. Vlad Fomenko, Weiyi Zheng, Wenda Zhou, Wes McCabe, Wojeiech Zaremba, Yann Dubois, Yinghai Lu, Yining Chen, Young Cha, Yu Bai, Yuchen He, Yuchen Zhang, Yunyun Wang. Zheng Shao, and Zhuohan Li. Openai ol system card, 2024a. URL
org/ abs 2412 16720
OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Floren- cia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Moham- mad Bavarian, Jeff Belgum, Irwan Bello, Jake Berdine, Gabriel Bernadett-Shapiro, Christopher Berner, Lenny Bogdonoff, Oleg Boiko, Madelaine Boyd, Anna-Luisa Brakman, Greg Brock- man, Tim Brooks, Miles Brundage, Kevin Button, Trevor Cai, Rosie Campbell, Andrew Cann, Brittany Carey, Chelsea Carlson, Rory Carmichael, Brooke Chan, Che Chang. Fotis Chantzis, Derek Chen, Sully Chen, Ruby Chen, Jason Chen, Mark Chen, Ben Chess, Chester Cho, Casey Chu, Hyung Won Chung, Dave Cummings, Jeremiah Currier, Yunxing Dai, Cory Decareaux, Thomas Degry, Noah Deutsch, Damien Deville, Arka Dhar, David Dohan, Steve Dowling, Sheila Dunning, Adrien Ecoffet, Atty Eleti, Tyna Eloundou, David Farhi, Liam Fedus. Niko Felix, Simón Posada Fishman, Juston Forte, Isabella Fulford, Leo Gao, Elie Georges, Christian Gib- son, Vik Goel, Tarun Gogineni, Gabriel Goh, Rapha Gontijo-Lopes, Jonathan Gordon, Morgan Grafstein, Scott Gray, Ryan Greene, Joshua Gross, Shixiang Shane Gu, Yufei Guo, Chris Hal- lacy, Jesse Han, Jeff Harris, Yuchen He, Mike Heaton, Johannes Heidecke, Chris Hesse, Alan Hickey, Wade Hickey, Peter Hoeschele, Brandon Houghton, Kenny Hsu, Shengli Hu, Xin Hu, Joost Huizinga, Shantanu Jain, Shawn Jain, Joanne Jang, Angela Jiang, Roger Jiang, Haozhun Jin, Denny Jin, Shino Jomoto, Billie Jonn, Heewoo Jun, Tomer Kaftan, Lukasz Kaiser, Ali Ka- mali, Ingmar Kanitscheider, Nitish Shirish Keskar, Tabarak Khan, Logan Kilpatrick, Jong Wook Kim, Christina Kim, Yongjik Kim, Jan Hendrik Kirchner, Jamie Kiros, Matt Knight, Daniel Kokotajlo, Lukasz Kondraciuk, Andrew Kondrich, Aris Konstantinidis, Kyle Kosic, Gretchen Krueger, Vishal Kuo, Michael Lampe, Ikai Lan, Teddy Lee, Jan Leike, Jade Leung, Daniel Levy, Chak Ming Li, Rachel Lim, Molly Lin, Stephanie Lin, Mateusz Litwin, Theresa Lopez, Ryan Lowe, Patricia Lue, Anna Makanju, Kim Malfacini, Sam Manning, Todor Markov, Yaniv Markovski, Bianca Martin, Katie Mayer, Andrew Mayne, Bob McGrew, Scott Mayer McKinney, Christine McLeavey, Paul McMillan, Jake McNeil. David Medina, Aalok Mehta, Jacob Menick, Luke Metz, Andrey Mishchenko, Pamela Mishkin, Vinnie Monaco, Evan Morikawa, Daniel Mossing, Tong Mu, Mira Murati, Oleg Murk, David Mély, Ashvin Nair, Reiichiro Nakano, Ra- jeev Nayak, Arvind Neelakantan, Richard Ngo. Hyeonwoo Noh, Long Ouyang, Cullen O' Oeeeffe, Jakub Pachocki, Alex Paino, Joe Palermo, Ashley Pantuliano, Giambattista Parascandolo, Joel Parish, Emy Parparita, Alex Passos, Mikhail Pavlov, Andrew Peng, Adam Perelman, Filipe de Avila Belbute Peres, Michael Petrov, Henrique Ponde de Oliveira Pinto, Michael, Pokorny, Michelle Pokrass, Vitchyr H. Pong, Tolly Powell, Alethea Power, Boris Power, Elizabeth Proehl, Raul Puri, Alec Radford, Jack Rae, Aditya Ramesh, Cameron Raymond, Francis Real, Kendra Rimbach, Carl Ross, Bob Rotsted, Henri Roussez, Nick Ryder, Mario Saltarelli, Ted Sanders, Shibani Santurkar, Girish Sastry, Heather Schmidt, David Schnurr. John Schulman, Daniel Sel- sam, Kyla Sheppard, Toki Sherbakov, Jessica Shich, Sarah Shoker, Pranav Shyam. Szymon Sidor, Eric Sigler, Maddie Simens, Jordan Sitkin, Katarina Slama, Ian Sohl, Benjamin Sokolowsky, Yang Song, Natalie Staudacher, Felipe Petroski Such, Natalie Summers, Ilya Sutskever, Jie Tang, Nikolas Tezak, Madeleine B. Thompson, Phil Tillet, Amin Tootoonchian, Elizabeth Tseng, Pre- ston Tuggle, Nick Turley, Jerry Tworek, Juan Felipe Cerón Uribe, Andrea Vallone, Arun Vi- jayvergiya, Chelsea Voss, Carroll Wainwright, Justin Jay Wang, Alvin Wang, Ben Wang, Jonathan Ward, Jason Wei, CJ Weinmann, Akila Welihinda, Peter Welinder, Jiayi Weng, Lilian Weng, Matt Wiethoff, Dave Willner, Clemens Winter, Samuel Wolrich, Hannah Wong, Lauren Work- man, Sherwin Wu, Jeff Wu, Michael Wu, Kai Xiao, Tao Xu, Sarah Yoo, Kevin Yu, Qiming Yuan, Wojciech Zaremba, Rowan Zellers, Chong Zhang, Marvin Zhang, Shengjia Zhao Tianhao Zheng, Juntang Zhuang, William Zhuk, and Barret Zoph. Gpt-4 technical report, 2024b. URL https://arxxt org abs http://b//2333..0 2303
Gabriel Poesia, David Broman, Nick Haber, and Noah Goodman. Learning formal mathematics from intrinsic motivation. Advances in Neural Information Processing Systems, 43057,, 2024.
George Polya. Mathematics and plausible reasoning: Logic, symbolic and mathematical. 2021.
16

---

Published as a conference paper at ICLR 2026
Yury Puzis, Yi Gao, and Geoff Sutcliffe. Automated generation of interesting theorems. In FLAIRS, pp. 49-54, 2006.
Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang. Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao. Daya Guo, and Chong Ruan. provveek-- Advancing for- mal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025. URL
https://arx:t .rg/ 2504 21801
Joseph Rotella, Zhizhen Qin, Aidan Z.H. Yang, Brando Miranda, Mohamed El Amine Seddik, Jing- wei Zuo, Hakim Hacid, Leonardo de Moura, Soonho Kong, and Shi Hu. Synthetic theorem generation in lean, 2025. URL pttetpss//operreviiee http:/iwwwwwwweeeeeeeeeeeeeeeeee wwt. foatt/form?iii (is.rummdddd
Edward A Silver. On mathematical problem posing, For the learning of mathematics, 14(1):19-28, 1994.
Benedikt Stroebl, Sayash Kapoor, and Arvind Narayanan. Inference scaling flaws: The limits of I1m resampling with imperfect verifiers, 2024.
17501
Zhengyang Tang, Xingxing Zhang, Benyou Wang, and Furu Wei. Mathscale: Scaling instruction tuning for mathematical reasoning, 2024. URL
HuggingFace Team.
Math-verify, 2025a.
URL http:://gittuubb.omm/uugggggg//
Qwen Team. Qwen3 technical report, 2025b. URL http://ss//aarxv.oooro/////////a
Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476-482. 2024.
Pablo Villalobos, Anson Ho, Jaime Sevilla, Tamay Besiroglu, Lennart Heim, and Marius Hobbhahn.
Will we run out of data? limits of Ilm scaling based on numan-generadl data, 2024. URL
https://arxiie http:///xxxxvv.rg//eee abs 2211 04325
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song. Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmick
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-prone prover preview: Towards large formal reasoning models with reinforce- ment learning, 2025a.
http:///wxxw...occab///b//////// 11354
Lei Wang, Ruobing Zuo, Gaolei He, Jianlin Wang, and Zhengfeng Yang. Qdtsynth: Quality-driver formal theorem synthesis for enhancing proving performance of llms. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp- 14683-14698, 2025b.
Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, and Ping Wei. Alchemy: Amplifying theorem- proving capability through symbolic mutation. arXiv preprint wrXiv:2410.157453 2024.
Ruijie Xu, Zengzhi Wang, Run-Ze Fan, and Pengfei Liu. Benchmarking benchmark leakage in large language models, 2024. URL
abs///b///// htt.b///444482//2
An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, Keming Lu, Mingfeng Xue, Runji Lin, Tianyu Liu, Xingzhang Ren, and Zhenru Zhang. Qwen2.5 5-tth technical report: Toward mathematical ex- pert model via self-improvement, 2024. URL http://ss///aiii.../r
2409. 12122
Yebin Yang. Huaijin Wu, Fu Guo, Lin Yao, Xiaohan Qin, Jingzhi Wang, Debing Zhang, and Junchi Yan. Jtok: On token embedding as another axis of scaling law via joint token self-mor modulation. arXiv preprint arX arXiv: 00800, 2026.
17

---

Published as a conference paper at ICLR 2026
Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhen- guo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint 1.Xiv:2309.1228. 2023.
Terry Jingehen Zhang, Wenyuan Jiang, Rongchuan Liu, Yisong Wang, Junran Yang, Ning Wang, Nicole Ni, Yinya Huang, and Mrinmaya Sachan. Lean meets theoretical computer science: Scalable synthesis of theorem proving challenges in formal-informal pairs. arXiv preprint S.Xiv:2508.1887, 2025.
Xueliang Zhao, Wei Wu, Jian Guan, and Lingpeng Kong. PrompiCoT: Synthesizing olympiad- level problems for mathematical reasoning in large language models. Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (eds.), Findings of the Associa- tion for Computational Linguistics: ACL 2025, pp. 18167-18188, Vienna, Austria, July 2025. Association for Computational Linguistics. ISBN 979-8-89176-256-5 doi: 10.1 10.18653/v1/2055. findings-acl.935.
windiiis-nninnninnnnnnnn 935/
Kaijie Zhu, Jiaao Chen, Jindong Wang, Neil Zhenqiang Gong, Diyi Yang, and Xing Xie. Dyval: Dy- namic evaluation of large language models for reasoning tasks. arXiv preprint arXiv:2309 17167, 2023.
Kaijie Zhu, Jindong Wang, Qinlin Zhao, Ruochen Xu, and Xing Xie. Dynamic evaluation of large language models by meta probing agents. In Proceedings of the 41 International Conference on Machine Learning, pp. 62599-62661 2024.
A FORMAL PROOF OF RECONSTRUCTION CORRECTNESS
Let [s1, . ST] be the sequence exploration steps, where ST Submit(hy: : U). Let r; Fal se denote Lean proof state before step 8;, with [ 0. Vacuous steps 83 that [x+1 [x are neglected. The indices {1, 1....... of steps: I (Introduction) and D [Di, ....... Dm] (Deduction). For any t E 21,2, m), the step SD, is deductive tactic that transforms proof state I' I'D, | False to I D False. By the definition of Submit(). we have (hy U) E P For E I, S; introduces a new variable or hypothesis r++1 r, {(u; T.)}.
}} are partitioned into two disjoint lists based on the type
Statement Reconstruction. The reconstructed statement is formalised 1 - U, where I {(v) kE) represents the collection of all introduced variables and hypotheses throughout the exploration.
Proof Reconstruction. The reconstructed proof script is the sequence:
[Encapsulate(saa ( r D.,, I +1)l o [exact hr]
where the Encapsulate operation wraps the deductive tactic ensure context consistency.
The Encapsulate Operator. Given deductive step that transforms proof state I' + False to I' False, the operator Encapsulate(ss. 1 r, I\) represents the following Lean tactic sequence. It temporarily restricts the proof state match Т, executes 8, and then restores the wider context.
Denote the sets of declarations involved as:
Future Variables: r \ r {(u; T.) (variables introduced after the step s).
New Deductions: I' r {(h/ HDP
. Consumed Hypotheses: I' 1 {(h; H.) (hypotheses consumed/cleared by s).
have ALDDEUUCIOONNENAASSSIITIIO. := by The proof target U is hidden revert V1 1/2 ... Un Future Variables \ are hidden have H_DEDUCTION ENCAPSULATION := by The context is now ident i caal to r
18

---

Published as a conference paper at ICLR 2026
The context is now identical to I' exact (show (Hī H2 A ... H2) by exact (Mi, H2,, H())
intros
exact ILLEDDCTION ELDEUUCTIOLLENAAPSLLTTOOO
The derived facts clear M N22 ... N2 hu h2 ... by ILEEDUCTIONEENNASSAAAAATEET
consolidated
LH DEDDUCTTION BEW.SSULTTINAASS
reases _LDEDDCTION ENCAPSULATION with Hí, 1/2 lig
Apply changes from I to 1" in the current proof state
If the rcases simplifies to rename'.
rename' ILCEDUCTIOLL
h
Moreover, r 0, the double have DEDUCTIOON ENCAPSULATION encapsulation is not required.
have JL ENCAPSOLATION := by The proof target U is hidden The context is now identical to r
The context is now identical r' exact (show (Hi A H2 ... HT)) by exact (M, M2, RP))
The appl ication of changes from I to H is identical to above.
Correctness Proof. We prove by induction that for any k E {1....,m) m.. the proof state after executing the first k encapsulated steps from the initial proof state 1 | U is ((++1) |- U, where
r(++)) {(w; Ti))er D
Intuitively, the context of reconstructed proof state always the union of the corresponding exploration context and future variables.
Base Step. For the first encapsulated tactic, the proof state is [()) + U, where r(1) = r Since all previous steps are introducing steps, the exploration context of SD; is
PD, {(1x Te))KEINNEDD C r
Therefore,
ro (To (TD,)= =
i.e. the encapsulated execution context for sp, exactly I I'D Hence, the encapsulated tactic Encapsulate(#D,, T J[,, 11)+ transforms proof state (11) + U into ( | U, where
( = - (TD, UTDi+1 T.)erNNDD UTD++1
Inductive Step. Suppose the k-th encapsulated tactic transforms the proof state to
r(++)) = {(v: T:))EENI UTD+11
The exploration state for s $D44 is
T D {(u; T.) UT ((++))
Therefore,
p(++)) \ (To =T
ie., the encapsulated execution context for 8D411 is exactly I D Hence, the encapsulated tactic Encapsulate (8 &D ro, [ D I Detit1) transforms proof state [(++1] } U into ( + U. where
(k+2) p(++1) (I'DEs UT ((v T)) UI Ul
Therefore, the proof state after Dm (mm+1) } where
r(m+1)_ {(v; Ti) UT 2 l 2 {(ho UU)
The last tactic exact by finishes the proof.
19

---

Published as a conference paper at ICLR 2026
B BENCHMARKING INFORMAL REASONING
In this section, we evaluate the informalized problem-solving questions of each method with open- source models: Qwen3-8i -BB (Team] 2025b),
122--B-Insse In-sructtt (OLMo et al. 2024). Phi-4-mini-instruce (Microsoft al. 2025). OLMo-2-
(Jiang et al. (023), Llama-3.2-3B.
Instruct (Grattafiori al. 2024). and
(Grattafiori et al. 2024).
The evaluation
Yang et al. of commit We set the random seed to 0, the temperature to = and the Top-P 1. The prompt template is in Appendix
is conducted using the repo of Qwen2.5-Math in bttps://gi com httpo/////ww////////////em Qww./.
2024
We filter out informal problem-solving questions that 1) fail to parse by Hug- gingface Math-Verify (Team] 2025a); 2) The type/module of parsing results does not fall in {sympy. sympy.sets, sympy. myrpp...atricss.. sympy. functions).
SSympy.core.ne.. numbers,, Latex2sympy2_extenddeee hympy.core..o
core. add, sympy. wore. The filtered out types/modules sympy. . core wttpyyooorrrrllaionnns.e. www.reelliinna... sympy. core. symbol}.
include
Datee22yymy22exteeddee
sympy. cympy.core.c. containers,
Then, we manually checked 100 informalized problem-solving questions uniformly sampled from filtered data. 97 of them They completely correct, only are incorrect by misformulating exis- tence proof problems into problem-solving questions.
The evaluation results are summarized Table 2 Note that a lower item difficulty index indicates more difficult problems. The top-500 problems generated by our methods are significantly more difficult than baselines (15.57% 5.10%), and even more difficult than AIME24 (6.11%). Regarding all generated problems, since our methods generate significantly more than PromptCoT
Table 2: Performance of ooen-source LLMs on informalized problem-solving questions synthesized by base- line methods and our methods. Accuracies on reference benchmarks, top-500 problems, and all problems are reported. Difficulty: average item difficulty index (average accuracy across methods), lower more diffi- cult; Llama-3.2: I.lama-3.2-3B-Insst
Phi-4: Phi-4-mini-instriett, Mistral-v0.3: Mistral-7R--Insruut--dd OLMo-2: OLMo-2-1 In-stut-nst Llama-3.1: Mema-L-aama-3.1 1-------.1-B---mmm- -8BB-Instruct; Qwen3: Qwen3-8B, Bold numbers emphasize best values: Underlined numbers emphasize second-best values; Cyan numbers are abla-
tive improvement compared to Sinjecture-Proveed
Split
Benchunark
Size
Llama-3.2
Phi-4
Mistral-v0.3
OLMo-2
Llama-3.1
Qwen3
Difficulty
MultiArith
600
94.00%
97.83%
74.00%
92. 22.83%
94.83%
98.33%
91.97%
SVAMP
1000
82.90%
91.80%
50.50%
85.00 $5.00%
86.30%
94.00%
81.75%
GSM8K
1319
72.33%
89.01
51.10%
83. 70%
81.96%
93 93.25%
78.56%
GSM Symbolic
5000
66 20%
82.64%
40 60%
71.34%
77.70%
81.78%
70.04%
Official
MATH500
45.00%
66.20%
14.20%
35.80%
45.40%
80.20%
47.80%
AQUA
254
27.17%
37.80%
18.50%
15.35%
16.14%
84.65%
33.27%
OlympiadBench
675
14.96%
32.30%
4.30%
13.48%
16.00%
46.67%
21.28%
AIME24
30
3.33%
6,67%
3,33%
0.00%
6.67%
16.67%
6.11%
MUSTARD
500
20. 20.20%
14.00%
8.20%
13.00%
19.20%
8..
15.57%
ScaleQuest-
40.80%
18.20%
28.00%
28.00%
PrompiCoT-Qu QwQ
500
21.209
51.00%
6.80%
17.60%
20.20%
65 60%
30.40%
Top-500
PrompiCoT-DDS
224
39.73%
$8.48%
10.27%
31.25%
37.95%
64.29%
40.33%
Conjecture- Prover
500
51.80%
65.00%
25.009
45.80%
52.880%
68.0000 00.0
551.40%
DExplorer (Staged)
500
6.00%
17.20%
2.00%
2.80%
5.20%
22.40%
9.27%
DExplorer
2.40
6.80%
3.40%
3.20%
3.20%
11.60
5.10%
MUSTARD
2744
82.18%
83.67%
66.51%
80.83%
82.87%
84.62%
80,11%
ScaleQuest Math
1886
77.41%
84.09%
54.19%
73.17%
78. 74%74%
83.79%
75.57%
PrompiCoT-QWQ
683
40.26%
63.98%
15.37%
34.41%
38.95%
74.52%
44.58%
Overall
PromptCoT-DS
39.73%
58.48%
10.27%
31.25%
37.95%
64.29%%
40.33
Conjecture
65.28%
46.23%
53.17%
51.79%
DExplorer (Staged)
1093
46.57%
61.12%
21.68%
42.36%
48.76%
63.33
17.30%%
(1
DExplorer
1326
48.57%
60.86%
19.98%
39.82%
49.62%
63.95%
47. 17.113% 94000
20

---

Published as a conference paper at ICLR 2026
(1326 224), the overall is slightly easier (47.13% 40.33%), but is still more difficult than MATH500 (47.80) (47.80%)
Ablations validate the effectiveness of our methods. The top-500 difficulty improves 42.13% from Conjecturer-Prowt Provvrrr to DExplorer (Staged), and further 4.17% to DExplorer. The overall difficulty improves 4.49% and 4.66% to DExplorer (Staged) and DExplorer, respectively.
C DISTRIBUTION SHIFT
The distribution of formal statements' complexity and informal problem-solving questions' diffi- culty synthesized by all methods is visualized Fig. 4 5
respectively. All methods demonstrate distribution towards generating harder problems when total token costs improve. While baseline methods, including Conjecture-Provee only demonstrate mild change, distributions of our methods demonstrate clear shift to complex and difficult problems.
Canplooy
Camplory
P0015
Dandlolty
Toeoh Dal
Figure 4: Distribution of complexity shifts across different total token costs. (Top) Success rate total token costs. (Body) Distribution of formal statements' complexity across total token costs. Areas are normalized to be identical across experiments.
D TUBRICS-BASHR EVALUATION
To assess the mathematical value of the generated problems beyond binary correctness and proxy metrics (e.g., length), we conducted rubrics-based evaluation focusing on Clarity, Difficulty, Ele- gance, and Interestingness. We employ state-of-the-arr reward model (RM), Kkywork-Reward-aa Llama-3.1-88 1-8-a--.-88--40M (Liu al.) 2025), and generalist L.M,, DeepSeek -...seeek-3..--..... V/.22Fxxp (DeepSeek-Al] 2025), as judges to reduce bias. The LLM judges score the statements scale of 0-10 based on detailed rubrics provided Appendix G.6
The evaluation results are presented in Table We report both the average scores over all valid gen- erations (Overall) and the average of the 500 highest-scoring samples (Top-500) for each metric. DExplorer significantly outperforms all baselines in the Top-500 regime across most metrics, par- ticularly Elegance and Interestingness, demonstrating its capability to discover mathematically meaningful problems. While Overall scores occasionally lower than Conjecture-P Prover, this
21

---

Published as a conference paper at ICLR 2026
Theme Brad
Socioe
Taket Cast
Figure 5: Distribution of difficulty shifts across different total token costs. (Top) Success rate across total token costs. (Body) Distribution of informal problem-solving questions' difficulty across total token costs, Areas are normalized to be identical across experiments. Lower item difficulty indicates more difficult problems.
expected as DExplorer generates vastly larger volume of valid statements (2726 1164), in- cluding simpler introductory lemmas that naturally dilute the average. However, the high scores in the Top-500 set confirm that DExplorer successfully pushes the frontier of mathematical discovery.
E TRAINING AND EVALUATING DETAILS
E. TRAINING RECIPE
Hyperparameters. All supervised fine-tuning are conducted using XTuner (Contributors) 2023 with the following hyperparameters:
Mixed Precision Training: bfloat16
Variable-length Attention: False
Pack to Maximal Length: False
Max Sequence Length: 8192
Sequence Parallel Size: 1
Batch size: 1
Gradient Accumulation: 64
Train Epochs: 3
Optimizer: Adam W with learning rate 2 10-5, B1 0.9, 82 0.999, weight decay 0
Gradient Clipping: by gradient norm 0.5
Learning Rate Scheduler: Warmup using linear learning rate scheduler with start factor 10-5 5 and warmup ratio 0.03 x epochs, then use cosine annealing learning rate scheduler with Muin 0.
22

---

Published as a conference paper at ICLR 2026
Table 3: cubrics-based evaluation results. Valid: number valid generations: RM: Reward Model scores
(unbounded logits, higher is better); LLM: LLM-based scores (0-10 scale, higher is better). Overall: average score across all valid generations: Top-500: average score of the top-500 samples sorted by the respective metric. Bold indicates best; Underlined indicates second-best.
Overall
Top-5001
Metric
Method
Valid
RM
LLM
RM
LLM
MUSTARD
3791
13.33
2.95
21.97
7.47
PromptCoT-DDS
457
18.79
1.45
18.79
1.45
PrompiCoT-QwQ
1024
19.95
2.37
25.73
4.57
Clarity
ScaleQuest-Math
2035
14.66
2.24
23.34
5.39
Conjecture Prover
1164
20.67
3.76
27.11
7.08
DExplorer (Staged)
2340
19.66
3.31
29.21
8.02
DExplorer
2726
20.40
3.32
30.39
8.14
MUSTARD
3791
-0.80
0.35
8.86
1.28
PromptCoT-DS
457
11.12
2.38
11.12
2.38
PrompICoT-QwQ
1024
12.35
2.37
19.16
3.90
Difficulty
ScaleQuest-Math
2035
1.01
0.46
11.30
1.50
Conjecture Prover
1164
13.39
2.62
21.77
4.90
DExplorer (Staged)
2340
12.25
2.43
23.50
DExplorer
2726
13.12
2.63
24.74
6.74
MUSTARD
3791
7.30
0.52
18.85
1.68
PromptCoT-DS
457
15.71
1.90
15.71
1.90
PromptCoT-QwQ
1024
17.07
2.16
24.00
3.38
Elegance
ScaleQuest-Math
2035
7.18
0.59
18.59
1.68
Conjecture Prover
1164
18.68
2.88
27.18
5.32
DExplorer (Staged)
2340
17.46
2.65
29.07
6.58
DExplorer
2726
18.15
2.79
30.16
7.09
MUSTARD
3791
4.87
0.13
2.33
1.01
PromptCoT-DS
457
8.40
2.23
8,40
2.23
PromptCoT-QwQ
1024
9.01
2.07
15.73
3.23
Interestingness
ScaleQuest-Mait
2035
-2.31
0.27
6.20
1.09
Conjecture-Prover
1164
8.50
1.83
17.00
3.34
DExplorer (Staged)
2340
7.71
1.79
19.15
4.25
DExplorer
2726
8.76
1.97
20.53
4.79
Training Devices: 8
Seed: 42
E.2 EVALUATION SETTING
Inference Hyperparameters. We use vLLM (Kwon et al.) (023) to serve all models with the
following hyperparameters:
Precision: bfloat16
Prefix Caching: True
Max Sequence Length: 8192
For each off-the-shelf LLM autoformalizer and prover, the hyperparameters in
ceneration_conff json, Huggingface example code, or vLLM's default settings:
Kimina-Autofommlize--3- (Wagg al. 2025a)
Temperature 0.7, Top-K 20, Top-p 0.8.
23

---

Published as a conference paper at ICLR 2026
Grevel-Prover- V2-8B (Lin et al.
2025).
Temperature 0.6, Top-K K 20, Top-p 0.95.
DeepSeek-Prover-V2-77 (Ren al.
2025).
Temperature 1.0, Top-p 0.95.
Kimina-Prover--istilllla (Wang et al.
2025a). Temperature 0.6, Top-p 0.95.
Our fine-tuned conjecturer and DExplorer uses vL.LM's default settings: temperature 1.0, Top-p 1.0.
Unconditional Generation. Our base dataset, NuminaMath-Lean (Wang et al. (025a), con- tains each problem's meta information including source, problem_type exam, author, and investionttyee Baselines, including MUSTARD and PromptCoT, synthesize problems con- ditioned on domains and knowledge points. Therefore, initially, the Conjecturer and DExplorer trained with conditional generation objective p(z[c), where represents problem.type and source. However, we find it difficult to design parallel comparisons to baselines, because conditions of NuminaMath-Leean, MUSTARD, and PromptCoT are significantly misaligned. For fair and focused comparisons, the 5000 generation attempts are based on the conditions from stratified downsampling all 39, 509 training data points. This marginalize out the condition by p(x) = p(rec)p(())
F LEAN 4 ENVIRONMENT DETAILS
The Lean environment in this research project depends on the following open-source projects:
Lean 4| & Ollrich (2021)
v4.15.0
Mathlib mathlib Community (2020)
v4.15.0
Aesop Limperg & From
2023
v4.15.0
Pantograp/AAniee Aniva et al. 2024
v0.2.25
With the following options:
Lean maxHeartbeats:: 0
Lean 4 maxtecDDptt: 100000
Lean 4 tacctcch.chhy false
Lean 4 ft.ffffllaeNle true
Lean 4 pp. ffnninee..ssssnddrrrpppss: true
Lean 4 pp..iii..nneerrepss: true
Pantograph timeout: 300
Pantograph imports: Mathlib, Aesop
When DExploration reconstructs formal statements from the Lean proof states, the following extra
options are set:
Lean 4 pp numericyyys true
Lean 4 pp. instanceTypes: true
Lean 4 pp. www.cccce.cc...o types: true
Lean 4 pp. www.mwaar..wi................... withtypee true
Lean 4 app.sstruutureelntaaateyeeeee true
Lean 4 p mvars: false
Lean 4 proofs: true
Lean 4 pp maxSteps: 100000
We sincerely appreciate the contributors of these awesome projects!
24

---

Published as a conference paper at ICLR 2026
G PROMPT TEMPLATES
Prompts templates for Kimina-AAtoffomaliznn-11 (Wang al. 2025a), Goedel-Prover-V2-11 (Lin et al. 2025). DeepSeck-Provers Prover-V2-7B (Ren et al. 2025), and Haimin-Provve-Disiieee -BB (Wang et al.
2025a are identical to their official templates.
G.1 DEXPLORER
System Prompt
You are an Olympiad problem setter and a Lean 4 expert.
You revel in confuring elegant problems starting from spare set of hypotheses, you 1et rigorous deduction lead you to surprising and beaut ful conclusions.
User Prompt
Given the introduced variables/hhpothhes. and the current context in
Lean 4, propose the single most natural next step explore toward a beautiful conclusion either
derive a new intermediate fact,
introduce fresh variable hypothesis,
submit one of the local facts the final answer.
Requirements
1. Flavoured "Iproblem type)" " and suitable for posting forums about " [[souree"".
2. Fully formal Lean code (inline comments natural language are fine for planning and reasoning). Assume 'import Mathlib',
Introduced Varisbles/Hypotheses
*1een
(introauced_fvars)
lean Context
"*1eaa4
(context)
G.2 CONJECTURER
System Prompt
You are an Olympiad problem setter and a Lean 4 expert.
You revel in conjuring elegant prcblems starting from spare set of hypotheses, you let rigorous deduction lead you to surprising and beautiful conclusions.
User Prompt
Propose Lean statement that explores toward beautiful conclusion.
Requirements
1. Flavoured (problem_type) and suitable for posting on forums about (source).
2. Fully formal Lean code (inline comments natural language are fine for planning and reasoning). Assume 'import Mathlib',
25

---

Published as a conference paper at ICLR 2026
G.3 INFORMALIZZTION WITH DEEPSEEK- V3.1 (FOR ALL METHODS EXCEPT MUSTARD)
All methods except MUSTARD generate self-contained formal statement and possibly for- mal proof. Therefore, they share an identical informalization prompt template as follows. The DEMONSTRATION.TEXT is 5-shot demonstrations randomly sampled from all statements, labeled by DeepSeek-V3. and manually revised.
System Prompt
You are a helpful assistant.
User Prompt
Given a Lean 4 formal statement and its proof, please translate then
into natural language.
1. Determine its question type: Question". Prefer "probl em-Solving Question" if possible. Question", please translate the formal code into a natural Language question, its answer, and its solution. appear in the question text. The solution
Question" "Proof
2. If it is a "Prablem-Solving
The answer should should wrap the final answer with "A]boxed(
3. If it is a "Proof Question", please translate it into a natural language proposition and its proof.
4. Please maintain the semantic equivalence between the natural language and the formal statement, and between the solution/proof and the formal proof.
questionvansserrprrppssi
5. Please zeply in markdown format with level-2 headers such as "## Problem-Solving Question", "## Answer" and "# Solution".
The following are some examples:
IDNMONSTRATIONNIII
Now, please translate the following formal statement and its proof.
## Formal Code
'>eean4
[formal_code)
...
G.4 INFORMALIZATION WITH DEEPSERK- V (FOR MUSTARD)
MUSTARD generates complete Lean 3 file, possibly consisting of multiple statements. We sepa- rately informalize each statement provided, all preceding code with the following prompt templates. is 5-shot demonstrations randomly sampled from all statements, la-
The DEMONSTRATION. beled by Ve3,Seek-V3.1, and manually revised.
System Prompt
You are helpful assistant.
User Prompt
Given Lean formal statement and its proof, please translate then
into natural language.
1. Determine its question type: PProblem-Solvinge Question" or "Proof Questicn". Prefer "Probiem-Solving Question" if possible.
2. If it is "Problem-Solving Question", please translate the formal code into a natural language question, its answer, and its solution. The answer should not appear in the question text. The solution should wrap the final answer with (1)boxed(())"
3. If it is a "Proof Question", please translate it into natural
language proposition and its proof.
26

---

Published as a conference paper at ICLR 2026
4. Please maintain the semantic equivalence between the natural language and the formal statement, and between the solution/proof and the formal proof.
puestlon-answer/prppossss
5. Please reply in markdown format with level-2 headers such as "## Provinm-Sclving Question", "## Answer" and "## Solution".
The following are some examples:
IDENONSTRATION_EEN TEXT)
Now, please translate the following formal statement and its proof.
# Formal Code
'1ean
[formal [ccmaa____d_ ccde]
...
G.S INFORMAL REASONING
For fair evaluation, the following prompt template is shared across all open-source generalist
LLMs, including Qwen3-8B (Team 2025b). Phi-4-mini-instruct (Microsoft et al. (025). OLMo-2-
1124-7B-Instruct (OLMo 2024), Mistral-7BB-Instrut--d0d (Jiang al. 20233) Llama-3.2-3B-
Instruct (Grattafiori et al. 2024). and Llama-3.1-88 ------Instttettt (Grattationi et al. 2024
System Prompt
P Please reason step by step, and put your final answer within \boxed:
User Prompt
(informal Linformal_question
G.6
RUBRICS- BASED EVALUATION
Rubries
"name": iinterestiggness "description": "evaluate the novelty, engagement, and curiosity-induciin nature of the problem.
High-scoring problems avoid standard 'textbook' templates application formulas. Look for a 'book' counter-intuitive result, a connection between seemingly unrelated mathematical fields (e.g., geonetry and nunber theory), or compelling narrative setup. The problen. should motivate the solver find the solution. Penalize standard drills (c.g., 'Caleulate the integral of x²2"), repetitive tasks, or problems that are mathematically trivial sidguissd with unnecessary verbiage."
"name": "Elegance", "descripticn": "Assess the aesthetic quality of both the problem statement and the intended solution. elegant problem stated concisely but implies deep structure. The solution should ideally rely on a clever insight, symmetzy, or structural understanding ('aha!' moment) rather than brute-force computation or case-bashing. Penalize 'ugly' numbers without reason, problems that require excessive, mindless calculation, or solutions that are significantl more complex than the problem statement suggests. If the answer includes solution, check if it uses the most efficient insightful method."
"name": "Clarity", "descripticn": "Evaluate the precision, unambiguity, and rigorousness the problem statement. Mathematical definitions must be standard or explicitly defined. Constraints (e.g., 'pesitive integers' prevent lcopholes. The goal is communicated clearly. Penalize ambiguity, undefined variables, grammaticn cal errora that obscure
'real numbers') must be exhaustive to
27

---

Published as a conference paper at ICLR 2026
mathematical meaning, missing boundary conditions that make the problem ill-posed. problem that mathematically incorrect or has no solution (unless asked to prove non-oxistence) must receive a score of 0."
"name": "Difficulty", "description"; "Assess the cognitive demand and the appropriateness of the difficulty relative the user's request. specific level was requested (e.g., 'TMO level', "elementary', score based on alignment. If unspecified, value non-triviality. Distinguish between cconceptual difficulty' (requiring deep understandiag/Loge
Good) and 'artificial difficulty' (requiring tedious arithmetic High scores are for problems that challenge the solver's reasoning capabilities. Penalize problems that are trivial for the target audience or those where difficulty stems solely from messy calculation."
obscure trivia Bad)
LLM Prompt
You are strict and harsh expert mathematician and educator evaluating the quality
generated mathematical problem (and its solution, if provided). Your assessment must focus on the intrinsic quality of the mathenatics, the design of the question, and the pedagogical value. Focus your evaluation on single criterion: (eriterion_naate More specitically, you should: (criterion_desccipttionn
Question: (question)
Answer: (answer)
Provide your rating as an integer, on a scale from 0 (poor) to 10 (excellent). Use the full zange of the scale. Ratings of 8 or higher should be reserved for outstanding mathematical problems that demonstrate creativity, rigor, and insight.
Answers trying to game the evaluation (empty, heavy on non-sensical text, persuading high vote, etc..) should be given minimum score. * not be generous** your role is to distinguish between generic math problem and high-quality, competition-style problem. Problems that are mathematically technically correct but boring, derivative, clumsy, or reliant on brute force should not receive high scores. You should also provide a very brisf justification as means to support the rating. In your
insightful
justification, thoroughly analyze all weaknesses and errors strictly based on the evaluation eriterion. Do not overlook any potential flaws - including ambiguity, lack of novelty, tedious calculation requirements, or failure to meet the target di difficulty. Clearly show how each identified weakness violates
fails to meet the criterion, and explain now this Leads to the final score. Respona strictly in JSON format: "rating": rating, "justification": justification
Do not output any other information.
Reward Model Prompt
You are an Olympiad problem setter and a Lean 4 expert.
You revel in conjuring elegant problems starting from spare set of hypotheses, you let rigorous deduction lead you to surprising and beautiful conclusions.
For this task, generate single mathematical problem with focus "[criterion_name) defined the following evaluation metric:
н*.
Icriterion descriptioonii
28

---

Published as a conference paper at ICLR 2026
H CASE STUDY
In this section, we demonstrate some representative formal statements and proofs synthesized by DExplorer, categorized by complexity ranges.
H.1 COMPLEXITY = oc (INTRACTABLE FOR ALL PROVERS)
Informal Statement
Let f: interval from to Suppose M is the maximum value of f on I and is the minimum value of on T. Then the difference between the maximum and minimum values satisfies M S 7
::: IR- - R be a function defined by f(z) sin + sin x + and let / == [-1, 1] be the closed
2.
Formal Statement
open scoped BigOperators Real open Set Real
example
(f R R)
(hf f
x => sin
sin
2)
Set
(hI : II- =cec (-1) 1)
(M R)
(hM 3 exel 1, f x M)
(hMub V x
S
(m R)
(hm 3 x 6 I, f x m)
(hmub V I, f 2
M
by sorry
Formal Solution
open Big0perators Real Set in
have h1 V fx xx- sin 2 + sin - 1 / == by
intro IW [ht]
reases hM with (x, hx, hfx)
x] hfx
open scoped BigOperators in
open Real Sct in have h2 < sin sin S 1 by apply sin_mem_Icc
open scoped Bigoperators in open Real Set in have h4 -1
< by nlinarith [sq_nenneg (sin Real.neg one le_sir x, sq sq_nonneg (sin 1), sq ss_nonneg (sin x + 1), Real.sin le_one one x, neg one le sin x, Real.sin_eq_add_com
2), Real sin le x,
x]
reases with (y, hy, hfy)
have h3 -1 < A _ := by
rw [hI] at hy exact hy
open scoped BigOperators in open Real Set in have h5 sin y -1 by 1inarith [Real. neeallnng_one_ee_si show sin y by apply sin_le_one]
29

---

Published as a conference paper at ICLR 2026
have h8
:= by
have h9 : f = := hfy
have h10 y (Real.sin y) 2 + Reall sin y + 2 := by apply hi
rw [h10] at h9
nlinarith [an_n (Reall.sin y) 1 2), Real.sin le Y, h5]
open scoped BigOperators in open Real Set in have h7 sin 1 by apply sin Le
open scoped BigOperators in open Real Set in have h6 by
7 1=
have h7 : f y := by
simpa using hfy
have h8 f y sin
+ sin + 1 / 2 : by
apply h1
[h8] h7
nlinarith [ag_nonneg (sin y 1), sq_nonneg (sin y 1), yl
Real deal.sin_sg_add_cos
have h9:
m $ / by 1
nlinarith [h4, h8, h6]
exact h9
Informal Statement
Let E R, x E R with x > 0, and y E R such that x + y = 2 and y > 0. Define a
sin cos"
Prove that 2 4
Formal Statement
open scoped gippprats in
open Set Real in
example
(0 R)
(x R)
(hx
x)
(y R)
(hxy : x y = 2)
(hy 00<)
(a : R)
(ha
a sin 2
0 ~ 2 y)
== by sorry
Formal Solution
have hl - 2 :- by linarith
have hxl
: by nlinarith [bxy, by]
have hyl : < 2 : by
have h2 y 2 x by linarith
[h2]
nlinarith
have h5
(2 - x) > == by mlinarith
have h2
(Real.sin 0 2) / (Real.co ~ 2) x)
30

---

Published as a conference paper at ICLR 2026
by
[ha] IW [show y = x by linarith]
open scoped Real in open Real Set in
have h6 sin
+ cos 2 : by exact Real Real. _q 0
open scoped Real in open Real Set in have h7
cos 0 by linarith [h6]
open scoped Real in open Real Set in have h8
0 2) / x) (cos -
by
Iw [h2] rw [h7] <;> rfng_nf
have h9 (x
x))
(Real.cos 0) - 2) x
(Real.cos - :-
by
Iw [h8] | (show # by linarith), (show (2 R 0 by
fiela_
mlimarith) | <;> ring
open scoped Real in open Real Set in have h10:
2 / := by {
by_contra h
push_ncg at h
have h12 :
/ 2 by
linarith
have h9 : a + (x (2 x)) (1 2) * (x (2 x)) : by
nlinarith [h12, show x * (2 x) > by linarith [h5], h9]
have h17
(x (2 x)) (1 2) (x (2 x)) :- h9
have h18 :
cos
(x
x)) := by
nlinarith [h17, h9]
mlinarith [sq nonneg (cos 2 (1 / 2)),
se se_nenneg (x 1),
se se_nenneg (cos
1)),
so se_nenneg ((1 cos 2) (X 1)),
h5
]
exact h10
H.2 COMPLEXITY IN [1200, oo)
Informal Statement
Let a, b, e be real numbers such that 2 2 and 1. Prove that
1b v 1)(c 1) + /(b l)(c - 1)) s 3(ab + be + ca - a - b-c).
Formal Statement
example (a R))
(ha a)
R)
31

---

Published as a conference paper at ICLR 2026
(hb b) R)
(ho : < c)
(illa - 1)
(b - 1)) + Vila - 1)
(c
1)) 6)
V(lb 1) * (c - 111)
< b
: by sorry
Formal Solution
have h1 a 1 := by linarith
have h2 0 < b - 1 1= by linarith
have h3
1) mul_nonneg h2
open Real in have h4
sqrt ((a 1) (b 1)) 2 (a - 1) (b 1) := by exact
Real.sq_sqrt sqrt (by positivity)
have h5 : 0 0 c == by linarith
open Real in have h8 (sqrt ((a 1) 1))) by
(a
1)
rw [Keal.sq_sqrt, nlinarith
have h9 Reallsqrtt ((b 1) (c 1111 (b 1) (0 1) := by
IW [Real.sq_sqrt, positivity
have h6
(c 1) nul_nonneg h2 h5
open Real in have h7 sqrt ((a 1) (b - 1)) + sqrt ((a 1) * (c 11) + sqrt ((b
1) (c 1)) 2 by positivity
open Real in have h10 :
(sgrt ((a 1) (b 1)) + sqrt ((a 1)
1)) + sqrt ((b - 1)
(e 1))) 2 <
** ((a 1) * 1) (a 1) (c 1) + (b 1) (c 1)] := by
nlinarith [sq_nonneg (sgrt ((a 1) (b - 1)) sqrt ((a 1) (c 1))),
se_nonneg (sqrt ((a 1)
1)) sqrt ((b 1) (c 1)]),
se se_nonneg (sqrt: ((a 1) (c 1)) sqrt ((b 1) (c 1]]},
Real.sqrt__onne ((a 1) * (b 1)),
Real. sqa_tsqg__nnneegg ( (a 1)
(c 1)), Real Real. sqrttnnnn_e ((b 1) (c
1)),
sq nenneg (sqrt ((a 1) (b 1)) " sqrt ((a 1) (c 1)) 2),
sc_nonneg (sqrt ((a - 1) (b 1)) - sqrt ((b - 1) (c 1)) 2),
sc_ sc_nonneg (sqrt ((a 1)
1)) " sqrt ((b 1) (c 1))
211
have hll:
(Real.sqre ((a
1)) Real. sqrt ((a 1) 1))
3 (a b b (c -1))
Real.sgrt ((b x
- c] := by {
nlinarith [h10, sq (a b), sq (b c), nonnen (c a]]
32

---

Published as a conference paper at ICLR 2026
exact h11
H.3 COMPLEXITY IN 1900, 1200)
Informal Statement
Let f R - R be a function such that for real numbers x and y. the equation f(x + y)
[(x) (vy 6xy holds. If f(-1) f(1) 9, what is the value of ((2000)? The answer is
12000000
Formal Statement
example
(f R + R)
(hf V x Y1 E (x
=f
6 y)
(h : (-1)+ 1 9)
2000 12000000
: by sorry
Formal Solution
have fo f 0 0 :- by
have h00 hε 0 0
norm num h00
linarith
have egl = hf 20
simp [f0] eql
have eq2 : (-1) f = : by
have eql' := hī (-1)
norm_num [20] at eql'
have h_eq : (-1) f := by linarith legi']
nlinarith [sq_nonneg (f (-1) 3), sq_nonneg (f 3), h_eq]
have fl f
have egll hf (-1)
have eel2 f (11 : R) + (-1 : BD E == by ring
rw [ec12] at eqll
rw [f0] at cql1
have cgg f (-1 R)
by niinarith [eq2, eq11]
Iw [eq9] at eqll
nlinarith
have fnegl f (-1) - =- by mlinarith [f], eq?]
have claim V (n N), ((fn R) (fa : R) := by intro n
induction with zero norm_num [f0] succ n ih =>
have eql (n + N) by specialize hf ((tn R) 1
R) = E ((fn R) + f 1 6 ((fn R
ring_nf at hf F
simpa using hf [eq1]
33

---

Published as a conference paper at ICLR 2026
rw [ih] rw [f1]
simp
ring_nf
have h2000 f 2000 (2000 R] 2 :- by
have h1 : (2000 R) (200C N) R) : by simp
IW [h1]
specialize claim 2000
simpa using claim
have h2001:
f 2000 12000000 :- by {
rw [h2000] num
exact h2001
H.4 COMPLEXITY IN [600, 900)
Informal Statement
Let be real number such that + 0 and
|ac| + 0.
Find the value of x. The answer is
1 V5
Formal Statement
example
(x R)
(hx * 0)
1 abs
x (1 /5) /2
:= by sorry
Formal Solution
have h1
by
by_contra h1
push_neg at hl
have h2 : x > 0 : by
by_contra h2
push_neg h2
have this x 0 == ay linarith
contradiction
have h3 1 / x 0 :- by
apply div_pos
norm_num
linarith
have h4 : abs x x := abs__af_app h2
rw [h4] at h
have h5
1 by positivity
linarith
have h2 abs = -x = by FW [abs_of_neg h1]
[h2] at
34

---

Published as a conference paper at ICLR 2026
have h3 field_simp [show x + 0 from hx] at h nlinarith
= by
have h6
apply or Real. sgrt / V intro h7
RRelll sqat. 5) / :- by
apply nlinarith [Real. pos mpr (show
(sub ne_ zero mpr h7)
R) by
R)
0), heal.sq_aqre (show < (5 : R) by num : (5 R) 2 0)
have h7: Real. sqrt 5) 2 by
cases h6 with
inl h7 =>
have h7 : x ;= by
nlinarith [Real. sgrt pos mpr (show (0 R) < by norm_num),
Real.sq_sqrt (show (0 IR) 5 by norm_nam)] nlinarith inr h7 =>
exact h7
exact h7
H.5 COMPLEXITY IN [300, 600)
Informal Statement
Let a be real number such that a² 3a² + 3a + 0. Evaluate the expression (a (a++1)= 2000 + (aa
1)2009 (a 1)2010, The answer is
Formal Statement
example
(a R) (h a 3 + 2
3
0)
(a 1) 2008
2009 (a 1) 2010
:= by sorry
Formal Solution
have (a + 1)
3 := by
nf at h 1inarith
have h2 +
:= by
have h3 (a 11 " +
:= by linarith
have h4 (a 1 1) ((a 1) *2 -2- (a + 1) 1) 0 :- by
nlinarith [sq_nonneg ((a + 1) 1), sq_nonneg ((a + 1) 2)
cases' (mul_eq_zero.ng h4) with h5
linarith
have h7 1) 2 (a 1 := by
nlinarith Isg ((a 1) / 21] nlinarith
have h4 -2 :- by 1inarith [h2]
35

---

Published as a conference paper at ICLR 2026
have h5 1) 2008
2009 (a 1) 2010 by
Iw [show -1 by linarith [h2]]
norm_num
exact h5
H.6 COMPLEXITY IN (0,300)
Informal Statement
Find the value of a + 20d, given that a and d are real numbers satisfying the equations a + 6d 30 and 10d 60. The answer is
135
Formal Statement
example
R)
R)
(ho : a + d 30)
(h1 : + 10 á 60)
20 * 135
by sorry
Formal Solution
have hd 15 / by linarith
have h2:
+ 20 d 135 = by {
linarith [h1, hd]
exact h2
I LIMITATIONS AND FUTURE WORKS
Controllable and Meaningful Generation. Current DExploration is bootstrapped by supervised fine-tuning (SFT) on data distilled from existing theorem-proff pairs. While our experiments show that it generates problems with superior elegance and difficulty compared baselines, relies implicit imitation rather than explicit optimization. Consequently, it underperforms at controlling specific domains, knowledge points, or difficulty levels on demand. Future works may incorpo- rate conditional training variables or reinforcement learning (RL) (DeepScek-Al 2024 Li et al.)
2025a Long et al., 2026) with subric-based reward functions achieve precise control and further maximize the meaningfulness of the generation.
fut-of-distribution Domains. Generalist LLMs are pretrained on web-scale knowledge, whereas the DExplorer is fine-tuned to explore mathematics primarily within the distri- bution of the training set. Future work may investigate techniques to maintain the broad knowledge coverage (Li et al. 2025b) of pretrained LLMs while adapting them to formally verified deductive exploration.
Generalization
Co-evolution of Formal and Informal Reasoning. DExploration effectively generates complex and difficult problems. This creates an opportunity for a virtuous cycle: using synthesized prob- lems to adversarially train and improve formal provers informal reasoners. Future work may explore this co-evolutionary pipeline to simultancously push the boundaries of problem generation and automated reasoning.
36

---

Published as a conference paper at ICLR 2026
J DECLARATION OF AI USE
We used DeepSeek- V3.1, Doubao, and Grammarly to assist writing in the following aspects:
Translating expressions in the native language into English.
Detecting grammar mistakes and polishing text.
We assure that ideas, methods, code implementations, experiments, analyses, and conclusions done by human researchers ourselves.
37


Reviews:
[{"review_id": "cTACgNF9Od", "reviewer": "Reviewer_8iAd", "summary": "This paper introduces DExploration, a Lean 4–based framework that reformulates mathematical problem synthesis as a step-by-step deductive exploration process.\nRather than directly generating conjectures or proofs, DExploration enables an agent to verifiably explore the mathematical environment through three atomic actions—Introduce, Deduce, and Submit—thereby generating both a formal statement and its proof in one unified loop.", "questions": "1. Have the authors tried fine-tuning a baseline prover (e.g., Goedel-Prover or DeepSeek-Prover) on the generated trajectories and evaluating it on public Lean benchmarks?\n2. Could the authors clarify which sources (Mathlib, NuminaMath, etc.) were used to generate the training data, and how they ensured no overlap with test theorems?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1. The paper makes good contribution by reframing theorem synthesis as verifiable exploration. The Exploratory Transformation pipeline that reuses existing theorem–proof data to construct fine-grained exploration trajectories is a natural and scalable way to create augmented theorem proving dataset.\n\n2. The authors perform a extensive ablation study that clearly supports their design choices, and the observed token efficiency improvement is both large and intuitively meaningful.", "weaknesses": "My main concern is the lack of external evaluation on public benchmarks. The experiments primarily analyze synthetic metrics (success rate, token cost, validity) on self-generated data. It remains unclear whether training on Exploratory Transformation data improves downstream theorem proving performance on public benchmarks such as MiniF2F, ProofNet or PutnamBench. Metrics such as “complexity” and “difficulty” are proxy measures based on proof length and model accuracy; these are helpful but insufficient for assessing real mathematical value.", "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": "FP52AZ2OFF", "reviewer": "Reviewer_kBGE", "summary": "The authors introduce DExploration, a step-by-step problem generation framework grounded in Lean 4, designed to scale synthetic mathematical data generation while ensuring provability. This approach offers a principled solution to the trade-off between scalability and formal correctness in mathematical reasoning datasets. Their empirical results show notable improvements in proof success rates, problem difficulty, and efficiency (token cost), though the study’s evaluation setup and comparison baselines raise questions about the robustness and fairness of the reported gains.", "questions": "On tactic reliability:\n- How do the authors ensure that all Lean tactics used (e.g., linarith, nlinarith, apply, constructor, cases) preserve the invariants required by their proofs?\n- Could they provide a more formal or machine-checkable justification that the selected tactic set does not violate the provability constraint?\n- Are there examples where tactic behavior led to incorrect or unverifiable results?\n\nOn heuristic verification:\n- The approach seems to rely on heuristic or single-sample checks. Have the authors quantified how often these checks fail to catch contradictions or reject valid cases?\n- How sensitive are the reported results to the choice of prover or verification strategy?\n\nOn evaluation design:\n- Why was a sample of 100 items chosen for manual evaluation, given the scale of generated proofs?\n- Could the authors provide metrics beyond binary correctness—such as clarity, ambiguity, or problem difficulty?\n- How representative is the 100-sample subset of the full set of 2,726 valid generations?\n\nOn the claim of “eliminating” external provers:\n- Since the system still depends on Lean, Aesop, and LLM-based provers for validation, could the authors clarify what they mean by “eliminates reliance”?\n- Would it be more accurate to describe the approach as “reducing” rather than “eliminating” dependency on external provers?\n\nOn limitations and open issues:\n- Could the authors discuss current limitations, such as tactic reliability, scalability, or remaining failure modes?\n- What are the main barriers to achieving a fully formalised notion of “deductive tactics”?", "limitations": "", "rating": 2, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "- Casting problem synthesis as an exploration process with three atomic actions: Introduce, Deduce, and Submit, is very simple and realistic, which closely mirrors the workflow of mathematicians, as well as a good way to approach the trilemma mentioned.\n- Reconstructing a formally checkable Lean 4 statement and proof from the agent’s exploration trajectory ensures validity in a principled, rather than heuristic way.\n- The Exploratory Transformation procedure (deductive rewriting → dependency graph → topological ordering) provides a sensible means to convert existing proofs into trajectories for supervised fine-tuning. The depth-prioritised reassembly is intuitively well-founded.\n- The paper reports substantial improvements in proof success and validity rates, alongside major reductions in token cost, which could be considered the main contribution of the paper. The generation of novel statements unprovable by SOTA provers further highlights the method’s potential (though if the results are robust).", "weaknesses": "- Lean tactics are tricky and very dependent on context. Common ones like linarith, nlinarith, apply, constructor, and cases can behave unpredictably in different settings. The authors note themselves (around line 1007) that a formal treatment of “deductive tactics” is still future work, and that some tactics can occasionally break the intended constraints. This makes the “guaranteed provability” claim a bit weaker than stated. Without a machine-checkable proof that the tactic set always preserves the invariants in their lemmas, the claim remains conditional. The reported 96.83% success rate is impressive, but it also shows that the guarantee isn’t absolute yet.\n- The method relies on heuristic or one-off checks, which are inherently probabilistic; some contradictions could slip through, and some valid but complex cases might get rejected. The paper mentions this, but doesn’t go into detail about how often such cases occur or how sensitive the results are to the choice of prover.\n- The manual evaluation covers 100 samples, with 97 marked correct. That’s a good sign, but the sample is quite small compared to the 2,726 valid generations and 39k training proofs. Also, the evaluation only checks for correctness, not for clarity or difficulty of the generated proofs.\n- The statement that “DExploration eliminates reliance on external provers and achieves fully provable generation” feels too strong. The system still depends on Lean, Aesop, and LLM-based provers for verification, and about 3% of outputs fail the final check. It would be fairer to say that it largely reduces external dependencies rather than eliminating them.\n- Finally, the paper doesn’t include a limitations section. It would help the overall credibility to acknowledge open issues; such as tactic stability, evaluation scope, or remaining failure modes.", "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": "ZChQiyqMCR", "reviewer": "Reviewer_ZhGX", "summary": "I think the authors did a genuinely impressive job with this paper. Let’s Explore Step by Step tackles one of the hardest open challenges in AI4Math: how to synthesize new, provably valid mathematical problems without relying on fragile external provers or autoformalizers. The proposed framework, DExploration, is both elegant and well-motivated. Instead of one-shot problem generation, the model explores mathematics step by step ie introducing variables, deducing facts, and finally submitting a conclusion — all grounded within the Lean 4 proof assistant.\n\nThis design ensures whole-process verifiability: every generated problem is backed by a valid proof trace, eliminating the need for an external verifier. I especially like how the authors handle data scarcity through Exploratory Transformation, which rewrites existing proofs into “exploration trajectories” via dependency graphs and topological ordering. It’s a clever and principled way to bootstrap training data from existing Lean corpora.", "questions": "Some questions that I had,\n\n1. **Domain Coverage and Generalization**: How does DExplorer perform on mathematical domains that have sparse coverage in Mathlib? Have you tested the method on areas like algebraic topology or category theory where formal libraries are less developed? I'm curious if the exploration quality degrades noticeably or if the framework is robust to these gaps.\n\n2. **Controlling Problem Difficulty**: Is there a way to guide the exploration toward specific difficulty levels or complexity targets? For educational applications, it would be really useful to generate, say, \"calculus problems suitable for first-year undergraduates\" versus \"research-level analysis problems.\" Have you experimented with any conditioning mechanisms beyond just adjusting the step limit?\n\n3. **Mathematical Interestingness**: Beyond formal validity, how do you assess whether generated problems are mathematically interesting or elegant? Have you considered getting feedback from professional mathematicians on whether these problems would be considered \"good\" problems? I'm thinking about the difference between a problem that's technically correct versus one that reveals some deeper insight or has pedagogical value.\n\n4. **Failure Mode Analysis**: The 3.17% of statements that fail the final typecheck is interesting. What patterns do these failures follow? Are they concentrated in certain mathematical domains or with specific types of tactics? Understanding what goes wrong could really help improve the framework.\n\n5. **Computational Efficiency in Practice**: You show impressive token cost reductions, but what about actual wall-clock time? How does the latency of making sequential Lean 4 calls compare to one-shot generation followed by proving? Is there a sweet spot in terms of step limits where you get the best quality-to-time tradeoff?\n\n6. **Scaling the Training Data**: The exploratory transformation works great on existing proof data, but could you bootstrap the process? For example, could problems generated by DExplorer be fed back as training data after human verification, creating a self-improving cycle?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "I think the authors have really nailed something important here with the core idea of DExploration. Instead of trying to generate entire mathematical statements in one shot, they've broken it down into a natural exploration process—introducing variables, deducing facts, and building up to conclusions step-by-step. This feels much more aligned with how mathematicians actually work, and the fact that every single step is verified in Lean 4 is brilliant. It completely sidesteps the validity issues that plague other approaches. The framework doesn't just generate statements; it simultaneously constructs their proofs, which means no need for external provers that might fail on harder problems. That's a genuinely clever solution to what the authors call the \"expressiveness-validity-complexity trilemma,\" and I find it both theoretically elegant and practically useful.\n\nThe experimental work is really thorough and convincing. Good job on testing across so many different dimensions; they don't just show their method works, they show it works *better* in multiple ways simultaneously. The 83% reduction in token costs alone is impressive, but combine that with higher success rates (40.70% to 54.52%), better complexity distributions, and harder problems that actually stump current state-of-the-art provers? That's strong evidence this approach is onto something. I particularly appreciate how they've evaluated both formal and informal reasoning, showing the generated problems are harder than AIME24 when translated to natural language. The ablation studies are well-designed too they clearly demonstrate that both the exploration framework and the exploratory transformation pipeline are pulling their weight. The Pareto optimality results across different computational budgets show this isn't just good at one operating point but scales gracefully.", "weaknesses": "My main concern is around how much this approach depends on having really good formal proof data to begin with. The exploratory transformation is clever, but it needs high-quality theorem-proving datasets like NuminaMath-Lean to work. I'm wondering what happens when you want to explore mathematical areas that aren't well-covered in existing formal libraries does the quality drop off? The authors don't really dig into this limitation much. It would've been helpful to see some analysis of how the method performs across different mathematical domains, especially ones with sparser coverage in Mathlib. Also, while they show the method can generate complex problems, there's not much discussion about controlling *what kind* of complexity you get. If you're building educational tools or want problems at specific difficulty levels, you'd need some way to steer the generation, and that's not really addressed here.\n\nAnother thing that's bugging me is the question of whether these generated problems are actually *interesting* from a mathematical perspective, not just formally valid. Sure, they're provable and they're complex, but are they elegant? Are they the kind of problems a human mathematician would find worthwhile? The explosion check prevents contradictions, which is great, but it doesn't guarantee the problems aren't trivial or weirdly artificial. The authors mention 97% correctness on a human evaluation of informalized problems, but that's just checking if the translation is accurate not whether the underlying problem is mathematically meaningful or pedagogically useful. I also would've liked to see actual wall-clock time comparisons, not just token counts. The multi-step exploration process involves lots of sequential calls to Lean 4, and I'm curious whether the latency becomes a bottleneck in practice compared to one-shot generation methods. These aren't dealbreakers, but they're gaps that future work should probably address.", "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)