Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
Authors: Chenrui Cao
Liangcheng Song
Zenan Li
Xinyi Le
Xian Zhang
HUI XUE
Fan Yang
Venue: NeurIPS 2025 poster ()
Keywords: Theorem proving
Large Reasoning Models
Neuro-symbolic
Lean
Primary area: deep_learning
TL;DR: By carefully coordinating off-the-shelf models with inference only, we show the DSP framework can achieve surprisingly good results in theorem proving, comparable to the frontier models with RL-based large-scale training.

Abstract: Recent advancements, such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B, demonstrate a prevailing trend in leveraging reinforcement learning (RL)-based large-scale training for automated theorem proving. Surprisingly, we discover that even without any training, careful neuro-symbolic coordination of existing off-the-shelf reasoning models and tactic step provers can achieve comparable performance. This paper introduces DSP+, an improved version of the Draft, Sketch, and Prove framework, featuring a fine-grained and integrated neuro-symbolic enhancement for each phase: (1) In the draft phase, we prompt reasoning models to generate concise natural-language subgoals to benefit the sketch phase, removing thinking tokens and references to human-written proofs; (2) In the sketch phase, subgoals are autoformalized with hypotheses to benefit the proving phase, and sketch lines containing syntactic errors are masked according to predefined rules; (3) In the proving phase, we tightly integrate symbolic search methods like Aesop with step provers to establish proofs for the sketch subgoals. Experimental results show that, without any additional model training or fine-tuning, DSP+ solves 80.7%, 32.8%, and 24 out of 644 problems from miniF2F, ProofNet, and PutnamBench, respectively, while requiring fewer budgets compared to state-of-the-arts. DSP+ proves imo_2019_p1, an IMO problem in miniF2F that is not solved by any prior work. Additionally, DSP+ generates proof patterns comprehensible by human experts, facilitating the identification of formalization errors; For example, eight wrongly formalized statements in miniF2F are discovered. Our results highlight the potential of classical reasoning patterns besides the RL-based training. All components will be open-sourced.

Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
Chenrui Cao Liangcheng Songl.2t, Zenan Li;, Xinyi Le Xian Zhang', Hui Xue', Fan Yang' Microsoft Research, University of Science and Technology of China, Department of Computer Science, ETH Zurich, Switzerland, *Rice University {caochenrui, slci) uste. edu. en, zenan. 1i@inn ethz. ch, r1105erice edu, {zhxian, xuehui, fanyang) emiieooscoii.. com
Abstract
Recent advancements, such Preview-72B, demonstrate prevailing trend in leveraging reinforcement learning (RL)-based large-scale training for automated theorem proving. Surprisingly, we discover that even without any training, careful neuro-symbolic coordination of existing off-the-shelf reasoning models and tactic step provers can achieve comparable performance. This paper introduces DSP+, an improved version of the Draft, Sketch, and Prove framework, featuring a fine-grained and integrated neuro-symbolic enhancement for each phase: (1) In the draft phase, prompt reasoning models to generate concise natural-language subgoals benefit the sketch phase, removing thinking tokens and references to human- human-written proofs; (2) In the sketch phase, subgoals are autoformalized with hypotheses benefit the proving phase, and sketch lines containing syntactic errors are masked according to predefined rules; (3) the proving phase, we tightly integrate symbolic search methods like Aesop with step provers to establish proofs for the sketch subgoals. Experimental results show that, without any additional model training or fine- tuning, DSP+ solves 80.7%, 32.8%, and 24 out of 644 problems from miniF2F, ProofNet, and PutnamBench, respectively, while requiring lower budget compared IMO problem in
Pooicck--Poov--22--11 and Kimina-Proved
sftteoof-the-at methods. DSP+ proves imo mmo_2019_pp_ miniF2F that is not solved by any prior work. Additionally, DSP+ generates proof patterns comprehensible by human experts, facilitating the identification of formalization errors; For example, eight wrongly formalized statements in miniF2F are discovered. Our results highlight the potential of classical reasoning patterns besides the RL-based training. Code and results are here: https: //git/gtittt com/ mi www.oooootttooccococooooooooooot Ptt//SPPPPuusu
Top Solutions miniF2F-test
95
Solution
Token Usage Pass
Pass
85
83.6
$2.0 H0.7 80.7
DSP+
4 (671B) 12k (7B)
1024
Pass Rate (%)
DeupSScck-Prover-22
(6711B
8192
75
68.4 67.6
65.9
64.7 63.5
Kimina- Paoina--Povee-Proviie
10k (728)
8192
65
DeepSeck-Provors Prover-oooooo-o11111
DSP- (ensemble)
DeepSeck- Prover-V2. V2-7BB
DSP (RI, V3, BFS-Prover)
55
Kimina-Provv Prover-Prevei
BFS-Prover
HunyuunProover
STP
38.9
InternI. StepPreeer Steee
Goedel
DeepSeck-Prover-V
DSP (Isabelle)
Figure 1: The best achieved results and the inference tokens used of top solutions on miniF22-test. DSP+, with inference only, can achieve comparable accuracy using fewer tokens.
Cooee and equal contributions. Work done during internship at Microsoft Research. 'Corresoondigg author.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

Introduction
Recently, a trend has emerged to leverage reinforcement learning (RL)-based large-scale training to improve the theorem proving capability of large language models (LLMs). Projects such as [3], BFS--rover [4], Goedel- 9 10, IT] are all dedicated to collecting or synthesizing large-scale formal statements and proofs, which are then used for RL-based LLM training. Coupled with significant human effort and computational resources, remarkable progress
AlphaProof (.. DeepSeek-Prover- V2 (2), Paiinna-Prove-Preeeeeee
Prover [3], STP-Prover [6), and many others 77] 8
has been achieved in challenging benchmarks like miniF2F [12]
Unlike the current trend, the prior Draft, Sketch and Prove (DSP) I relies on an inference-only framework with three phases to imitate the classical human reasoning patterns of
14], achieving fate--of-the-ar at its publication time. Despite the insight, DSP and its subsequent development [33 [S] were limited by the insufficiency of the frontier LLMs and the symbolic search,
thus being significantly outperformed by current top solutions, as shown in Figure
In this work, we surprisingly find that by carefully coordinating existing reasoning models and tactic step provers, the DSP framework can be revived as DSP+ to achieve notably higher proving accuracy that is even comparable to current state-of-the-art models tailored for theorem proving. DSP+ achieves this through fine- grained and integrated neuro-symbolic enhancements based on three intuitions, which differ from the maase-grained, thase-independent, and neural-syme neural-symbolic workflow in the original DSP: (1) Reasoning models generally have a stronger math reasoning capability than non-reasoning models, which can be prompted to generate concise drafts to benefit the sketch phase, with thinking tokens filtered; (2) LLMs can specify hypotheses in the sketch to benefit the proving phase, and most sketch lines after autoformalization are syntactically correct while incorrect ones can be "masked" by simple rules (e.g., replaced with sorry or removed directly) to sidestep obstacles in the workflow; (3) Sketch subgoals can be completed using both symbolic search and a weaker step prover like PFo-Prrver 4 with an efficient built-in integration.
We instantiate DSP+ in Lean 4 (version 14.17.0--cu [16]. In the default setting, DSP+ uses three open- sourced models, QwQ-32B [17]. DeepSeek- V3-0324 [18] and BFS-Prover [4] for draft (without human informal proof), sketch, and proving phases, respectively. And DSP+ can achieve comparable accuracy on benchmarks of miniF2F-test (79.5%), ProofNet-test (32.8%), and PutnamBench (24/644), under the search budget of 1024, 128, 128 workflow attempts, respectively. The miniF2F accuracy increases to 80.7% when replacing QwQ-32B with DeepSeek- R1-67166111 IB [19] even with fewer total inference tokens spent than those of Kimina- Simina-Prover-PPee Proveer-rreview-221 as shown in Figure [
We also have ablation studies to show that with an ensemble setting of DSP+, namely with different combinations of reasoning models, the accumulative accuracy can be further boosted as 83.6%, 33.9%. 25/644 for miniF2F, ProofNet, and PutnamBench, respectively, and from 40% to 45% for miniF2F/IMO. As shown in Figure and Table [] the accuracy of DSP+ is either on par with or outperforms prior arts 2 3 4 5 o proves imo _mo__m19__ppp__p__p an IMO problem miniF2F which not solved by any prior work (illustrative DSP+ workflow in Appendix Hp. Moreover, we independently find eight problem statements of miniF2F are wrongly formalized by examining the inconsistent behaviors of DSP+ in subgoal proving (details in Appendix FF). We ascribe the power of DSP+ to the synergy of reasoning models, step provers, symbolic search, and the careful ceuro-symbolic coordination. Our findings highlight the overlooked potential of existing reasoning models and suggest an efficient, complementary approach to the prevailing trend of RL-based training in theorem proving.
8 10, especially given the same search budget. Notably, DSP+
In summary, the contributions of the paper are: (1) We revisit the DSP framework, identifying its underestimated potential and incorporating fine-grained and integrated neuro- symoosym enhancements into its three phases: (2) We develop a system that facilitates flexible and efficient model coordination and ensemble settings, boosting the performance of theorem proving; (3) We conduct comprehensive experiments across various benchmarks to demonstrate the efficacy, efficiency, and synergy of DSP+.
2 Background and Related Work
Reasoning Models. Reasoning models, like OpenAl o-series, DeepSeek-R1 19 are emerging L.LMs to demonstrate strong reasoning capability with thinking tokens after a training process of reinforeement learning. For competition-level mathematics such as AIME, which test for
QwQ-32B 17
2

---

math word problems, reasoning models are achieving scores comparable to top human competitors. However, proving problems that require rigor are still challenging for reasoning models 20|21]
Theorem Proving with LLMs. LLMs' limitation on proving problems necessitates another strand of recent work, which focuses the proving capability of L.LMs with the automatic verification of theorem provers such as Lean [16]. Isabelle (22), and Coq [23] In these approaches, LLMs are required to generate formal proof, which consists of tactics resembling tuman-written proof steps. The search space for a single tactic is infinite and the tactic is required to link to theorems or axioms in the underlying library, both amplifying the challenges for theorem proving.
Much effort from the community focuses on the foundational setup for theorem proving [2 25], such as statement and proof synthesis 226 27 28 29] 30
31 [32 efficient framework and algorithms
33 34
36 37 38
37
15
39
proof reuse and repair [40 and library search 42 43
Based on these foundational work, recent projects such as AlphaProof and Laiina--rroer-Peeeeee
DeepSeee-Prooer--22 (
[3], and many others 4
5 6
g
build or synthesize large-
scale formal corpora for expert iteration, train with large-scale methods such as Rejection Sampling Fine-tuning (RFT) [55 and RL, and scale inference using techniques like Best First Search (BFS)
and MCTS, leading to strong results m2 112. ProofNet [46], and PutnamBench [47).
Symbolic Search. Symbolic search is an automatic mechanism widely used in theorem proving. which relies on pattern matching of pre-defined rules. It aims to better leverage the theorem libraries or tacties built upon axioms for vertical or even general domains. Symbolic search especially useful to close the trivially correct statements or subgoals (e.g., lemmas with have) without the tedious effort for the axiom-level rigor. For example, tacties in Lean like linari th can generally prove statements related to linear equations and norm_ num for numeric calculations, while simp and rfl can work for definitional conversions within a certain computation budget.
And one of the most universal tactics for symbolic search in Lean is aesop white-box and highly customizable proof search engine, which allows fine- grained control over the search space and the prioritization of tactics. In Aesop. each step of the search takes proof state as input and outputs tactic, through a general tree-based search with the pre-defined prioritization of theorem or tactic candidates. The search process can be configured with maximum computation budget for a valid proof, which is similar to the timeout in sledgehammer
Aesop serves as a
48 of Isabelle.
Draft, Sketch and Prove (DSP). To address the challenges of theorem proving, the DSP framework
13 introduced by synergizing neural and symbolic patterns: (I) to leverage LLMs (i.e., the neural) trained with extensive mathematics corpus for the "intuition" of proof draft; (2) to leverage the symbolic search for bridging the rigor gap between the intuition and the formal proof. Correspond- ingly, three phases are proposed in a course- course-grained and non-integrated setting, with first two as neural and the last as symbolic while no cross-phase optimization: The draft phase is to generate a natural language proof draft either by referring to human proof or by directly prompting LLMs, which initiates a constrained search. The sketch phase to generate hierarchy of subgoals in formal language (i.e., sketch) with omitted proving details, which is to leverage L.MMs capabillity of autoformalization (27) that interprets the draft from informal to formal. The proving phase is to fulfill the proving details omitted in the sketch by querying the symbolic search to automatically assemble the underlying tactics and theorems. DSP has inspired a sequence of work (49 50 40) with its intuitive neural- -eural-symbolic synergy. However, as shown in Figure DSP has been surpassed by wide margin by all the current models, which represent the new era of RL-based large-scale training.
Interestingly, the performance of DSP can be degraded with different settings. As discussed in [15 5) their re-implementations of DSP in Lean 4 can respectively prove at most 28% and 31% problems of miniF2F with LLMs like OpenAl-ol and DecpSeek Prover v1.5 [10) showing an accuracy drop w.r.t. the DSP in Isabelle, due to the limited search capability of aesop compared that of sledgehammer.
3 DSP+
In this section, we present DSP+, a DSP framework with fine--rainee and integrated neuro-symbol enhancements, where each phase is optimized by both neural models and symbolic rules in considera- tion of itself and other phases. This is different from the original DSP with draft and sketch phases as neural and the proving phase as symbolic, and with no cross-phand phase optimizations. For convenience, we use the draft model, the sketch model, and the proving model to represent the LLMs used in the
3

---

Formal Statement
Sketch with Hints and Masking example
Formal Proof
example (x y 3) (h1 x 1/2)
example :- by
(h2
Real.sin
Step
y
have ha Real.sin x by
have h3 Real.sin 5 by
with [h2]
clear h2
exact (sin h2).
Step
Step 2
Concise Draft
y
h4
by
<think>
prove_with [h3, t]
clear h3 t
/
Okay, so need to prove...
exact t.trans
</think>>
Step have h5 y (1:R)
Step
Step I: sin(x)
for 0ex
have hs (1:B) by
[Step 2: y
prove_with [h1, h4]
clear
1inrith
Stte 3: y² y
[M-] sonry
exact hs
Draft Model + Filter
Sketch Model Repair
Proving Model Tree Search
Figure 2:
The workflow of DSP+ consists of three phases. Every phase is enhanced with neural models and symbolic rules in consideration of itself and other phases.
corresponding phases. Each of these can be instantiated with any suitable LLM. We provide one-shot prompts for draft models and sketch models, listed in Appendix G The workflow, as illustrated in Figure2 will be explained in the following paragraphs.
3.1 Draft Phase with Thinking and Conciseness
As imput to DSP+, we directly provide the formal statement to the draft model, instantiated in our work as reasoning model (e.g., QwQ-32B, DeepSeek-Re R1). Reasoning models are widely considered more powerful in math reasoning they can perform deep reasoning, self-reflection, and advanced pattern recognition within the <think> tokens, enabling more accurate outputs after thinking.
Besides filtering out the thinking tokens, we also prompt the draft model to produce concise outpuls, focusing only the key formulas of proof steps. This prevents overloading the sketch phase, which may otherwise suffer from the "lost in the middle" (51) effect. Furthermore, we find it even more important to balance the format and flexibility of model output, as discussed Section 6.2
3.2 Sketch Phase with LLM Hints and Error Line Masking
instruct the sketch model to autoformalize P the concise informal proof provided by the draft model into hierarchy of subgoals in formal language, but without the proof for any subgoal. The sketch model required to explicitly specify the potential supporting hypotheses for each subgoal using a format like (prove_wt) wwht [h2]), as shown in Figure This format acts structured hints to the proving model. We define prove_wite t_wtth as a pseudonym for Lean's sorry, which denotes that proposition has yet been proved but temporarily assumed be true; in implementation, is augmented with explicit hypothesis usage. The explicit hypothesis specification benefits the proving phase,
observe that both proving models and symbolic search degrade when faced with overly cluttered subgoals. This is different from SeepSeek-Provers V2 [2], which leverages either all or none hypotheses in subgoal proving.
The sketch model may still fail to produce a syntactically valid sketch. To address this issue, we introduce an automatic iterative repair process, named error line masking. This process first parses the generated Lean code into a hicrarchical tree structure based on indentation, after which the Lean compiler identifies all erroncous lines. For each detected eиror, prune the corresponding node and its entire subtree from the code tree, optionally appending sorry at the original position. We aim to sidestep the re-execution of the sketch phase and retain sketch lines much possible, which is different from the proof truncation in DeepSeek-Provee Prover- [10]
3.3 Proving Phase with Step Prover and Tree Search
For the proving phase to fulfill subgoal proof, we further enhance the symbolic engine with proving model for more heuristic search, as envisioned [33. Especially, we leverage step prover (e.g.. Pro-rr (4, InterLMM2.--StePPre (52), which predicts the next tactic given proof state. We

---

tightly integrate the step prover with search-based approaches like free search (e.g., Acsop), in which each node the tactic tree is generated either by the default symbolic engine or by the step prover. This built-in integration can facilitate the independent search for the proof tactics to eliminate every prove_ wi and sorry in the sketch given the corresponding proof state (details in Section (
Implementation
In this section, briefly introduce how we instantiate DSP+, with further details in Appendix A We choose Lean 4 (v4.17.0-rc1) as the formal language and Acsop [3] for the tree search. We use QwQ-32B [17,, SrepSeek-V3-0333 [88. and BFS-Prover 44] as our default setting for the draft, the sketch, and the proving models, respectively. To enable the interaction between BFS-Prover and Aesop, we incorporate the Lean Copilot 34 framework, which enables built-in integration of LLM with Aesop's s internal logic and circumvents the tedious processes of converting proof states to theorems or external parsing. We also configure Aesop's 's search space include tactics proposed by BFS-Prover as well as few common tactics (e.g., linarith), similar to the configuration in [I3]
We set the configuration of QwQ-V3-BFS experiments, regarding the capability of math reasoning. instruction following, and subgoal proving. In fact, through our later ablation studies (eetioo(6.3). the default setting not the optimal given the output randomness and the vast design space. Therefore, for one problem, the workflow of DSP+ can be executed for k times fully explore the possibility of LLM generation for proving, which contributes to the pass@k lc accuracy in this work. In addition, besides the default setting, we introduce the ensemble setting where different model combinations are used one by one for solving one problem until proven or timeout. For the setting of DSP+ ensemble, DSP+ with different configurations of reasoning models and different pass @ (e.g., pass @ 1024, pass@ 128. pass @ 32) are attached after the default setting for solving one problem. We find that with moderate search budget, the ensemble setting can further increase the accuracy for solving challenging problems (e.g.. IMO, Putnam) given the diversity from different combinations.
default according our observations in early toy
We also optimize DSP+ regarding the modularity and the efficiency, which can benefit both the default and the ensemble settings. For modularity, DSP+ guarantees easy replacement of reasoning models where users only need to update prompt template according to the LLM interface and serve the model via vLLM [53). Besides modularity, DSP+ also guarantees efficiency with a pipelined and buffered process for theorem proving: each phase loads the results of the previous phase in the buffer and sends processed results to the buffer for the next phase. And the buffered results are shared for different model combinations to circumvent re-processing.
Evaluation
5.1 Experimental Setup
QwQ-32B, DeepSeek-V3-O0 V3-0324, and other models. We use the APIs provided by Microsoft Azure AI Foundry. For QwQ-32B, parameters are temperature = 0.6, top-p = 0.95, and max_ tokens = =32,768. For DeepSeek- V3-0324, the temperature is set to 0.7 with other parameters left as default. We use similar settings for other models.
BFS-Prover-7B. We deploy 4x40GB A100 GPUs with one model per GPU using vLLM. The sampling parameters are temperature 1.1, max_tokens 64, top-p= 1, 8.
Tree Search. Tree search is performed on 96-core CPU hosted on Microsoft Azure, with constraints including beam width of 4 (selected from 8 sampled tactics) a tree size limit of 64, and up to 8 search attempts for each subgoal. For details on the sample budget during tree search, please refer to Appendix B Fach proof search and verification process is limited to 2400 seconds. The search process terminates if no available targets, search budget runs out, or the time limit exceeded. All proof's are verified using Lean 4 (4.017.0-rc] with the corresponding Mathlib4 (54)
5.2 Benchmarks
miniF2F 12].
The miniF2F benchmark assesses formal reasoning capabilities high school mathe- matics, featuring problems from competitions including AMC, AIME, and IMO. This benchmark
5

---

contains balanced splits of 244 validation and 244 test problems, with curricular focus on algebraic reasoning and number theory. We use the Lean version of the dataset for evaluation.
ProofNet [46]. Designed for undergraduate--evel theorem proving, ProofNet aggregates 371 prob- lems (185 validation, 186 test) spanning core mathematical disciplines: real/complex analysis, linear/abstract algebra, and topology. Similar to miniF2F, we use Lean 4 version for evaluation.
PutnamBench [7 PutnamBenchh provides 1,709 theorem-proving challenges of Putnam Mathe- matical Competition problems (1962-2023), This benchmark features cross-lingual formalizations aggregated across multiple proof assistants, with our evaluation focusing the Lean subset, which consists of 644 problems at the time of our evaluation and is extended to 658 problems later.
5.3 Results
Main Results. Table I summmrrizs the performance of top solutions on the miniF2F-testt, ProofNet, and PutnamBench. Due to page limit, we move details into Appendix [ As shown in the table, all top solutions, except DSP+, models with RL-based large-scale training and categorized as either whole-proof generation or tree search, which complete the proof with single-pass and with interactions between theorem provers, respectively. By contrast, DSP+ is hybrid of whole-proo -roof (draft and sketch phases) and tree search (proving phase). With 1024 workflow attempts, DSP+ achieves performance comparable to extensively via RFT and RI., and evaluated at pass @ 92 for miniF2F-test. DSP+ also spends fewer inference tokens compared to Simina-Prover--revveeee
Prover-
which is the frontier model trained
discussed in Section 6.4
Results of DSP+ ensemble. Furthermore, the accumulative performance of DSP+ ensemble ap- accuracyJachievedd achieved by DeepSeck-Prover- V2-67 IB for the three bench- marks under the same sample budget, outperforming all other solutions. As detailed in Table 2 the combination of configurations tion, which contributes to the accumulative accuracy. For PutnamBench and ProofNet, our ensemble setting only uses 32 additional workflow attempts, with DeepSeek-R phases intact, resulting in an improved performance on both benchmarks.
proaches the state-of-the-an accuracy
prove miniF2F-test problems not found by the default configura-
the draft model and other
Results of miniF2F/IMO. As shown in Table we also compare DSP+ and other solutions with available results on the IMO subset the miniF2F benchmark. Our solution, DSP+ and DSP+ ensemble, can respectively prove 40% and 45% IMO problems with moderate search budget, on par with Kimina-Prover- Prover-Preview-777 and DeepSeck-Prowet Bricck--Prve-Veee Prover-V2-6711 of pass@819) Our solution also finds proof for amm__019_ppppp an IMO problem not solved previously, as detailed in Appendix H
Case Studies. We have included the success cases in Appendix J which show how DSP+ uses Jensen's inequality for high school competition problem and solves the real analysis problem of the Putnam exam, respectively. We also find the proofs of DSP+ different from those of DeepSeek- Prover-Ve V2, Kimina-Prow Proin--rrvve-PPeee Prover-Preview, and BFS-Prover, with details in Appendix M
6 Further Analysis
In this section, we will answer four research questions (RQs) with ablation and case studies: RQ1 Synergy. Does DSP+ synergize reasoning models, step provers, and symbolic search?
RQ2 Effectiveness. Does DSP+ benefit from our neural-symbolic enhancements?
RQ3 Robustness. Does DSP+ apply to various settings of LLMs and configurations?
RQ4 Efficiency. Does DSP+ spend more inference tokens than those with large-scale training?
For the rest of the section, unless specified, we use the default setting as baseline and set the maximum workflow attempts as 128. And we focus miniF2F-rest for the ablation experiments. In every curve graph, we plot the number of solved problems at different workflow attempts for stable comparison and include the pass @ 128 accuracies in the legends for clarity.
'Issues of Lean 4 v4.9.0-re may negatively impact the accuracy of DeepSeck-Proot Prover- V2 [56

---

Table Performance of top solutions across benchmarks (best results among the top in bold). DSP+ achieves performance comparable to frontier models (e.g., Kimina-prev prover, DeepSeckProver-Ve V2).
Type
Solution (Model Size)
Sample Budget
miniF2FFttet ProofNet PutnamBench miniF2F/IMO
32
15.2%
6/644
Goedel-Prove-788 S
512
62.7%
7/644
25600
64.7%
STP-7B 6
3200
65.0%
23.9%
8/644
25600
26.9%
52.5%
32
63.1%
192
10/444555
Whole- proot Generation
1024
52.9%
8
65,2%
Kimnnn Prover Preview 72B
32
68.915
1024
77.9%
8192
80.7%
40 %
1
58.6%
32
75.6%
23.0%
11/658
DeepSeek Prover V2-7B
128
25.4%
15/658
1024
79.9%
29.6%
23/58
8192
82.0%
61.9%
32
82.4%
30.5%
22/658
DeepSeekk-Proeer V2-671B
128
33.6%
33/688
1024
86.6%
37.1%
49/638
8192
88.9%
50%
2 x 32 600
50,7%
6/640
IntemLLM2.--stopPPooe----
256 32 600
65.9%
27.0%
Tree Scareh
PoppScck-Prooe--1.5-L... RMaxTS
T0
4 x 6400
59.6%
25.3%
x
HunyuamProver-7B
2
600 x 8 x 400
68.4%
20%
2048 x 600
70.8%
25%
BISS-Prove--BB
accumulativv
(GPT-4o, Isabelle)
10
4/640 551
DSP (Minerva-540B, Isabelle)
100
38.9%
5%
DSP- (QwQ-320 32B, V3-671B,
8
68.4%
Hyhrid
sborthand DespSock-V3-0324)
32
71.3%
24.7%
15/644
shorthand DeepSock-R1.)
128
74.2%
32.8%
24/644
1024
79.5%%
40%
DSP- (QwQ-328, QwQ-328, BFS-Prova-7BB
1024
79.1%
DSP- 671B, V3-671B, Prover DSP- (ensemhlle)
1024
$0.7
accumulative
83.6%
33.9%
25/644
45%
6.1 The Synergy in DSP+
Ablation of Components. Figure the results of different configurations, where one or more components are removed from the DSP+ framework. All variants exhibit performance degradation compared to the default "DSP+ (full)" setting. To further clarify each configuration, we take the "Draft + Sketch" setting as an example. In this setup, the Sketch model is directly prompted output the final, complete Lean code directly given the natural language draft, which means it produces tactic-level code without any "sorry" placeholders. The remaining ablation settings are constructed in similar manner. The "Sketch Prove" setting shows slight performance drop, benefiting from DeepSeck- V3's strong capability of one-step sketch generation. Interestingly, the "Draft + Sketch" configuration solves fewer problems than "DeepScek-V3 only". highlighting the critical role of step provers within DSP+. Finally, the "BFS-Prover with Aesop" variant achieves much lower performance than reported in 4. primarily due to the constrained computational budget described in Section 5.1
Synergy from Ensemble Setting. The synergy also manifests given the diversity of solved problems with different configurations. As listed Table 2 we choose three configurations of draft and sketch models for @ 1024 and three others for pass I 128, with the proving model fixed as The sample budgets are allocated according their potential in toy experiments. And we find that different model combinations cover different solved problems for the accumulative accuracy.
7

---

Unique Proofs and Synergized Applications. Besides the accuracy results, we also investigate the output of every phase. As discussed in Appendix|M the proofs generated by DSP+ differ from those by BFS-Prover for the same problems, with both improved readability and controllability. As direct consequence of the synergy: DSP+ has facilitated us to analyze the unfinished subgoals after the proving phase and find eight wrongly formalized statements, which are detailed in Appendix
Minif2f Test Problems Solved (out of 244)
Draft-Sketch, Pass@n
#Solved #Accum.
QwQ-V3@ 1024
+194
#Succossfull Proofs
160
RI-V3@ 1024
+5, -2
+5
120-
QwQ-QwQ@ 1024
+4,
+2
DSP- (74.2%)
None-V V3 @ 128
+1,-20
+1
80
Slurch Pooee (11 (%g
Skotch (22.5%
QwQ(No format)- V3@ 128
+1,-11
+1
QuQ only (27-9%)
RI-QwQ@ 128
+3,-11
+1
40-
Derptickk V3-0324 only (26,6%)
Total: 204
BFS Piover with Aesup (49.9%)
Table 2: Configurations of DSP+ ensemble for miniF2F. (+x, -y) indicates the setting solves x new problems but with y unsolved w.r.t the default setting. The accumulative solved problems (#Ac- cum.) show the synergy of configurations.
0
32
64
96
128
#Workflow Attempts Per Problem
Figure 3: Ablation of DSP+ components,
which shows the synergy in DSP+.
6.2 The Effectiveness of Neuro-Symbolic Enhancements
Conciseness of Draft. We observe that removing the prompting for conciseness slightly improves performance with larger pass@k k as shown in Figure In fact, as in the case study of Appendix K an unconstrained draft can be more informative with comparable length, which is acceptable for strong sketch models. Another interesting observation is that DSP+ shows higher accuracy without human informal proof, which different from
13 and detailed in Figure T0 Appendix D
Optimizations in Sketch. In Figure 5 we conduct ablation studies on the two optimizations in the sketch phase: (1) the explicit specification of subgoal hypotheses, and (2) the error line masking. Removing either optimization leads to a significant drop in accuracy and sample efficiency.
Symbolic Search with Proving Models. This is studied in Figure 3 and Section 6.3
Minif2f Test Problems Solved (out of 244)
Minit2f Test Problems Solved (out of 244)
#Successfull Proofs
180
#Successful Proofs
180
160
140-
140
Both Optimizations (74.2%)
120
Concise Steps (74.2%)
120
No Erve Masking (71.3%)
No Format (75.4%)
Hypothesis Specification (71.3%)
100
0
32
64
96
128
32
64
96
128
#Workflow Attempts Per Problem
#Workflow Attempts Per Problem
Figure 4: Ablation of Draft Formats. Free formatting is better as more informative.
Figure 5: Ablation of Sketch Optimizations.
Both optimizations are effective.
6.3 The Robustness of DSP+
Different Draft Models. As shown in Figure DeepSeck-RI I achieves higher accuracy than QwQ 32B, indicating our default setting may not be optimal. We also observe that QwQ-32B exhibits stronger instruction following capability than DeepSeek-R1, which can bring higher sample efficiency (details in Appendix L
We also provide details about output tokens in Appendix [
Different Sketch Models. As shown in Figure we find QwQ-32B, despite being primarily designed for natural language reasoning, achieves results comparable to DeepSeek-Ve V3, including solving some previously unsolved problems. This suggests the potential of QwQ-32B as the sketch model. We also provide more quantified metrics about them in Appendix

---

Mini[2[ Test Problems Solved (out of 244)
Minif2[ Test Problems Solved (out of 244)
#Successful Proofs
180
#Succcssful Proofs
180
160
160
QwQ-32B (74.2%)
140-
DeepSeck-RI (75.8%)
140
PeepSeck-V3-03222 (74.2%)
GPT-4o (71.7%)
GPT-4o (71.3%)
120
DeepSeck-VV V3-0344 (73.0%
120
Qwem2.5-32B-Imsimen (71.7%)
None (71.7%)
QwQ-32B (74.6%)
100
32
64
%
128
100
32
64
128
#Workflow Attempts Per Problem
#Workflow Attempts Per Problem
Figure 6: Comparing Different Draft Models. Reasoning models are optimal.
Figure 7: Comparing Different Sketch Mod- els. DeepSeek- V3 and QwQ-32B are optimal.
w/ and w/o Proving Models. We study two configurations for the proving phase: the default setting with BFS-Proved and another with common tactics (Appendix A.T). which show pass@ 128 accuracy of 74.2% and 47.5% respectively. We plan integrate models like DeepSeek- Proverr-Povv [TO] and SeeemLLM..---StPPrrooo
[52] in the future for more diversified capabilities (see Appendix !I
6.4 The Efficiency of DSP+
We collect the token statistics from 2 and 3 inference tokens, which are #Average tokens per pass X #Passes, compared to Kimina-Proved Prover-Preview even for the same accuracy. And the most balanced configuration our default configuration given the token efficiency and the dataset accuracy.
As listed Table 3
DSP+ can use fewer total
Table 3: Average inference cost different solutions in miniF2F-test. DSP+ (RI-V3-BFS) can achieve the same accuracy with less total inference tokens w.r.t. Kimina-Prover Preview.
Average per pass
Solution
Accuracy
7B
32B
72B
671B
DSP+ (QwQ-V3-BFS,
12k
6.3k
0.8k
79.5 @ 1024 Pass
DSP+ 1EP+(RI-V) (R1-V3- (3--V)
12k
3.6k - 0.8k
80.7 @ 1024 Pass
DSP+ (QwQ=QwQ-BBS))
6.3k
@ 1024
Kiminn-Prowt Prover Preview 3
10k
80.7 @ 8192 Pass
DoopSSck--roveerr
6.75k
88.9 @ 8192 Pass
The Limitation of DSP+
Underexplored Design Space. Due the vast design space of DSP+, we did not fully explore and set the optimal configuration as the default. And there are also opportunities to find the optimal configuration for the DSP ensemble given the differences in model capabilities and token efficiency. In addition, the DSP+ itself can be optimized to circumvent duplicated searches. All these can contribute more powerful and efficient search, which leave as future work.
Failure Cases. We detail failure cases in Appendix E In summary, we have identified challenges in every phase of DSP+, such as the proof of novelty for the draft, vague abstraction for the sketch, and misaligned difficulty for the proving. Interestingly, even different Lean versions affect DSP+ accuracy. We regard both model training and better proof assistant support essential address these challenges, which require more computing resources and more expert effort, respectively.
8 Conclusion
In this work, we revisit the DSP framework, which resembles the human reasoning pattern from informal formal. We find DSP is underestimated and can be revived as DSP+, which is as powerful as cutting-edge models for theorem proving. The key is our neuro-symbolic enhancement, which carefully coordinates reasoning models, symbolic search, and step provers in three phases.
With our comprehensive evaluations on benchmarks, we find DSP+ universally applicable frame- work with high proving accuracy and token efficiency, which potentially benefit the deployment

---

Towards and the re-development from the theorem proving community. DSP+ can also serve in the pipeline for generating high-quality cold-start data for model training. as indicated in DeepSeekProver-V V2.
We hope that, through our results and code, the community can have more diversified and synergized approaches for advanced theorem proving, besides the prevailing trend of large-scale training.
Acknowledgment
We thank the anonymous reviewers for their insightful feedback and constructive suggestions. We gratefully acknowledge the developers of the open-soures BFS-Prove model, as well as the Qwen and DeepSeek model series, for providing invaluable resources supporting our research. All experiments in this work were conducted at Microsoft Research Asia.
References
[1] AlphaProof and AlphaGeoomety teams. AT achieves silver-medal standard solving In- terntioonl Mathematical Olympiad problems. https: https://deepm:: http:///deeeedddde/emm wooplmmiindgggglle.... google/discover///
ai- ei-solves-imes iimee--mmoprroooo -eree-iiioooooeeee--eee siwver--vedssse medal-levell July 2024, Accessed: 2025-05-12.
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. Deepseck-proved prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025.
[3] 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 Bailcy, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schnne
Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang. Stamislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu. Zihan Wang. Zhilin Yang, Zhengying Liu, and Jia Li. Kimina-prov prover preview: large formal reasoning models with reinforcement learning. 2025.
[4] Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502. 033488 2025.
[5] Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover. A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.0760
2025.
[6] Kefan Dong and Tengyu Ma. Stp: Self-play Ilm thcorem provers with iterative conjecturing and proving. arXiv e-prints, pages 2502, 2025.
[7] Yang Li, Dong Du Linfeng Song, Chen Li, Weikang Wang. Tao Yang, and Haitao Mi. Hunyuanprover; A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024.
[8] Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internim2. s-stepprover: Advancing automated thcorem proving via expert itcration on large-scale lean problems. arXiv preprint arXiv:2410.1553 15700, 2024.
[9] Fabian Gloeckle, Jannis Limperg, Gabriel Synnacve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop Mathematicul Reasoning and Al NeurlPS'24, 2024.
[10] Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang. Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseck-prover-y S: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.088 08/522 2024.
[11] Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint ar.iv:2405........ 14333, 2024.
[12] Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. Minifff: a cross-systen benchmark for formal olympiad level mathematics. arXiv preprint arXhv:2109.00/10 2021.
10

---

[13] Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. The Eleventh Internaiional Conference on Learning Representations. 2023.
[14] Jacques Hadamard. An essay on the psychology of invention the mathmattiaal field. Courier Corporation, 1954.
[15] Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine-tor to- machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. arXiv preprint arXiv:2410. 16429, 2024.
[16] Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction Iidluction-CADE-222 25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378-388, Springer. 2015.
[17] Qwen Team. Qwq-32b: Embracing the power of reinforvement leaming, March 2025.
[18] DeepSeck-Al, Deepseek-v3 technical report, 2024.
[19] DeepSeek-AL. Deepseek-rl: Incentivizing reasoning capability in Ilms via reinforcement learning, 2025.
[20] Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović, and Martin Vechev. Proof or bluff? evaluating Ilms on 2025 usa math olympiad. arXiv preprint arXiv:2503. 2025.
[21] Roozbeh Yousefzadeh, Xuenan Cao, and Azim Ospanov. A lean dataset for international math olympiad: Small steps towards writing math proofs for hard problems. arXiv preprint XrXiv:2411.18877 2024.
[22] Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994.
[23] Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Cog Art: the calculus inductive constructions. Springer Science Business Media, 2013.
[24] Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su. Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. survey on deep learning for theorem proving. arXiv preprint (XXi:22444009939 2024.
[25] Kaiyu Yang, Gabriel Poesia, Jingxuan Hc, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXi::2412. 2024.
[26] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu, Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations, 2022.
[27] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, Advances Neural Information Processing Systems, 35:32353- 32368, 2022.
[28] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Tlya Sutskever. Formal mathematics statement curriculum learning. The Eleventh International Conference on Learning Representations, 2023.
[29] Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, and Ping Wei. Alchemy: Amplifying theorem-proving capability through symbolic mutation. arXiv preprint arXiv:2410.1574 15748, 2024.
[30] Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformalization. In The Thirty-eighth Anmual Conference on Neural Information Processing Systems, 2024.
[31] Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean-githube Compiling github lean repositories for versatile lean prover. arXiv preprint 20v: / 17227, 2024.
[32] Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: large- scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.038847 2024.
[33] Kaiyu Yang. Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song. Shixing Yu, Saad Godil, Ryan Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. Advances in Neural Information Processing Systems, 36, 2024.

---

[34] Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models copilots for theorem proving in lean. arXiv preprint 12X154 2024.
[35] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint ar0ii:2009.00000 03393, 2020.
[36] Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337-266 -63499 2022.
[37] Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang. Jing Tang, Jian Yin, Zhenguo Li, et al. Proving theorems recursively. arXiv preprint arXiv:2405. 14111 2024.
[38] Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 51 Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). pages 12632-1 12246. 2023.
[39] Zenan Li, Zhaoyu Li, Wen Tang. Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang. and Xiaox- ing Ma. Proving olympiad inequalities by synergizing iims and symbolie reasoning. arXiv preprint arXiv:2502. 13834, 2025.
[40] Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Eaze Xie, Jian Yin, et al. Lego-prover: Neural theorem proving with growing librarics. In The Twelfth International Conference
Learning Representations, 2024.
[41] Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229-1241, 2023.
[42] Guoxiong Gao, Yutong Wang, Jicdong Jiang. Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated Ican 4 dataset. arXiv preprint arXiv:2410. 10878, 2024.
[43] 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, pages 253-266, 2023.
[44] Jingyuan Zhang. Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover Posttraining scaling in formal reasoning, arXiv preprint arXiv:2504.06122 2025.
[45] Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Keming Lu, Chuanqi Tan, Chang Zhou, and Jingren Zhou. Scaling relationship on learning mathematical reasoning with large language models. arXiv preprint 2rXiv:2308.01822 2023.
[46] Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformaliiing and formally proving undergraduate-Ieve mathematics. arXiv preprint ar 12433, 2023.
[47] George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathe- matical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024.
[48] Sascha Böhme and Tobias Nipkow. Sledgchammer: judgement day. In Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 19, 2010, Proceedings 5, pages 107-121. Springer, 2010.
[49] Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-hased expert learning for theorem proving. arXiv preprint arXiv:2408. //172, 2024.
[50] Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal- bubgoal-based demonstration learning for formal theorem proving. In Forty-first International Conference on Machine Learning. 2024.
[51] Nelson F Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang. Lost in the middle: How language models use long contexts. Transactions of the Association for Computational Linguistics, 12:157-173, 2024.
12

---

[52] Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang. Dahua Lin, and Kai Chen. Internim2. S-stepprover: Advancing automated theorem proving via expert iteration large-scale lean problems. arXiv preprint urXiv:2410.15700 2024.
[53] Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng. Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang. and Ion Stoica. Efficient memory management large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles. 2023.
[54] Mathlib Community. The Lean mathematical library, In Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, page 367-381. Association for Computing Machinery, 2020.
[55] Trishul Chilimbi and PutnamBench Contributors, Putnambench leaderboard, 2023, Accessed: 2025-05-05.
[56]
Lean Zulip Chat. DeepSeek- Prover V2 TODO List, htwp:pppp//eeaapppro........aaaa
zww.aaapppprr......uc.ccccacatta com/nnarroo Theorem Pootr Pww.po/iiiocccccpoopppsoeooeeeee
Mawe1999--Mahhheee-eeee 20TODO 20tistt//tt//1110333333 2025. Accessed: 2025-05-12.
for-
20V2. 20V2.
[57] Leanprover Community. A read-eval-print-lopr for Lean 4.
com/
Leanprover- community/repl 2023.
13

---

NeurIPS Paper Checklist
The checklist is designed encourage best practices for responsible machine learning research, addressing issues of reproducibility, transparency, research ethics, and societal impact. Do not remove the checklist: The papers not including the checklist will be desk rejected. The checklist should follow the references and follow the (optional) supplemental material. The checklist does NOT count towards the page limit.
Please read the checklist guidelines carefully for information on how to answer these questions. For each question in the checklist:
You should answer [Yes], [No], or [NA].
[NA] means either that the question Not Applicable for that particular paper or the relevant information is Not Available.
Please provide short (1-2 sentence) justification right after your answer (even for NA).
The checklist answers are an integral part of your paper submission. They are visible to the reviewers, area chairs, senior area chairs, and ethics reviewers. You will be asked to also include (after eventual revisions) with the final version of your paper, and its final version will published with the paper.
The reviewers of your paper will be asked use the checklist as one of the factors their evaluation. While "[Yes] is generally preferable to "[No]" ", it is perfectly acceptable to answer "[No] providedd proper justification is given (e.g.. "error bars are not reported because it would be too computationally expensive" or "we were unable to find the license for the dataset we used"). In general, answering binary way, we
"[No] or "[NA]" is not grounds for rejection. While the questions are phrased acknowledge that the true answer is often more nuanced, please just use your best judgment and write justification to elaborate. All supporting evidence can appear either in the main paper or the supplemental material, provided in appendix. If you answer [Yes] to a question, in the justification please point to the section(s) where related material for the question can be found.
IMPORTANT, please:
Delete this instruction block, but keep the section heading "NeurIPS paper checklist",
Keep the checklist subsection headings, questions/answers and guidelines below.
Do not modify the questions and only use the provided macros for your answers.
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
The abstract and introduction clearly state our claims.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize other settings.
is fine include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: The limitation is thoroughly discussed in Section 7
14

---

Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
Justification: [NA]
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: Implementation details of our proposed framework are provided in Section We will open-source the code and data for reproducibility.
Guidelines:
The answer NA means that the paper does not include experiments.
15

---

If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution primarily new algorithm, the paper should make it clear how reproduce that algorithm.
(b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is new model (e.g., large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g.. with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: We provide the code of our theorem proving framework, well as small part of derived results, in the supplementary material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips. cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed to to reproduce the results. See the NeurIPS code and data submission guidelines (https
//nips.cc/public/eee.c wttp://dddee/oeeuumiieeeeeeeeeee ssi ssionPolicy) for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
16

---

Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification:
The evaluation details are carefully discussed in Section 5.2
Guidelines:
The answer NA means that the paper does include experiments.
The experimental setting should be presented in the core the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification: We cannot provide statistical significance of the experiments due to the extensive evaluation cost.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report I-sigma error bars, but one should state it. The authors should preferably report a 2- 2-simma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time exccution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
The details are discussed Section 5.1
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
17

---

The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethies
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics http:://wwaurp.cccpppppcccccccaa
Answer:
[Yes]
Justification: We check and confirm paper conforms with the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g.. if there special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: [NA]
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility ML).
11. Safeguards
Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, scraped datasets)?
Answer: [NA]
Justification: [NA]
Guidelines:
The answer NA means that the paper poses such risks.
18

---

Released models that have high risk for misuse or dual-use use should be released with necessary safeguards to allow for controlled use of the model. for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: Code packages and datasets are properly cited.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re- re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors are encouraged to reach out to the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification: The paper has not released new assets up to now.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: The paper does not involve crowdsoureing nor research with human subjects.
19

---

Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According to the NeurIPS Code Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent)
may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
20

---

A Implementation Details
A.1 The Configuration of Aesop
We configure Aesop's search space to be either tactics proposed by the step prover, or be with a few commonly used and efficient proof strategies (rfl, linarith, nlinarith, ring, positivity, omega, ring_nf, ring_nf of at *, simp, simp_all, all, field_simp, field_simg [+] *, norm_num, norm_num [+] *, norm_ norm cast at *). Furthermore, we modify Aesop's internal search prioritization to adopt the noraaizeer scoring heuristic introduced in BFS-Prover (4.
In addition, the hypotheses specified by the sketch model are sometimes inaccurate. Therefore, during the proving phase, split the budget into strategies: one using only the hypotheses hinted with tactics (clear ... (exemplified in Figure 2) and another using all available hypotheses. either attempt succeeds, we consider the proof successful.
A.2 The Motivation for the Built-in Integration of Step Provers
There are two common approaches leverage the neural models in the proving phase: one is the state-to-theorem approach so that the converted theorems can be proved by models; the other is to exterally parse and extract the state so that the step provers can help. However, both approaches are nontrivial with challenges, which motivate our built-in integration:
For the below. The subgoal of step4b can be correctly proved within the original test theorem shown in the left. However, if the state corresponding the right, the same proof fails due to the change of variable types. Similar issues are common- for instance, missing numbers variable types often lead to incorrect converted theorems given Lean's foundation on the dependent type theory. We suspect the Lean state contains more information than what visible at the string level. VSCode's 's Info View window, all numbers and variables can be queried for their specific types, but these details are not explicitly reflected in the string representation, leading loss of information. For parsing and extracting Lean proof state (e.g., using external Python). it is also challenging, as Lean code may involve complex tree structure, which is difficult to parse purely from code strings.
approach, example demonstrate the challenge is shown in the figure
step4b is converted into theorem,
shown in
theorem test (m N) (ho m.ged 6) (hi m.m 126) 60 m := by
Convert step 4b to theorem:
theorem step4b (m
(ho :
let /
m. m.ged n 6) (h; : m.lem n 126)
have step4b n
(b : N := 6): (n = bb :=
/- State: N
by
/- State:
ho m.ged n
h : m. lcm n = 126
bo : m.ged n = 6
: := / 6
h m. 1cm = 126
optParam (n 6)
rw [Nat. div ddv__canceel] have h² := Nat. faat.gdd_dvd_rigee m simp_all
rw Dat mul mil_diii______ieeideeeeelllliill mancel'] ']
lactic 'rewrite' failed
have h2 :- Nat.ged dvd right n simp_all
Fortunately, at the Lean level- as with aesop is possible to directly access Lean't 's internal structural information and run tactics based state, which significantly improves efficiency.
Another independent approach DeepSeekProver-V [2] demonstrates to reconstruct subgoals as theorems by purely syntactic parsing without referring to the Lean state, and therefore sidesteps the challenges we mention here. However, this approach can only work for the well-formatted sketch, not generic and flexible the built-in integration in DSP+
21

---

A.3 Lean Server Speedup
Even we have leveraged the built-in integration of tree search in Lean, which greatly reduces the need to recompile proven code, the verification process is still slow. The main timing bottleneck occurs during the header import (i.e., import Mathlib). Therefore, using the LeanREPL- multi-process verification scheduler framework of PrepSeek-PPoove-VVe of the (import Mathlib) as header, while still allowing different namespaces to be opened during verification. This results in reduction of approximately 10 seconds in average for each verification.
[TO], we support the reuse
A.4 The Workflow of DSP+ and DSP+ Ensemble
Following Section 3 the entire DSP+ process with default setting is as follows: formal statement is first sent to QwQ-32B which generates draft. This draft is then passed to DeepSeek- VVkk-323- which produces the initial sketch. Then, the sketch is processed with error line masking by interacting with the Lean environment via REPL [57]. Finally, the subgoals in the sketch are filled respectively with Aesop and BFS- BFS-Prover given the feedback from Lean. The DSP+ process terminates when the statement is proved, when resource parameters are exceeded, or when timeout occurs. In this work, we try 6 combinations for DSP ensemble in miniF2F-test as listed in Table And we only try R1-V3-BFS with pass @ 32 as the additional combination after default setting for ProofNet and PutnamBench.
B Sample Budget Configuration of Proving Phase
For the proving phase, use A x W x T for the maximum sample budget per subgoal, where A denotes the number of search attempts, W denotes the number of tactics generated for each expansion, T denotes the number of expansion iterations, namely tree size. If not specified, A = 8, W 8, and = 64. However, few proving phases can actually use up its entire budget. The reasons are listed below:
For parameter Not every subgoal is difficult- can be solved directly by symbolic search or resolved by single BFS-Prover expansion.
For parameter T. In tree search, if no expandable nodes remain, the process terminates early. Since each node expands only to width of 4 (by sampling 8 times and retaining at most 4 deduplicated expansions), this occurs frequently for hard problems.
For timeout. Additionally, a maximum verification time limit of 2400 seconds set for each proving phase, resulting in the process often being terminated before the full budget utilized.
We observe that under evaluation on miniF2F-test with Pass @ 32, each attempt of the DSP+ workflow samples the BFS-Prover for about 1500 times average during the proving phase, and generated about 8 tokens per sample, far below the upper-bound A x W per subgoal. This is well within acceptable limits for the relatively small BFS- IFS-Prover-7B model.
C Detailed Evaluation Results
Table Table all recent top solutions on miniF2F. We also include the results of miniF2F subsets like miniF2F/IMO, miniF2F/AIME, and miniF2F/AMC in Table 5 The results are consistent with the overall trend observed in the main table.
As our independent interest, Table 6 presents DSP+ performance on ProverBench (2), which is introduced recently with little probability of data contamination. We can see DSP+ approaches the performance of DeepSeek-Provent Prover-V2-671BB 2711,, showing the generalization of our method.
D More Ablation Studies
Detailed Ablation Studies of Draft Models. Besides the accuracy of different models, we also investigate the average number of tokens in the generated proofs and the average number of tokens in the thinking process. The results are shown Figure g We find that the QwQ model has lower average number of answer tokens (AAT) and higher average number of thinking tokens
22

---

Table 4: A collection of top solutions three benchmarks (best results among the top in bold). DSP+ and DSP+ ensemble are comparable to Simina-PPover-Previee and DeepSeekProver-VV V2, outperforming all others.
Type
Solution (Model Size)
Sample Budget
2i-i
ProoINet-test
PutnamBench
31
x 32 100
48.8%
18.15
4/640 55
Lcamnbell-Prover-78
128
61.1%
6400
58.4%
23.7%
DxepScok-PPovee- -..--oo--
10
Goedel-Prwer-T11
512
62.7%
7/644
25600
64.7%
3200
65.0%
23.9%
8/644
STP-7B
25600
67.6%
26.9%
1
52.5%
32
63.1%
192
10/644 55
1024
70.8%
peuol Generation
$2.9%
65.2%
Kimminu Preview 72B
32
68.9%
1024
77.9%
8192
80.7 %
1
58.6%
32
75.6%
23.0%
11/658
DeepScek--Proeer V2-7B
A
128
25.4%
15/658
1024
79.9%
29.6%
23/58
8192
82.0%
1
61.9%
32
82.4%
30.5%
22/658
DeepSeeks Priiii-Prvee---ee BB
33.6%
33/658
1024
8192
OpenAl a3-mmin gemini 2.5 pro preview 03-25
32
24.6%
3
32
37.7%
RcProvar-229M 33]
26.5%
13.8%
0/640
GPT-4o
10
1/644
55
DeepSeek-R R1-67
1/644
55
UV644
55
32
25.0%
Intenl..M.5-SStppooee--88
256 32 600
65.9%
27.0%
6400
59.6%
25.3%
DeppSeck-Proe--LLL5BR---- RMaxTS 10
Thee Search
32 x 6400
63.5%
HunyuanProver-77
600 x 8 x 400
68.4%
2048 2 600
70.8%
BFS- Prowerow !
accumulative
73.0%
596
7/640
64
41.3%
DSP (GPT-4o, Isabelle)
10
4/640
55
(Minerva Isabelle)
38.9%
52.5%
DSP+ (QwQ-32B, V3-67IB, BFS-Prower:7R)
8
68.44%
Hlbrid
DeepSeek-V3-de V3-0324.)
32
71.3%
24.7%
15/644
shorthand DeepSeek RI.)
128
74.2%
32.8%
24/644
1024
79.5%
DSP+ (QwQ 32B, QwQ.32n, BFS Prover
1024
79.1%%
DSP+ (R1-671B. V3-671B. BFS-Prover-7B) DSP+ (ensemble)
1024
80.7 %
socumulative
83.6 %
33.9%
25/644
ProlfNett-al results are used unavailable ProofNet-test
23

---

Table Performance of top solutions on IMO, AIME and AMC problems of miniF2F-test. DSP+ and DSP+ ensemble are comparable to Kimina Kimina-Prover Prover-Previews and DeepSeckProver- V2.
Solution
Sample budget
miniF2F- -est
miniF2E/AMO
miniF2//AIME
miniF2//AMC
Hunyua-Phova-78
600 x 8 x 400
68.4%
20.0%
BFS PB--Provr--7B
2048
600
70.8%
25.0%
Kimina-Prover Pree--Prrveeeeiiieee Prrina--Pove--Prevww---88
8192
80.7%
40.0%
86.7%
66.7%
DeepSeek Prover V2-671B
8192
88.9%
50.0%
93.3%
77.8%
DSP+ (QwQ-V3-BFS)
1024
79.5%
40.0%
86.7%
64.4%
DSP+ (ensemble)
accumulative
45.0%
86.7%
71.1%
Table 6: Performance of top solutions on ProverBench. DSP+ and DSP+ ensemble are comparable to Proveer.
Solution
Sample Budget
ProverBench
32
27.5%
STP-7B
128
31.4%
512
36.3%
DepsSckk-Prower-2--BB
51.7%
52.9%
DeepSeck Prover-V2-67IB
128
56.5%
512
59.1%
46.77%
DSP- (QWQ-V3-BBS)
52.92
DSP= (ensemble)
accumulative
55.69
(ATT) compared to DeepSeek-RI. Interestingly, reasoning models show lower AAT compared to non-reasoning models, which demonstrate that the thinking tokens can benefit the conciseness of the draft.
Detailed Ablation Studies of Sketch Models. Besides the accuracy, we also investigate the average translation rate (ATR) and median translation (MTR) of different sketch models. The results shown in Figure / We find that the DeepSeek- V3-0324 model has a higher ATR and MTR compared other models, indicating that it is more effective in generating correct code lines. This suggests that the DeepSeek-V3-Wee V3-0324 model is better suited for the sketch phase of DSP+.
We also investigate whether muman-writted proofs help improve accuracy, by providing them to the draft and sketch phases respectively. and comparing the results with counterparts that do not include human proofs shown in Figure [10] We find that incorporating informal proofs does not lead to an overall improvement performance, which is different from the original DSP [
Ablation Studies of Human Informal Proof.
E
Failure Cases of DSP+
We observe a wide range of failure modes, with most attributed to the following categories.
Minif21 Test Problems Solved (out of 244)
Model
AAT
ATT b
#SScccesstul Proofs
180
QwQ-32B
575
5682
160
DeepSeek-R1
693
2888
QwQ-32B (74.2%)
GPT--4-20224-11-20
748
DeepSeck-RR RI (75.8%)
140-
DeepSeek-V3-0024
948
GPTT-4o (71.7%)
None
120
DeepSeck- V3-0324 (73.0%)
None (71.7%)
100
"AAT: Average Answer Taken
ATT: Average Thinking Token
#Workfllw Attempts Per Problem
Figure 8: The Performance DSP+ with Different Draft Models. Reasoning models are better than non-reasoning models with the help of the thinking tokens.

---

Model
ATR
MTR
Minif21 Test Problems Solved (out of 244)
DeepSeek- 84.2%
100.0%
#Snccessfhul Proofs
180
QwQ-32R
63.2%
70.0%
Qwcn2.55322B-Imse.
71.0%
80.0%
160
GPT-40-2024-11-20
77.6%
89.2%
DeepSeck-V3 V3-0322 (74.2%)
140
GPT-4o (71.3%)
"ATR: Average Translation Rate. During the Sketch phase, erroneous code lines are iteratively removed until the code syntactically correct. The translation rate defined as the percentage code lines (excluding headers, comments, and blank lines) that remains after removal.
120
Quven2.5332BInnsien (71.7%)
Qw<Q33BB (74.6%)
100
32
64
96
128
#Workflow Attempts Per Problem
MTR: Median Translation
Figure 9: The Performance of DSP+ with Different Sketch Models. DeepSeek-V V3 shows strong capability of autoformalization with high translation rate.
Minit2f Test Prohlems Solved (out of 244)
180
#Successftl Proofs
140
Drall willoud Human (74.2))
Proof
120
Sketch without Human proof (No Draff) (?) (77%)
Sketch with Human Proof (No Draft) (67.8%)
0
32
64
96
128
#Workflow Attempts Per Problem
Figure 10: Ablation of Human Informal Proof. Human informal proof offers no help for reasoning
models generate good draft in miniF2F.
E.1 Limitations in Draft Phase
Many IMO problems involve very long natural language proofs, such as imo _mo_1977_pp (Reference Solution: fttt::://artooprooeemss/) Problems/Problems
comwiiki/iiixxxx phtiddex.pppppeepo http/1977_IND IMO_ These problems and their solutions are challenging even for humans to come up with, and thus the same for the reasoning models. Once the draft is incorrect for the intuition, DSP+ workflow struggles to produce a correct proof, because the sketch and proving phases faithful translators and executors. Here is example of unsuccessful attempt:
Wrong Draft
Informal Statement: Let (n) be function f : N+ - N+. Prove that f(n + 1) > s(f(n)) for
each positive integer then (n) =
dihink>..</thinkks
Step 1: f(1) =11)=11
Step 2: Assume f(k) - k for all Sn
Step 3: f(n) =
Step 4: f(f(n))= = f(n) =
Step 5: n << ffnf(t)))
Step 6:
11
Step 7: Suppose f1=+1)== + + lo with à 2
Step 8: f(++1 < 2)
Step 9: n+1+k2n+2
Step 10:
f(m+1=k) 2 / +
Step 11: Contradiction implics &o
Step 12: f(n+11
+1
Step 13: f(n) n for all E
25

---

E.2 Limitations in Sketch Phase
Difficulty of Formalization. Some solutions are inherently difficult to formalize in Lean. For instance. the standard solution to amc12a 12a_ _a__020_________________________ (Reference Solution: wwwkiiiiidee phpppppppp2/.// _____ 1er__r2Alllaaa Problems/Problee /troppoollmmmmmee requires the use of the function graph solve the problem, which could be hard to interpret in Lean. Moreover, since this is originally a multiple-choice problem, even the standard solution lacks full formal rigor, making it still some distance away from being accepted in Lean.
AoPS's Solution to 2020 AMC 12A Problem 9
y oa
Challenge of Lean's Syntax. Lean's syntax requires much higher level of rigor and delicateness than natural language, and it can sometimes produce unexpected emrors. This poses a serious challenge for the sketch model, which does not have access real-time Lean feedback. For example, the type of number often inferred from the context, and if the context is unclear or inconsistent, the system may raise obscure type errors. Below, present an example illustrate such challenging issue:
import Mathlib example : RR) (ho:
by exact
eq_eq_one_iff. mp ho
example (x : R) (bo: 2 x 1) x == by sorry
In Lean, the first expression compiles correctly, while the second one raises the error: failed to synthesize HPow N R ?m. xxx, because is treated natural number, and the operation of automatically converting a natural number to real power is undefined. These nuances are not convenient to humans, which also applies to LLM.
Misalignment of Function Definitions. The definitions of functions in Lean does not always align with human intuition, especially those learned from the standard curriculum. As mentioned in the Appendix F the domain the Real.log() function in Lean is all real numbers. Similarly, functions defined on the entire real number domain, such HDiv hDiv, Real sqrt, deal.arcsin. etc., may have values outside their domains that appear illegal humans, yet they can still significantly impact the proof of theorems. The above findings be demonstrated with the following code, which holds true Lean 4:v4. 17. 0-rc1:
import Mathlib
example
:= by simp
example 1 0 := by simp
example Real log 0 := by simp
example Real.
RReal.pi / 2 :- by simp
example Real.sgrt (-1)
:- by simp [Real.
That to say, while 1 - = -1 holds the integers, the value - does not exist in natural number domain. As result, in Lean's definition over natural numbers, we have 1 1 0. This means that subtraction on natural numbers often fails to satisfy the commutative law.
E.3 Limitations in Proving Phase
Some statements may appear trivial in natural language but are counter- -ounter-intuitively difficult to verify formally. For example, showing that æ > 3. 3.15,,, proving that the positive divisors 81 are exactly (1,3,9, 9, 27, 81), deducing a = 7, b = from the equation + vb + v1T when a and b are integers, all seem straightforward, yet constructing rigorous proof can be unexpectedly challenging.
26

---

import Mathlib
example Real. pp 3.141 :- by sorry
((1.3,9,27,81) Finset N) example (x y N) (h: 81): x
sorry
example (a b : 2) (h: a Real.sqrt by sorry
Real Real.sqrt 11): b 11
E.4 The Impact of Lean Versions
We use the miniF2F dataset from DeepSeek-Provee Prover-VI.. [T] which employs Lean 4:v4.9. 1...9..0-rcc 0-rc1. Our experiments reveal that the rfl tactic be used solve some problems in this version, but the same proofs fail Lean v: 17. 0-rc1, suggesting behavioral differences the tactic's implementation across versions. Below is example that is affected by the Lean version:
open BigOperators Real Nat Topology Rat theorem mathd www.mmmmerrrbr_222e..111 (b ZMod (11 2)) (ho
24-1) 116
by subst hn
simp_all only [reducePow] rfl
F Identified Errors in the miniF2F-test Dataset
With DSP+, identify 8 incorrect problems in the miniF2F-test datase The discovered problems are: 1i122a_2200_pp__ amc12a_2020 _0__220200_ppp__1_ amc12a_2021_ps imo 1968_p5_1, mathd_algebres
anduction_procm www.oooooooppppi1ee1mmmmmmmmmm mathd_ baad___mmberthory_BB25 errors, causing a mismatch between the Lean formalization and the natural language description.
mathd_alget Beahhd_aleebr__a___ These problems are either unprovable or contain translation
Example: amc12a 11122__2220_110
The original Lean theorem stated as:
theorem amc12a_ @alaa_2220_p11___ (n N) (bo n) (h: : Real, logb 2 (Real .lobb 16 n) = Real. logb 4 Cleal.logg 4 n)) (List.sum (Nat. digits 10 n)) = 13 := by
Since our workflow allows partial proofs containing sorry, find that of the 12 generated subgoals could not be proven in one attempt. The details of the proof attempt are shown below.
N) (ho n) Real. logb 4 (Real, (Real.logb 4 n)) : (List.sum digits 10 n)) 13 by
theorem amc12a_ amc12a_2020_ppl 2020_p10 (n
n) (hi Real. logb (Real. logb 16
Step 3: Substitute into original equation
have step3: Real ((Real. n) / 2) Real logb 4 (Real logbb 4
n) :- by ...
Step 4: Split log of quotient
have step4 : Reab 2 (Real logb 4 n) Real Real.logh logbb 2 2 = Real, Real.logb 4
(Real.logh 4 n) by
sorry
Step 8: Solve for log2 (logan)
have step8 : Reab 2 (Real logb 4 n) 2 : by Step 9: Exponentiate to solve for logan by
have step9 Real.logb sorry
KKimina Prover Preview project identifies 5 incorrect problems in miniF2F-tes 2 of which aime aime_1994____ 1994_p99pp and mathd www.enutmerrrrreeee cambbertheoryy_611 discovered by us. We their corrected versions experiments.
27

---

From Step to Step 4, the LLM applies the logarithm quotient rule, i.e.,
log, (z/3) log, I logs y.
We can use tools such as loogle, mathlib4 docs, or leansearch to find how this theorem is defined in Lean. In Lean, it is stated as:
theorem Real. _ogb_div (hx * 0) (hy * 0) logb (x / y) logb logb b y
Therefore, if we want to apply the logarithm quotient rule, also need to prove that Real. .oob n &f One might assume that since heal.logb n appears as the argument logarithm in the original problem, it must be nonzero. Unfortunately, this cannot be proven in Lean, because in Lean, the definition of Reeal.log is:
As with the natural logarithm, define logb b to be logb b xx| for 0, and ( for x = 0.
In this definition, Real. logb 4 n can be zero though it appears the argument of another Real. logbb. We now verify whether is provable that Real .lobb 4 n n 0 under the assumption that n >
Unfortunately, the whole equation still holds when n 1, which can verified Lean with:
theorem amc12a_2022 _020_p1000 N) (ha 1) Real .ogbb (Real. 16 n)
Real.logb 4 (Real.logb 4 n) :- by simp_all
So we are unable establish that Real logb + 0, which prevents the application of the logarithm quotient rule in Step 4.
Furthermore, Step Step 9 also presents difficulties. Although it may appear straightforward for humans, Real.logt .logb n could potentially be -,, and this case must be explicitly ruled out to ensure correctness.
In our revised version of the miniF2F dataset, we modify the condition (No << n) to ensure that all arguments passed to Real .logb are strictly positive, consistent with the domain of the logarithm function over real numbers as understood by humans. We also make adjustments to some other problems with domain definitions inconsistent with human interpretations, although in some cases, the parts outside the commonly accepted domain could be ruled out by contradiction.
G Prompts Used in This Work
Prompt for Draft Model
[formal statement]
Please provide extremely detailed mathematical calculation following your thinking. Each step only contain **nn*** equation without any explanation.
Here an example:
### Step 1:
x y
80
### Step 5: Mx+y+ + xy 81
Prompt for Sketch Model
informal informaalpproff:
[detailed_ing ddetailed_ifformal___ inforrma__protf Prove the theorem Iean code. You should translate steps in informal proof in series "have"/ l'let''et' "inducttion' / match' suffices statements, but you do not need to prove them. You only need to use placeholder "by [new line Jprove with[hl, step5. ... (hypothesises used here which proposed ahead) ]]' We want to have many lemmas possible, and every lemma must be easy proof.
28

---

When using a/b, b. you must specify *ea's or b's type**, because (1:R) 0.5, but (1:2) 2 0. When using you must specify **a's or b's type*s, because (1:2) 2 11,--,1,, but (1:N) 2 0. n! incorrect. you should (a)!.
Here is an example:
import Mathlib
example (x y R)) (h1
S 1/ 2) (h2 I 0) (t: < Real.sin
(x)): 1
by
Step
have Step 2
(1:R) := by
have h4 Real.sin S :=
prove_with [h2]
Step have h5 x :- by
#rove_with [h4, t]
prove_ prove_with [h1, h5] h3
formal statement:
"lean4
[header] [formal_statemenn statement]
H
Illustration of DSP+ Workflow with an IMO Problem
Our method successfully proves imo_ _no_2019_p1, whereas all prior arts have failed to solve this problem. Here we present its entire trace. However, due to the extensive length of QwQ's reasoning, we are unable to display the thinking part of draft phase here. In this problem, we can find all the techniques introduced by our fine-grained and integrated neuro-symbolic enhancements. To clarify the effect of enhancements, we use "Comment" to highlight our observations, which not generated by the sketch model.
Formal Statement
open BigOperators Real Nat Topology Rat
theorem imo _oo__019_p1 (f
Z + Σ)
(V (2 a) 2
f b = (f (a b))) V f V
f
by
Draft
<thinks..</thinkk>
Step 1: +22()) f(f(a+b)) Va
Step 2: f(0)
= f(f(b)) VbEZ
Step 3: (22()) = [(f(a)) Va EZ
Step 4: f(0)+2f(()
=
VOE
Step 5: f(2a) ff(0) Va
Step 6: +(2)+ f(f(b+1)) WbEZ
Step 7:
VbEz
Step 8: (22)+2((b) = =f(0) +[(()+((+++] Vb
Step 9: 2f(b+1) = +2)())))) 2b
Step 10: f(b+1)= 112)-110) f(b) VeE
Step 11: f(b+1) -f(b) f(2)-1(0) VbEZ
Step 12: f(z) -m where m 12)-110 and f(0)
2
Step 13: 2m(a + b) + = m²(a
(m 1)c Va, EZ
Step 14: m² 2m =0 + m(m (1
Step 2c = (m + +1)c (2 103-mmp m)c= 0
Step 16: = 0 c= or and is arbitrary
Step 17: [(z) = or [(=) + V2 E z
29

---

Corresponding draft steps in comment, sketch the red left, proof the green right
open Bigoperators Real Nat Topology Rat
Step 11
theoren ino 2019 p1 + 2) : (v b, b))) V f
have h11 122 2)
b, (b + r
a) 2 f
6, 2, =2-
prove_with [b10]
clear h10 (simp_all)
Forvard dérection: aseune equation holde, Issear
f
let
(f
(2
intro h
let c : f
Step 2
Step 12
have h2 V b, +
have h12 V 2, 12
by
intro
provo_with [b10]
clear h10
emact à 10 : 2)
have :- aimp_all
intro
sorry
inductiou? using
Step 3 have V a, a2 2
Iat. induction_oa with = ib ib
ring [h10]
intro
linarith
ezact à 2)
(simp_all)
have h10 (-2)
aorry
have h2 := h10 (-2 1)
eimp_all
Step have n4 V b,
linarith
sm by
Step 13
prove_vith [:2, b3]
clear
h2 b3
have h13 V b, (n (2 a)
(n
intro
c)
(n (a
by
linarith [12 b, h8 b]
prove with [b12]
(eimp_all) _all)
#Comeent:: sisaing gäven LLM
14
uneap Lasnable interpretation.
have h14
(m 2) :- by
Step
have 16 4 b, 2
(f (b 1)3
prove_uith with [b13]
clear
intro
have h14 :- h13 1
ring.nf
szact & (1 2)
have 15
b
linarith [h13 2 0, h14]
sorry
ZW coms 15
[add_comm] h5
Step
TW [add_comm]
65
have h15 (2
by
Conments: Tree search say lead to looped transitions between efates. Ve uitl address this iseue the fature.
[add_comn]
h5
prove_with [h13]
KW [edd_coum]
at b5
have h14 := h13 1
[ond__co]]]] h5
ring.nf h14
[oud] hs
linarith [h13 0 2, h14]
FW cears) h5
[add_comm] b5
Step have h_n_eg0_or_2
simpa [add_comm,
by (ozega)
mul_comm] using
prove_uith [h14]
Stop 7 have 1) =
(einp_all)
b, (b 000+2410
cases f_n__eg0_or__ with iill h_m0
Step 16
epact A2 Co 1)
(sinp_all)
sorry
prove_vee with [a15, b_m0]
clear h15 h_n0 (ulinarith)
Step 8 b,
1) :=
have __r_ 8,
by
pithe_with [h6,
prove_ with [b12, b_m0, h_c0]
clear h12 h_nD h_c0 (ainp_al1)
(sinp_all)
Step have h9 V b, 2
exact fun z -> Or.inl (b_f_zero z) h_n2
(t
by
have h_orists_c cl, V
pith [b8]
clear h8
exact fun by linarith
intro
[bS b]
eq
ra [b_m2] at exact eq
Step
have h10
Cb ((t 2 0) (2
)) f =- by
enact fun
(sinp_all)
Dr. sar (c, ezista_d e)
pich [h9]
clear h9
eorry
intro b
have h10 (b 1)
have h11 := (b
omaga
30

---

(Continuation of the previous figure)
direction:
Isnear, equation holds
intro h.rey
h_rev_aplit
0) G c,
c) by
prove_vita [b_rev]
hrrev
by_casea
3
cases h_rev, optsc uith
right
anl h_alt_sero
intro [h_att_arr,, 11
left
2) wwr.rollva_rrpp...
isr (e, R.J.eg)
have ths.vat (2 a) by
cases herev_aplit with inl h (eimp_all)
[h_f_eg (2 h_1_eg b]
inr h_1 m>
ring_nf
obtain (2, h) : h_1
f (1 6)) +)
(norn_num [4] (linarith)
3 by
fh.f.eq h.f-eg
c]
*Comentt*; The left part has errors, and the Error Line Nashing technique successfully meplaces the corresponding code with tactic sorry. Thsa éa proved later by Pro-err
ring_nf fth_ vhs_val]
sorry
I Capability Comparison of DeepSeek-Provers V1.5-RL and BFS-Prover
Although BFS-Prover is powerful prover, we use it more because its input is solely state, which fits framework. This offers benefit given -2..5-StepProoeer and DeepSeekProver-v both require chain-of-thought prefix, which incompatible to our current framework. However, in terms of performance, -FS-rrover cannot outpace all current provers. Here example:
example (b : R) (step6 b 9 (2 3) 9): (b = 2 3) := by apply Eq. symm
mlinarith (step6, sq_nonneg (b
(2 3) 2), sq_nonneg (b (2
3) ~ 3), sq_nonng (b (2 3) ~ 4), sq sq_nonneg (b ~ (2 3) - 5),
sq_ na_nonneg (b 6 (2 3) 6), sq nonneg
(2 / 3) 7), sq_nonneg (b 8 (2 3) 8), sq nonneg (b 9 (2 3) 9)]
This statement appears subgoal. Unfortunately, under configuration, BFS-Prover cannot solve it. By contrast, we find DeepSeck-Prover- V..--LL can provide the correct proof given moderate search budget. This indicates the diversified capabilities of different models.
J Success Cases of DSP+
J.1 Using Jensen's Inequality to Solve an Inequality
Statement
open BigOperators Real Nat Topology Rat theorem algebra, apbonzponaleegpommpppono (a
R) (n N) (ho 0
b) (hi n) ((a b) 2) n
n) 2 1= by
Draft
thhink>..<<hhinkks
Step 1: [2th < 26*
2
Step 2: Lei f(x) = x" for x > 0 and
Step 3: Since f*(x) n(n 1) 1==="== 2 0 for x > 0, f convex.
Step 4: By Jensen's incquality for convex functions: f aabb) < [(a)
Step 5: (at+)* < 2'
Step 6: Alternttvvly, consider using induction...
31

---

Sketch
open BigUperators Real Nat Topology Rat
theorem algebra_apbonan hwwp:appppppollppppppppeeooo
R) (n R) (ho : 0
0 b) (h1 0 < n) ((a b) / 2) n & (a
n
m) / 2 = by
Step 1: Define the function f()) n'n
let f R
- R fun
Step Show that is convez
have ConvexOn (Set. 0) f := by
prove_with[]
Step 3: Apply Jensen's 's inequality to have h3 ((a b)/2) I (f a b)/2 by
have
Set prove_wi Leve_with[Ma [ho]
E Set. Ioi by
have h5 (a + b)/2 E Set. Ioi := by
prove_ with_withhee [ho]
have h6 (1/2 R) (1/2 R)
by
prove_with[]
[ro h4, h5, h6]
Step 4: Rewrite using defénition of f
have h7 ((a b)/2) S (a n2/2 by
prove_with
Pinal conclusion
exact h7
Proof
theorem algebra_ algebra_apbon
R) N) (ho : 0
o b) (h1 0 < n) ((a b) / 2) n S (a
n +
n) / 2 := by
Step 1: Deféne the function f(m) =
let R I2 fun
Step 2: Show that f is convez
have h2 ConvexOn (Set. Ioi 0) f := by
apply ConvexOn.por
exact convexOn_id (convex_Iol Ioi (0 R)) le_of_lt
exact fun x Step 3: Apply Jensen's inequality
f
have h3 f ((a b)/2) < (f a f b) : by
have h4
E Set. Ioi
b E Set. Ioi by
clear ho obtain (left, right) ho
apply And.intra intro exact left exact right
have h5 (a b)/2 E Ioi by clear he
obtain (left, right) : hn
(field_simp)
have h6 (1/2 R) (1/2 B) clear (hinarith)
clear h2 h4 h5 h6 rw [ConvexOn] at h2 have h2. 2 h4.1 h4.2 (by positivity) (by positivity) h6 simp only [emul_equ [amul_eq_mul] h7
convert h7 using 1 ring_nf
ring
Step 4: Rewrite using definition of f
have ((a b)/2) S n n)/2 : by
clear h3
exact h3
Pinal conclusion
exact h7
32

---

J.2 Solving Putnam Problem on Real Analysis
DSP+ successfully solves a real analysis problem from the PutnamBench. include here as part of our results. This suggests that all three LLMs employed demonstrate genuine grasp of the subject beyond high school level. Furthermore, this highlights the general applicability of our framework.
Statement
open Metric Set BuclideanCeometzy Filter Topology theorem putnam_1977 1aamam_1177__ba b3 (S Set (R IR)) (a b R) (hab
b) (hS V
9, S} by
Ioo (hSclosed IsClosed S) IsClosed {y (x,y)
Draft
think>..<</tiinks
Step 1: Let (y.) be sequence in T converging to yo.
Step 2: For each n. there exists 2, E (a, b) such that (æ., yn) S.
Step 3: The sequence (æ..) is bounded since 2, E (a, b) S [o,
Step 4: By the Bolzano-Weierstras theorem, there exists a subsequence (Iny Un.) converging to some (zro)ol)
Step 5: E [a. b) because Jng in [a, b].
Step 6: Since S is closed. (zo. yo) S.
Step 7: By hypothesis. (x. y) E implies æ E (a. on E (a, b).
Step 8: Thus, (2o, yo) S. so E T.
Step 9: Therefore, T contains all its limit points, hence T' is closed.
Proof
open Netric BuclideanGeenetayy Topology
Step 4: By Weserstrazee enists a convergent subseguence (Xo R), StrictMone A Tendato (x yp atTop CN xo) :- by have h4 isCompact_ Ice tendsto_subee h3
RD) b) (h8 V a E b R) (hab
theoren putnam, 1970__33
Ioo a b) (bSclosed IeClosed 5) IeClosed
1133 3 R, (x.7) 9) by Step 1: Let (gn.) be seguence in converging to rv (iaClosod_aff_cuustee
rcases with (xo, hxo, y,, hymeno, hplim)
Yo
exact (y,, Xo, himano, hplim)
ssap only (wen_set0f at have bi ; (u n) 8) Tendsto atTop (N by
Step 5: E [a,0] becouse kt. [a,b]
1. (V n, 3 x: R.
h4 with (p, No. hp, hxp)
have h5 xg E Icc a in by n, (p n) Icc by
simp only [clusterPt_pp [clusterPt.princcpall prt.acpal...tt..rrouatt... men_ net_r eq] obtain (u, hu) Bu: R, N (x. u n) E 9) Tendeto u atTop (N yo)
intro
exact: (yp n) clear hxy this
apply eventually.
hxp Step 6: Sence sa closed, (30 E
reasea exists_aag, woralorall_oooo freqquttyyy (u, hu)
have Tendato (fun by
(xa, ro)
exact (u, ha.2, 1)
(x (sp n), (p n))) atTop (V (xo, yol) by
exact (u, hu)
Step 2: For each there ewists
[abde_prod_eg, cendetoo_poo__fff"
(a,b) such that (an. Bnd E
constructor
with hu, handatas
have b2 by
3 E Ico a b, (x, un
apply hu, tendate.
exact hp.tendsto_arfon
intro reases bu n with (x, ax)
have Y (x (p n), (p n)) s
by
exists
intro
exact (hS (x, nj hx, hx)
exact (hx (ip n)).2
Step The sequence (a.) bounded since 2a, E (a,b) 5 [a,b]
this_!
apply hSclosed. reeeeddeeeeooo www.eennn._eeeeeeoeeeeeeeeeeeeee te_deno this_1 simp [thia]
using
have h3
Ice by
Step 7: By Aypotheris, E (a,0) have xo E Ioo
intro a
by
Too_subset, Icc_ (bx n).1
clear hS h6
exact h8 h6
30
exact (xa, b6)
33

---

K Draft Comparison of Concise Steps and No Format
"Concise Steps" on the left, "No Format" on the right
Step 1:
To prove that (2918 5t8) mod 7 3, modular arithmetic Fermat's Little Theorem. 1. Simplity 29 mod 7:
29 mod 7 1
Step 2:
mod 7
Step 3:
29 7 remainder
29 = mod 7
29 mod 7 = 13 mod
Therefore:
Step 4:
11==1 =1
29 mod 7= 1 mod 7 1 mod! 7
Step
2. Simplify 5 mod
5 mod 7 7=1
Step 6:
k 5 mod
13 = 6 2
To compute 518 mod 7, apply Fermat's Little Theorem:
Step 7:
518 mod 7 (5 x 5 mod 7
Since 7 is prime and 5ot 0 mod 5% mod 7
Step
(1)* x5 mod 7 = 5 mod
Express 13
+ 1:
Step 9:
(29 513) mod (1 5)
513 = (59)² x 5 = (1)² x x5 mod 7
mod! 7
3. Compute the difference modulo 7:
Step 10:
1 1- 5=-4
(29 -5th mod (1-5) mod Convert a positive residue:
mod
Step 11:
mod 7 3
- -4 3 mod 7
Conclusion:
Thus, (2923 513) mod 7 = 3.
L Draft Comparison of QwQ-32B and DeepSeek-R1
In our early toy experiments, provide the same draft prompt to both QwQ-32B and DeepSeek-RI. and compare their final outputs after thinking session. To exemplify, the prompt is attached below:
Draft Prompt
formal statement:
theorem aime_ 1983_p2 (x (f: R- R) (h. : 0<p : 15) (b2 fx= abs (x p) abs (x 15) abs (x p 15)) 15 fx::=by
Please provide extremely detailed mathematical calculation following your thinking. Each step can only contain **on*** equation without any explanation.
Here is example: ### Step
1 = 80 J
### Step 5:
1x+y+xy+1=811
QwQ consistently produces responses that follow the instructions, shown below:
34

---

Output of QwQ-32B
##ff Step 1:
##f Step 6:
M f(x) = Ix + 151 ix (p 1
f (x p) x) (p x)
### Step
### Step 7:
M[ MeextGGiven ) Veq x lleq 15 limplies
M [f(x)= - p xX]
-
### Step 8:
#ifl Step 3:
M [[(x) = (x - x) (-p + (15 + 15) V
Meext(Given ) Meq 15 kimplies ix 151
#illi Step 9:
15 x
[[(x) =
x
### Step 4:
### Step 10:
M Mext Given } x Mlq 15 Mext/ and ) p>
M f(x) = 3
Nimplics Vleq 15 15 kimplies ix (p+
### Step 11:
15)I (p 15) \]
MexieGiven Given Vee 15 limplis Igeg
Step
-15 Vimplies 30 x lgeq 15
[[(x) = (x p) (15 x) (p 15 X
### Step 12:
M f(x) Igeq 15
By contrast, the output of DeepSeek-RI 1 does not strictly adhere to the instructions and fails to follow the one-shot formatting. Additionally, DeepSeek-RI sometimes includes its own Lean proof, which is often incorrect, as demonstrated below:
Output of DeepSeek-RI
Step 1:
Step 9:
M[ [(x)= = + lx 151 lx
Therefore, for V( p Veeq Veg 15 V),
Step
M f(x \geq 15
((p Veq Veq 15)).
"'lean4
[ -k-pt pl = -p
1983 p2 (x R) (f: + R) theorem dime_1983_____
Step 3:
(bo 0< p< 15) (h: x 15)
I[ 15 15 X
(h2 : abs (x
abs (x 15) abs by
Step
-p)15))
M 151 p 15 X
have : : by linarith
Step 5:
have h4 x 15 by linarith
Combine terms:
have hş 00<p by linarith
[(x) = (x p) (15 (p 15
have ha p 15 := by linarith
Step
simp all only [abs_of tatssssf_oonnen of_nonneg.
Simplify:
abs of "o__oo__oonos, sub_nonnene sub_ sub_nonpos, ha ha hs. ha]
M f(x) - 15 x 15 x
Step
For p < 15, simplify the absolute values linear expressions
=(x)==x++ 30
Step
-- ppppp=x p. lx 1.1 15 x,
Since V = = 30 - x is decreasing on V( [p.
151 p
15) 1). the minimum occurs at x 15 V):
-
Combine these to get f(x) -x 30
[[((5)= 30 15 15 !]
Since f(x) 30 is decreasing [p.
15]. the minimum occurs at
f(15) = 30 15 15
linarith
Therefore, we do not use DeepSeek-RI R1 as the sketch model at first, as this phase requires strong instruction-follwwii capabilities.
M Proof Comparison of Different Solutions
Since Kimina-Prover-Preeve uses the problem imo_ imo_1960 1962_p2, to compare with BFS-Prover, we also present DSP+ proof for this problem. As can be seen, our generated proof well follows human proof conventions at the have statement level, resulting higher readability. Only during the subgoal proving phase, the BFS-style and symbolic interaction with Lean slightly reduces the readability.
35

---

Proof of IMO-1962-P2 found by DSP+
theorem 1mo_1962_pp (x R) Cho 0 < 3 - x) (h.
S
1) (h2 1 2
Real.sqre (3 x) Real.sqrt (x 1)) -1
Real sqrt 31
by
Step 1: Domasn conditions
have h3 x < 3 := by
clear ho
(linarith)
h4 -1 v := by
clear h1
(linarith)
Step 2: Original inequality
have RRell. (I + 1) (1 RR) Real.sqrt (3 x) by
clear h2
(linarith)
Step 3: Squaring both sédes
have (Real.sqrt (3 x)) (Real. (x + 1) (1 R) / 2) by
clear hs ring_nf
ring_nf nf at hg ulinarith
(3 x), Real heal.sqrt_nonee (1 + x)]
Step 4: Expand squared terms
have h7
x
1) Real.sqrt (x 1) + (1 4 := by
nlinarith [qeal. h1, Real. ha]
Step 5: Simplify inequality
have hs (7 R) / 4 2
heal.sqra (x 1) by
clear hr
(linarith)
Step 6: Square again
have he ((7 R) 4 2 x) x by clear hs
norm_num hs +
Iw [t sub_pos] at hg contrapose hg rw [sub_pos]
rw [not_lt] hg
apply le_sqrt_of_sq.11 exact hs
Step 7: Empand and rearrange
have h1o 4 x 8 * (33 RR) 16 0 by
clear hg
(linarith)
Step 8: Multiply by 16 to clear denominators
have h11 64 * x-2 128 33 > :=
clear h1o
(linarith)
Step 9: Find roots of quadratic
have h12 < (8 Real.sqrt 31) / 8 V > (8 + Real. sqrt 31) / 8 == by clear hi1
refine' le.iff_not_imp_eee contrapose!
fun h
contrapose! hil
ulinarith [h11, h, Real sqaart (by norm num (0 R) 31)]
Step 10: Eliminate impossible case due to domain have his contrapose! h12 refine'
Real.sqrt 31) := by
(by linarith herl_ssrt_nowee (x 1), Real heal.sqrt_nonnee (3 x)], by
linarith [Real. Cheal.sqrt_nann sqrrt_oonneggggggteeeeeeogoggete 1), Real. Real.sqrt. sgrt_nooneegggggggggeggeggggngge (3 x)])
Final conclusion
have h14 x < Real. sqrt 31 / := by
clear * h1s
(linarith)
exact (h4, h14)
36

---

Proof of IMO--962-PP found by BFS-Prover.
theorem imo_1962.22 (x R) (ho 0 o 3 - x) (h.
S
1) (h2 1 2
Real.sqre (3 Real.sqrt (x 1)) -1
Real sqrt 31
by
constructor
linarith
Iw [t- sub_pos]
field_simp [Real sqrt_itt ha
apply 1t_of_le_of_1 rw [mul_comm]
rw apply it_of_le_of__
[t- "__sub_iff_ade
ring_nf
Iw [t- it_aub_iff__dd__
linarith [Beal.sq_sqr' (by linarith : S + x)]
rw [Real.sqrt_]] (by norm_num)]
rw [Real. sorl.sgrt_il <;> nlinarith
norm_nin num at this
Proof of IMO- 1962-P2 found by Kimina-
Limina-Prover Prover Preview.
theorem imo _eoo_992__p222 (x R) (ho 0 S 3 x)
(hi
0 <
1) (h2 1
Real. eqalt (3 := by
Real.aqrt (x 1))
Real aart 31
have h3 -1 - x := by
nlinarith
have h4 Real sqrt (3 x) RRall sqrt (x 1) / by linarith
have Real.sgrt
1) 2
heal.sqrt_noneee (x
/ 4 2 x) Real..srtt (x 1) := by
nlinarith [Real.sq_aqe
(show (0 R. < linarith),
by linarith),
Real sqart (show (0 R) x
deal.sqrt sonnnnggt_monneg (3 x), Real haal.sqrtnonneer (x 1)]
have
x) ~ (Real.sgrt nlinarith [h6, Seal.sggt_nonne., (x 1)]
1)) 2 by
have h8 (7 4 2 x) 2 x
by
have h10 (Real.sqrt (x 1)) -
by
rw [Real.sq_sque linarith
nlinarith [a7, h10]
have h9 64 * x 2 128 33 :
mlinarith [h8]
: x
Real.sgrt 31 / 8 :- by
by_contra hx
push_neg at hx
have h12 Real.sqrt 31 0 : by
apply keal.sqrt.pos.mp norm_nth num
nlinarith [aq_nonneg (x (1 Real..grt 31 8)), sq_nonneg (Real. sqrt 31), Real. sq_ttrt (show (0 IR) < 31 by norm_num), h12] exact (h3, h10)
Proof of IMO--192-42 found by DespSeck- V2.
theorem imo iho_1992_pp (x R) (ho 0 3 x) (hi
0 <
1) (h2 1 / 2
Real. (3 x) Real. sqrt (x 1)) -1 ISS A Real .grrt 31
by
have ha -1 S x : by
linarith
have h1 Real. sqrt (3 x) Beal.sqra (x 1) > 1 / 2 :=
linarith have ha Real. sqrt
Real.sgrt (x 1) / := by
37

---

linarith
by have he 3
Real.sqrt (x 1) + 1 :=
have hāt Real.sqrt (3 x) > Real sqrt (x
have hg2
< Real.sqrt (x 1) := Reat..srt_.nomeg
1)
have hes
S Real.sqrt (3 x) := Real.sqrr (3 x)
have bea
0 S Real.sqrt (x + 1) * (1 / 2) :- by positivity
have has 0 S Real.sqrt (3 x) : Reall neat.segt_nonne (3 x)
has (Real.sqrt (x 1) + +1 +1/2/
Real.sqrt (x 1) :- Real.sqrt_nnomeg (x
have her
2 0 := by positivity
have has Real.aqrt (3 x) > Real. sqrt (x + 1)
2 == hs
have ha9 (Real.sqrt (x + 1) + 2) 2 (Real eqrt (3 x)) 2
by
gcongr
<;> nlinarith Meal.ss_ssqu (show 0 S x + 1 by linarith), Real.aq aq.att (show 0 S 3 x by linarith)]
have b610 (Real. (x 1) + 2)
(x 1) + Real sqrt (x
1) := by nlinarith sqaar (show 0 S x 1 by linarith), Real.sq_sqrt
(show x 3 3xx by linarith),
sq_nonneg (Real. (x + 1) 2)]
have b611 (Real.sqr) (3 x))
3
rw sqarr] <;> linarith
nlinarith [Real sq.art (show 0 $ x + 1 by linarith), Real sqr by linarith)]
(show $ 3
have h7 7 x Real. sqrt (x 1) := by have h71 3 1 Real. (x
have h72 nlinarith dgeal.sqrt_nonee (x 1)]
< Real. 1) := Heal.sqrt_nonnee monnee (x
have hs
/ by
by _o_coa
have hs1 2 / by linarith
have ha2
8 x 5 by
linarith have has
Real.sqr (x 1) 200 = by positivity
linarith
ho
heal.sqrt 31 by positivity
have hıo 64 x 22 128 x 33 > 0 :- by
have h101 : 7 8 4 Real.sqrt (x + 1) :- hy
have h102 0
(x + 1) := Real. Real.sqrt__nonennn sqrt_nonneg (x 1)
have h10s 0 -
:= by linarith
have h104 0 Real.aqrt (x 1) := phal..qrt_nnomee
1)
have h1os : 0 0 - x := by linarith
have h106 (7 8 ***** x) 2 (4 * Real (x + 1)) 2 : by
geongr
have h107 : (4 Real.sqrt (x 1))
(x := by nlinarith [Real. sqrt (show 0 x + 1 by linarith), sq sq_noneeg
(Real.sqr sqrt (x 1) 2)]
have h1os (7 8 x) 2> 16 * (x 1) :=
linarith
nlinarith [Real sq_art (show 0 < x 1 by linarith), sq_nonneg (x 1)]
have h11 x < Real. sqrt 31 : by
by_contra h
have hm
1 Real sqrt 31 8 by
linarith
have h112 : 64
2 128 x + 33 < := by
have h113 : x 2 1 Real. sqrt 31 / 8 : h111
have h114 : x 1 Real sqrt 31 / 8 : by
bo_tantra h114
have hiss : x
Real sqrt 31 / := by linarith
have his6 : 64 * x 2 128 * x + 33 = hıo
have h117 : x < 8 : hs
ulinarith [Real. [Real.sqrt. sartt_ontt__ne 31, Real sqqrt (shou 0 31 by
norm_num)]
nlinarith [Real heellssqrt_nonee 31, Real.sq_sqrt (show 0 S by norm_num).
38

---

eq_ooneeg (x (1 Real.aqrt 31 8)), nonneg (x (1
Real. sqrt 31 / 8))]
linarith [hio]
exact (hs, hm))
Comparison with BFS-Prover. Our observations consistent with Kimina-Prover Preview: the proof generated by BFS is very difficult to understand, while both our code and Kimina-Prover Preview relatively more aligned with human proof writing habits.
Comparison with Kimina-Prove Prover Preview. A comparison between Kimina-Provert Prover-Previens 's open- source solutions and solutions reveals non-overlapping subset of solved problems. Specifically, Kimina-Prover- Prover-Preview's 's solutions include 4 problems that DSP+ does not solve, while our ensemble setting solves 11 problems unsolved by problem-solving styles between the two approaches. Below, we present one example of a problem solved by Kimina-Prover Preview but not by our method.
This suggests notable difference in
theorem aac12a__020__pa (S Finset N) (ho V N, 9999 (A a N, d Nat.digita 10 Even by have h1 Finset.filter. (fun => 1000 I Nat Nat. digits 10 >> Even d) A 5 n) (Finset Icc 9999) by
++ 1000 < A n) S.
A n S 9999 A (V d N, d E
ext simp [ho]
<;> tauto Iw [h1] native_decide
Comparison with DeepSeek-Prone Proiee--Prve--Vee V2. Our method fails to solve 16 problems that DeepSeek-
Prover V2 solves, but also succeeds on 3 problems that DeepSeek- Prover- V2 does not, One of the problems is imo_2019 2019_p11 1 in Appendix H
39


Reviews:
[{"review_id": "dl1b7e7jMV", "reviewer": "Reviewer_eJnA", "summary": "The paper revisits the Draft-Sketch-Prove approach to formal theorem proving in the lean language. That is: given a lean statement we wish to prove we 1) prompt a model first to make a natural language proof draft, 2) prompt a model to extract formal goals conditional on this draft (which is roughly formatted as a partially completed lean proof with placeholder statements that need to be filled in) and 3) we use a llm + search algorithm to fill in the missing details of the previous step. This is all prior work - the current paper extends this with various improvements, most notably 1) using reasoning model for the draft step, 2) better prompting and post processing of the sketch and 3) integrating with a tree search method (aesop) rather than the simpler heuristic “sledgehammer” algorithm used in the original DSP paper.", "questions": "Q1) Can you please clarify the numbers on the rhs of figure 1? Why the + ? Why the 1024 vs 8192? Make the xB explicit as params in billions. Thanks!\nQ2) Can you please list in a precise and unambiguous manner what the contributions are? My guess is that it is a) the use of chain of thought, b) using a newer and better base LLM, c) some heuristics to clean the sketches, d) prompting the model to make a concise sketch, e) masking generated lines of the sketch that produce lean errors, f) explicit specification in the subgoal hypothesis of the draft step.\nQ2b) What does f) in Q2 mean?\nQ3) Might # tokens be a better x axis for Fig 3?\nQ4) Is the legend clear? I could not quite figure out exactly what was presented.\n\nMinor points\nLine 17 fewer budgets -> reword + state of the arts -> reword", "limitations": "Yes", "rating": 2, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 1, "significance": 2, "originality": 1, "strengths_and_weaknesses": "Strengths\n\nThe overall problem is important. The experimental results are strong, only beaten out by the bespoke and super strong RL fine tuned DeepSeek Prover. The authors appear to be very talented at making the LLM pipeline really shine.\n\nWeaknesses\n\nThe paper has relatively little technical novelty, but is rather a well executed application of lots of small known ideas. It presents a nice engineering effort, but this may not be appropriate for the NeurIPS main conference, and may be better suited to a more practical workshop track or so.\n\nThe presentation somewhat obscures the actual novelty in the paper. For example, the authors repeat the phrase “fine grained and integrated neuro symbolic enhancement” as a contribution, but this is rather vague. On line 64 the explanation for the good results is also rather vague.\n\nThe contributions such as certain prompt tweaks are somewhat tied to the specific LLM and not especially valuable scientifically.", "was_revised": true, "final_justification": "I have considered everything already, thanks.", "rebuttal": "### **Clarifying Figure 1**\n\nIn RHS of Figure 1, each line represents \"model size\" x \"inference tokens\" x \"inference times\". For example, DeepSeek-Prover-V2 uses 671B model, and generate 8192 solutions for one problem, with each costs about 6.7K tokens on average.  The **\"+\"** in the rhs of Figure 1 indicates that our best configuration `(DeepSeek-R1-671B, DeepSeek-V3-0324-671B, BFS-Prover-7B)` uses the combination of two 671 billion-parameter models. And the two 671B models spend an average of 3.6k and 0.8k inference tokens in the miniF2F evaluation, respectively. Regarding the \"1024 vs 8192\" comparison, due to limited computational resources, we only report results for the 1024 budget. This budget still achieved superior performance compared to Kimina-Prover-Preview.\n\n### **Clarifying technical contribution**\n\nThe main concern of the reviewer is the technical contribution of our paper. We would like to clarify that, our contributions are twofold. First, we introduce the first method to implement a high-accuracy, DSP-based framework in Lean, integrating a series of systematic techniques (e.g., error line masking, hypothesis specification, and built-in tree search) within DSP. Our results significantly revitalize the effectiveness of DSP, which was previously noted as underperforming in Pantograph [1] and GoedelProver v1 [2]. Our framework reveals that even powerful natural language reasoning models, without task-specific fine-tuning, can achieve results comparable to state-of-the-art formal proof generation models when integrated with effective tree-search techniques. This finding aligns with recent advancements, such as DeltaProver [3], which secured a silver medal in the IMO 2025 competition.\n\n[1] Aniva, Leni, et al. \"Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4.\" *International Conference on Tools and Algorithms for the Construction and Analysis of Systems*. Cham: Springer Nature Switzerland, 2025.\n\n[2] Lin, Yong, et al. \"Goedel-prover: A frontier model for open-source automated theorem proving.\" *arXiv preprint arXiv:2502.07640* (2025).\n\n[3] Zhou, Yichi, et al. \"Solving Formal Math Problems by Decomposition and Iterative Reflection.\" *arXiv preprint arXiv:2507.15225* (2025).\n\n### **Clarifying “prompt tied to specific LLM”**\n\nOur core contribution is the robustness of the DSP+ framework itself, not specific prompt text. To prove this, we demonstrate its general applicability across various LLMs. As shown in Figures 6 and 7, our framework functions effectively when using different models like DeepSeek-R1, GPT-4o, and QwQ-32B. The performance remains strong, confirming that the framework's design (including prompts) is robust and not over-tuned to a single model.\n\n### **Explaining explicit specification**\n\nIn the sketching stage, explicit specification significantly boosts the subsequent proving stage. Elaborately, this means that when an LLM converts a natural language draft into a formal proof sketch, it not only formalizes subgoals but also explicitly states any necessary hypotheses or assumptions for proving them.\n\nThis is achieved by using the `prove_with [h2, h5]` notation (or similar), which clearly indicates the premises relevant to a given subgoal. For instance, consider the formal proof example in Appendix H (Page 22). If a subgoal were initially marked with `sorry` in the sketching stage, it would lead to an unconstrained and potentially excessive search for premises during the proving stage. However, by explicitly specifying `prove_with [h2, h3]` for that same subgoal, we effectively constrain the involved premises, thereby streamlining the proof search and making it far more efficient.\n\n### **Using different x-axis in Figure 3**\n\nTo benchmark the proving performance of various methods, we utilize Workflow Attempts Per Problem (equivalent to Pass@k). We also agree that the comparison of computational efficiency is necessary; therefore, we will include plots against total inference tokens in our revision.\n\n### **Explaining legends in Figure 3**\n\nFigure 3 presents an ablation study demonstrating the necessity of each component in our framework. We use **DSP+ full (74.2%)** as a reference, which comprises QwQ-32B (Draft), DeepSeek-V3-0324 (Sketch), and BFS-Prover with Aesop (Prove). The comparison methods are detailed below:\n\n- **Draft + Sketch (22.5%)**: Skips the interactive Proving stage. The Sketch model is prompted to generate a complete proof directly.\n- **Sketch + Prove (71.7%):** Discards the natural language Draft stage; the Sketch model is directly prompted to generate a formal sketch for a given problem.\n- **QwQ-32B only (27.9%):** Uses only the Draft model to generate the final Lean code from the Lean problem statement.\n- **DeepSeek-V3-0324 only (26.6%):** Uses only the Sketch model to generate the final Lean code from the Lean problem statement.\n- **BFS-Prover with Aesop (49.6%):** Employs only the step-prover to solve the theorem given the Lean statement.\n- **Aesop only (35.2%):** A purely symbolic approach using Lean's built-in tactics, with no LLM involvement. The input is the Lean problem statement.\n\n### **Minor points**\n\nThanks for the comments. We will revise it in the next version."}, {"review_id": "DCD38veJG1", "reviewer": "Reviewer_GGi1", "summary": "This paper designs a novel formal theorem prover by advancing the Draft, Sketch and Prove framework. The model integrates neural-symbolic tools with LLMs. In contrast to prior works, LLMs are introduced in each phase, and integrated with neuro-symbolic tree search methods via built-in implementation in Lean4. The framework is free of training or finetuning, while achieves comparable performance to frontier theorem provers based on post-hoc training of LLMs. Ablation studies validate the robustness of design, and efficiency w.r.t. inference tokens.", "questions": "1. Since the most advanced formal prover generates whole proof, is it possible to integrate whole proof generators to the Prove phase, to replace or complement the BFS-prover?", "limitations": "yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 3, "originality": 3, "strengths_and_weaknesses": "### Strengths\n1. As the most significant implication, the paper demonstrates that incorporating multiple existing LLMs and step provers into a delicately designed DSP framework can result in a significantly more powerful formal theorem prover. It increases BFS-Prover's accuracy on MiniF2F from 73% to 84%. Notably, the framework is free of post-hoc training of LLMs, while achieving comparable performance to the frontier large-scale whole-proof generator based on RL. The training-free feature is particularly valuable given the scarcity of formal proof samples.\n\n2. The proposed method sharply improves over previous DSP frameworks (39%-84%). The improvement is mostly attributed to the prove stage, which features a novel built-in integration of LLM-based step prover with neuro-symbolic tactic tree searcher. \n\n3. Sufficient ablation studies validate the synergy of all three component (DSP). The framework is flexible and modular, while being robust to the choice of LLMs for each phase.\n\n### Weaknesses\n1. The paper is not absolutely free of model training, since the step prover is post-trained from LLMs. However, the performance boost over  the step prover is significant enough.", "was_revised": true, "final_justification": "Considering the feedback from the authors, I maintain my vote for acceptance. The paper has made the following contributions.\n\nS1. The paper presents a refreshing view of the capability of the DSP framework with strong empirical results. It addresses the first effective integration of neural symbolic tools with LLMs.\n\nS2. Thank the author for their response to W1. In summary, the proposed DSP framework is training-free in the sense that it utilizes and combines off-the-shelf models and produces a significant boost of performance against each component.", "rebuttal": "### **Clarifying training-free of the framework**\n\nWe apologize for the misunderstanding. When we refer to \"training-free,\" we are highlighting that the DSP+ framework operates entirely with \"off-the-shelf\" models throughout its three stages. This approach contrasts with the conventional workflow of data collection followed by model fine-tuning. We will further clarify it in the next version.\n\n### **Integrating SoTA whole proof generators to the Prove phase**\n\nIt is quite possible to integrate SoTA whole proof generator (DeepSeek-Prover-V2 671B) into the prove phase of our framework. However, DeepSeek-Prover-V2 671B are currently impractical for us due to limited computational resources and the absence of public APIs. We intend to explore its integration into our future system once these constraints are resolved. Furthermore, its technical report indicates that DeepSeek-Prover-V2 already incorporates a DSP-like pipeline for data synthesis prior to reinforcement learning, suggesting that the model may have internalized this reasoning process."}, {"review_id": "4szz6liaip", "reviewer": "Reviewer_hncJ", "summary": "This paper revisits a technique called Draft, Sketch, Prove (DSP) on the performance of formal theorem proving with more advanced reasoning models. The authors identify that the original DSP framework has three independent phases that do not coordinate with each other. The authors propose DSP+ by tightly connecting the phases. Specifically, the draft phase leverages advanced reasoning models like DeepSeek-R1 while still making the response concise, the sketch phase checks for syntactically incorrect statements and repairs them and finally prove phase uses a more advanced BFS-prover. The results show that DSP+ attains strong performance close to SOTA DeepSeek Provers while using fewer inference tokens.", "questions": "1. Is it possible to integrate the techniques of DSP+ on top of the best models for proving such as DeepSeek-Prover-V2 671B and see if new SOTA results can be established?\n2. For the ablation of components, how does \"Draft + Sketch\" prove theorems? Is it just with the common tactics?\n3. In Figure 4, it seems that the No Format draft mode is better than Concise Steps, why not use this as the default and report main results with this setting?\n4. Are authors fully committed to release all code to reproduce the main results? I believe a paper of such type needs to release code in order to benefit the community.\n5. What is the iterative repair process discussed on Line 154?", "limitations": "The limitations section is very helpful and the authors provide various failure mode for their framework.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths\n- The paper revisits baselines that benefit from more advanced LLMs. This is crucial since baselines should be kept up to date in order to be fairly compared.\n- The method does not require additional training, which is easy to adopt for practitioners.\n\nWeaknesses\n- Although the number of inference tokens is fewer than some baselines, the framework has a sequential workflow with different models which could make wall-clock time or resource requirement larger than some baselines.\n- More weaknesses can be found in the Questions section.", "was_revised": true, "final_justification": "I have read the authors’ rebuttal as well as the comments from Reviewer eJnA. Overall, I concur that the work is largely empirical and engineering-focused. Nevertheless, I recognize the substantial performance improvements achieved and appreciate the authors’ commitment to open-sourcing their work. I also hope that future methods will consider this paper as a baseline, rather than the original DSP. My perspective may be somewhat subjective, as I am very familiar with DSP.", "rebuttal": "### **Clarifying time and resource requirement comparison**\n\nWhile sequential workflows may incur higher latency per problem compared to one-shot generators, our framework remains highly competitive due to several key optimizations. First, by maintaining a persistent session for the ensemble tree search (`lean_copilot`, `aesop`), we avoid the repetitive overhead of launching new Lean processes, a feature not found in many prior works. Furthermore, we reuse the compiled header environment, saving approximately 10 seconds per verification call. Finally, our system supports high-throughput parallelism—up to 112 workers can run simultaneously. \n\nRegarding resource efficiency, our approach offers significant advantages. It is completely training-free, avoiding the significant GPU and time costs required for post-training or fine-tuning. It also consumes fewer inference tokens—a hardware-independent advantage that directly reflects reduced latency and GPU utilization. Moreover, our experiments—conducted mostly using readily available APIs—require only a 7B parameter proof model, making it more cost-effective and accessible than recent baselines of 72B or 671B that lack commercial APIs.\n### **Integrating DSP+ with DeepSeek-Prover-V2 671B**\n\nIntegrating state-of-the-art whole proof generators like DeepSeek-Prover-V2 671B into the proving phase of our framework is highly feasible. However, its immediate adoption is impractical for us due to current computational resource limitations and the lack of public APIs. We plan to explore this integration into our future system once these constraints are alleviated. Notably, DeepSeek-Prover-V2's technical report indicates that it already incorporates a DSP-like pipeline for data synthesis prior to reinforcement learning, suggesting an internalization of this reasoning process.\n\n### **Clarifying how \"Draft + Sketch\" prove theorems**\n\nIn this setup, the Sketch model (DeepSeek-V3 671B) is directly prompted to output the final, complete Lean code directly given the natural language draft. This means it produces tactic-level code without any \"sorry\" placeholders, unlike the standard sketch model.\n\n### **Clarifying why not use No Format draft mode as the default (cf. Figure 4)**\n\nIn our initial experiments, the performance of \"No Format\" and \"Concise Steps\" under smaller-scale tests (and up to pass@64 in Fig. 4) is nearly identical. Therefore, we chose \"Concise Steps\" as the default because it produced more human-readable proof drafts (see Appendix K). \n\n### **Code release**\n\nYes. We are committed to open-sourcing both the code and data once the review is finalized.\n\n### **Clarifying the iterative repair process discussed on Line 154**\n\nThe iterative repair process involves three key steps:\n\n1. We parse the Lean code into a tree structure, using indentation to define its hierarchy.\n2. The Lean compiler then identifies all lines containing errors.\n3. For each error, we prune the corresponding node and its entire subtree from this code tree.\n\nThis automated, non-destructive repair method offers greater robustness compared to simple truncation. We'll elaborate on this process further in the revision."}]

Author rebuttal:

Meta-review: This paper develops a new version of Draft, Sketch, Prove (DSP, Jiang et al ICLR 2023), a method for formal theorem proving in interactive proof assistants. The new method, DSP+, achieves very strong performance, improving substantially upon the underlying models that it uses and exceeding the performance of methods based on different approaches to theorem proving (e.g., tactic-level tree search, full proof generation). This is in contrast to other attempts to adapt DSP to the Lean proof assistant, which showed only modest performance.

The three reviewers were split on their ratings, with two positive ratings (4, 5) and one negative rating (2). The negative review's primary concern was that DSP+ has limited novelty, amounting to a combination of many known components. However, the final judgement of novelty was left to the AC, and thus I will consider it closely here, since otherwise the reviewers were in favor of acceptance.

DSP+ has several interesting differences with DSP. DSP+ targets the Lean proof assistant rather the Isabelle proof assistant, which has several implications. Isabelle has access to powerful low-level automation (Sledgehammer) and typically follows a declarative proof style, which the original DSP took advantage of. Since Lean differs from Isabelle in these respects, it has been an open question whether a DSP-style approach is even suitable for Lean at all. Indeed, previous attempts have underperformed compared to alternatives, as I previously mentioned. Answering this question involved creating new components that were not present in the original DSP (e.g., hypothesis specification), figuring out many details, and justifying them through experiments. I view this as a valuable form of research.

The resulting system leads to a few interesting insights. For example, it is now clear that a DSP-style approach can achieve near state-of-the-art performance in Lean. This can impact the future direction of research in the area. Second, it shows that lower-level provers in the Lean toolchain (including tactic-style LLM provers such as BFS prover) are complementary to a higher-level sketching prover. This insight was not crystallized in the original DSP, since it relied on Sledgehammer in the Isabelle proof assistant.

Additionally, the authors use only open-weights models and will release the code, so DSP+ could serve as a new baseline or starting point for future research. Using only open-weights models and releasing code is becoming more rare in this sub-field, so this is a nice addition.

For these reasons, I agree with the evaluations of the positive reviewers. Overall, I believe that this paper offers an interesting and non-trivial extension of Draft, Sketch, Prove, and new insights that could impact the sub-fields of AI formal theorem proving and AI for mathematics. I recommend this paper for acceptance and think it would be a good addition to the NeurIPS program.
Decision: Accept (poster)