Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation Ruida Wang1 , Rui Pan1 , Pengcheng Wang1 , Shizhe Diao2 , Tong Zhang1 1
University of Illinois Urbana-Champaign, 2 NVIDIA
{ruidaw, ruip4, pw29}@illinois.edu, [email protected], [email protected]
arXiv:2606.19315v1 [cs.LG] 17 Jun 2026
Abstract
Enhancing the formal math reasoning capabilities of Large Language Models (LLMs) has become a key focus in both mathematical and computer science communities in recent years. While significant progress has been made in using state-of-the-art Auto-Regressive (AR) LLMs for formal theorem proving, these models suffer from inherent limitations. Their next-token prediction generation methods may yield suboptimal performance due to the challenges of long-range coherence and the compounding of errors over long sequences. Recent advancements in diffusion LLMs (dLLMs), which generate text through iterative denoising of a multi-token block, offer a promising alternative. However, the application of dLLMs to formal mathematics, where maintaining longrange coherence is critical, remains largely understudied. To address the challenges above, we propose Diffusion-Proof, to the best of our knowledge, the first framework to train and apply dLLMs for formal theorem proving. Our frameworks contain training and inference methods for two models. The first one is dLLMProver-7B, which performs whole-proof writing with long-range coherent tactic usage. The second one is dLLM-Corrector-7B, which is a novel large block diffusion-based correction model. It leverages the in-filling capabilities of dLLMs to perform local proof correction using bi-directional information. Extensive experiments demonstrate that Diffusion-Proof relatively significantly outperforms the AR LLM baseline trained under the same dataset. Diffusion-Proof achieves an absolute improvement of 1.61% on ProofNet-Test and 6.14% on MiniF2F-Test benchmarks compare to the baseline. Notably, Diffusion-Proof successfully resolves one IMO problem that more advanced thinking model DeepSeek-Prover-V2-7B (Ren et al., 2025) could not solve, showcasing the unique advantage of dLLMs in formal theorem proving.
1
Introduction
Building machine-learning systems capable of performing human-level reasoning based on rigorous logical rules has always been considered a fundamental goal for artificial intelligence (Wang et al., 2024). This capability is often evaluated through the derivation of complex formal mathematical proofs, where maintaining long-range coherence is essential (Yang et al., 2024a). However, the inherent ambiguity in natural language makes it challenging to formally verify the intermediate reasoning steps. To provide a trustworthy foundation for mathematical reasoning, multiple works have developed verifiable languages based on different theoretical foundations. Some apply the dependent type language, such as Lean (De Moura et al., 2015; Moura and Ullrich, 2021) and Coq (Coq, 1996), which enforce type safety to ensure logical consistency. Others employ higher-order logic, such as Isabelle (Paulson, 1994) and HOL (Harrison, 2009). Proving both types of systems allows explicit verification of every internal step, regardless of its complexity. The formal verification minimizes errors and prevents the hallucinations and logical inconsistencies often observed in natural language-based reasoning. With the rapid development of Large Language Models (LLMs), their significant potential in formal reasoning using Lean4 (Moura and Ullrich, 2021) has become a key area of research. Recent efforts focus on generating large-scale datasets (Ying et al., 2024; Wu et al., 2024; Xin et al., 2024a; Wang et al., 2024) and training models using methods ranging from standard Supervised Fine-Tuning (SFT) (Wang et al., 2024; Lin et al., 2025a) to advanced Reinforcement Learning (RL) (Ren et al., 2025; Wang et al., 2025a; Lin et al., 2025b). Latest research proposes multi-agent methods, from recursive decomposition of subgoals (Varambally
Block Diffusion Training Sample
Base dLLM
Cleaning Selection 5.5M Lean dataset
300k NL-FL mixture data
Correction block filling
/-<NL-analysis>-/ -- Rewrite the equation to have the terms involving x on one side and constants on the other side. rw [eq_comm] at h₀…
Block Diffusion Training
Selection Sub-goal decomp data
theorem lean_workbook_plus_79832 (x : ℝ) (h₀ : 5 + 3.5 * x = 2.5 * x - 25) : x = -30 := by
Block diffusion training
dLLMProver Correction training data
Diffusion Correction Training Sample theorem lean_workbook_21545 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hab : a + b + c = 3) : a ^ 2 / ( a + 1) + b ^ 2 / ( b + 1) + c ^ 2 / ( c + 1) ≥ a * b * c / ( a + b + c) * Real.sqrt ( a * b + b * c + c * a):= by … have h₂ : b ^ 2 / (b + 1) ≥ b ^ 2 / 4 := by gcongr; linarith <|fim_middle|><|fim_middle|>… have h₃ : c ^ 2 / (c + 1) ≥ c ^ 2 / 4 := by … have h₄ : … Large diffusion block
Diffusion Correction Training dLLMCorrector
covering correction window
(a) Data Collection & Model Training Initial Lean Proof Lean statement theorem mathd_algebra_215 (S : Finset ℝ) (h₀ : ∀ (x : ℝ), x ∈ S ↔(x + 3)^2 = 121) : ∑ k in S, k = -6 := by
dLLMProver
Fixed Lean Proof
Proof Done
theorem mathd_algebra_215 (S : Finset ℝ) (h₀ : ∀ (x : ℝ), x ∈ S ↔(x + 3)^2 = 121) : ∑ k in S, k = -6 := by have h₁ : <stat_1> := <proof_1> have h₂ : <stat_2> := <proof_2> have h₃ : <stat_3> := <proof_3> exact h₃ Block diffusion gen.
✅ ❌ with have statement error
dLLMCorrector
theorem mathd_algebra_215 (S : Finset ℝ) (h₀ : ∀ (x : ℝ), x ∈ S ↔(x + 3)^2 = 121) : ∑ k in S, k = -6 := by have h₁ : <stat_1> := <proof_1> have h₂ : <stat_2> := <fixed_proof> have h₃ : <stat_3> := <proof_3> exact h₃ Large diffusion block correction
(b) Proof Writing & Correction
Figure 1: Diffusion-Proof framework: (a) Data Collection and Model Training: We first collect a 5.5M Lean SFT dataset from previous works, then perform cleaning and selection to obtain 300k natural language (NL)-formal language (FL) mixture data to fine-tune Fast-dLLM-V2-7B into dLLM-Prover-7B. Subsequently, we select data with subgoal decomposition and perform block filling to formulate data for corrector training. The dLLM-Corrector-7B is fine-tuned by the dataset using Large-block correction training. (b) Proof Writing & Correction: The prover model firstly generates the complete proof for the Lean4 theorems using block-diffusion generation. If the verification fails but the skeleton is correct, the corrector model applies large diffusion block correction to adjust the subgoal proofs based on bi-directional information.
et al., 2025), to agentic RL methods (Wang et al., 2025c; Chen et al., 2025) for formal theorem proving. However, most, if not all, previous works on exploring LLMs’ usage in formal theorem proving are based on traditional Auto-Regressive (AR) LLMs. The AR models perform next-token prediction in a strict left-to-right manner. It has inherent problems, including potential exponential error accumulation (Dziri et al., 2023) and a lack of longrange coherence (Ye et al., 2025). Furthermore, the AR models are naturally unable to perform infilling proof correction. These make AR models have natural flaws for formal reasoning. On the other hand, diffusion LLMs (dLLMs) present a promising alternative in language generation by reformulating the task as an iterative denoising process of the multi-token block. Recent studies (Nie et al., 2025; Ye et al., 2025; Wu et al., 2025b; Bie et al., 2025) have demonstrated their potential in coding tasks, supported by efficient training and inference frameworks (Wu et al., 2025a). While dLLMs naturally benefit from longrange coherence and bi-directional awareness in generation, their application to formal reasoning remains largely understudied. To address the limitations of existing methods,
we propose Diffusion-Proof, to the best of our knowledge, the first framework for training and applying dLLMs for formal theorem proving. The overview of our framework can be found in Figure 1. Diffusion-Proof contains the training and inference methods of two 7B-parameter models that work synergically together, namely dLLM-Prover7B and dLLM-Corrector-7B. In the training stage of Diffusion-Proof, we collect 5.5 million records of theorem proving data from previous works, clean and select 300k records of SFT data. It is applied to fine-tune Fast-dLLM-V2-7B into dLLM-Prover7B to enhance its whole-proof writing capability. Subsequently, we introduce a novel Large Block Correction training method, enabling the model to perform local in-filling correction of formal proof with bidirectional information awareness. During inference, the dLLM-Prover-7B firstly generates proofs based on the theorem statement. If the initial proof is wrong but the proof skeleton is correct, we apply dLLM-Corrector-7B using large diffusion block generation to refine the proof locally. We summarize our contribution as follows: (1) To the best of our knowledge, we present DiffusionProof, the first framework for fine-tuning and applying the dLLMs for formal theorem proving. (2)
We introduce the novel large-block correction training and inference method that leverages the bidirectional information to perform in-filling correction. (3) Through extensive experiments, we demonstrate that Diffusion-Proof relatively significantly outperforms AR LLMs trained on the same dataset, achieving a 1.61% improvement on ProofNet-Test and a 6.14% improvement on MiniF2F-Test under pass@32. Notably, DiffusionProof successfully solves one IMO problem that the more advanced DeepSeek-Prover-V2-7B (Ren et al., 2025) could not solve. Our study highlights the unique advantages of dLLMs in theorem proving, and (as far as we know), as the first work in such field, we plan to release all training code, models, and datasets presented in this work.
2
Methodology
In this section, we introduce the details of the Diffusion-Proof framework. It is designed to leverage the long-range coherence and in-filling correction capabilities of diffusion LLMs (dLLMs) for formal theorem proving. We first present the preliminaries of dLLMs in Section 2.1. Subsequently, Section 2.2 details the data preparation and Section 2.3 presents model training. Finally, we present the proof writing and correction method that applies the trained model in Section 2.4. 2.1
Preliminaries
Consider a token sequence x = {x1 , x2 , · · · , xL } with length L, traditional Auto-regressive (AR) LLMs generate text sequentially following a stright left-to-right manner by modeling the conditional distribution Pθ (xi |x[0 : i − 1]), where θ is the AR model’s parameters. These models are trained to minimize cross-entropy loss of predicted tokens based only on previous tokens. Diffusion LLMs, on the other hand, approach text generation differently by introducing a time step t ∈ [0, 1] and adding noise to create x(t) , where tokens are masked independently with probability t. The model Pω (x(0) |x(t) ) iteratively predicts the original tokens from the noisy input. The training objective for dLLMs is defined as: P (t) L(θ) = −Et,x(0) ,x(t) [ L = [MASK]] · i=1 I[xi (0)
log Pω (xi |x(t) ) In the Diffusion-Proof, we apply the block dLLM framework as the base model. Unlike the traditional dLLMs, the sequence is divided into blocks
of size B, with bi-directional attention restricted to individual blocks while preserving causal relationships between blocks. During inference, the block dLLMs iteratively decode one block at a time until a stopping condition is reached. This process balances the diffusion generation and the flexible nature of AR models. 2.2
Data Collection & Pre-process
This section outlines the data collection and preprocessing steps for fine-tuning dLLM-Prover7B and dLLM-Corrector-7B models in DiffusionProof. While previous works (Wu et al., 2024; Lin et al., 2025a; Dong and Ma, 2025; Wang et al., 2025c,a) have contributed millions of theorem proof records. The data lacks proper structuring. Specifically, these datasets are often in their raw input-output form and lack a clear separation between FL statements, NL statements, and FL proofs. Thus, to uniform the dataset, we extract and standardize the data using rule-based methods to separate NL statements, FL statements, and FL proofs. Additionally, proof data from STP (Dong and Ma, 2025) lacks NL components and is used as syntax understanding data for Lean. In total, we obtained 5,595,798 records of code-completion proofs and sampled 300k records to create the SFT dataset for prover. We maintain an approximate ratio of 1:2 between pure Lean proofs and those with NL annotations and comments. Following the DeepSeek-Prover (Xin et al., 2024a) standard, we format the data in a code-completion style without adopting a chat template. Examples of the training data are provided in Section E.1. We then prepare the data for the training corrector by sampling from the 300k data that has subgoal decomposition in its proof. For a Lean proof, subgoals are defined as internal statements and their proofs in the theorem proof are marked by the have keyword, as illustrated in Figure 2. We organize the top-level subgoal proof into token blocks of size 256 by filling the proof with a placeholder <|fim_middle|> token. The data trains the model to fill placeholder token when a block of proof is finished. Additionally, we only consider one to fill in the block at a time for a proof containing multiple subgoals. Following the above preprocessing, we construct a dataset containing 300k records of SFT data for prover training and 128k records for corrector training.
theorem lean_workbook_21545_1 (a b c: R) (ha: 0 ≤ a) (hb: 0 ≤ b) (hc: 0 ≤ c) (hab: a + b + c = 3) : a^2 / (a + 1) + b^2 / (b + 1) + c^2/(c + 1) ≥ a*b*c / (a + b + c) * Real.sqrt (a*b + b*c + c*a):= by rw [hab] have : 0 ≤ a*b*c := by positivity have h1 : a^2 / (a + 1) ≥ a^2 / 4 := by gcongr; linarith have h2 : b^2 / (b + 1) ≥ b^2 / 4 := by gcongr; linarith have h3 : c^2 / (c + 1) ≥ c^2 / 4 := by gcongr; linarith have h4 : a^2 / 4 + b^2 / 4 + c^2 / 4 ≥ a*b*c / 3 * Real.sqrt (a*b + b*c + c*a) := by have : a*b*c ≤ 1 := by nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a)] have : Real.sqrt (a*b + b*c + c*a) ≤ 2 := by apply Real.sqrt_le_iff.mpr constructor · positivity · nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a)] nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a)] nlinarith
Figure 2: Example of data with subgoal-decomposition, the have hi at top-level is the decomposed subgoal
2.3
Prover & Corrector Training
After obtaining the dataset, we fine-tune the dLLMProver-7B and dLLM-Corrector-7B models. For the prover model, we start with the base model Fast-dLLM-V2-7B (Wu et al., 2025a) and employ a standard text-to-text training framework under the Lean4 code-completion task. To ensure the stability of training, we maintain the diffusion block size to be 32, which is consistent with the original model. Additionally, we implement curriculum data sorting (Wang et al., 2024), which organizes the training by increasing order of proof complexity based on proof length. This approach enables the model to first learn simpler proofs before progressing to more complex ones, thereby stabilizing the loss curve. Following the above training process on the 300k SFT dataset, the dLLM-Prover-7B becomes proficient in formal theorem proving. Such training enables the model to write formal proofs with better long-range coherence in the sense of planning and tactic usage through block diffusion generation. Subsequently, we further leverage the bidirectional information understanding of dLLMs by proposing a large-block training method for the corrector. Under such a training method, we extend the diffusion block size from 32 to 512 and apply loss to both the subgoal proof block and the placeholder token. It aims to train the model to write local corrections and fill the rest of the block with placeholder tokens. We apply such a training method to dLLM-Prover-7B and obtain the dLLMCorrector-7B. This enables the corrector to utilize
information from the extended diffusion block to perform in-filling corrections on subgoals by leveraging bi-directional information. 2.4
Proof Writing & Correction
Using the dLLM-Prover-7B and dLLM-Corrector7B trained from above steps, Diffusion-Proof is able to perform both whole-proof generation and error correction with long-range coherence. During the whole-proof writing stage, the dLLM-Prover7B generates proofs based on the NL and Lean4 statement of the theorem. This process is based on the proof generation method from DeepSeekProver-V1 (Xin et al., 2024a). If the initial proof by the prover fails the Lean verification but all the top-level subgoal statements and their usages are correct, we perform a largeblock correction using the corrector. The correction process begins with deleting the proofs in the subgoal that causes the error and replacing them with a 256-token sequence of diffusion generation mask <|MASK|>. The dLLM-Corrector-7B then refines these masked sections using 512-length diffusion blocks, such that a large block can leverage both prefix and suffix context to perform in-filling corrections. To encourage more creative and accurate proof writing, we set the generation temperature to 1.2. Additionally, the confidence of one token to be denoised is increased to 0.95 to ensure the robustness of the generation. The input-output example for dLLM-Corrector can be found in Appendix F. Through the above inference process, we are able to perform long-range coherent proof generation that surpasses the limitations of AR generation
and effectively fixes local errors through in-filling corrections.
3
Experiments
We evaluate Diffusion-Proof on Lean4 theorem proving through extensive experiments on MiniF2F-Test (Zheng et al., 2021) and ProofNetTest (Azerbayev et al., 2023) benchmarks. Section 3.1 and 3.2 describe the experiment setup and implementation details. Subsequently, Section 3.3 reports the main results of our experiment. Furthermore, Section 3.4 provides further analyses in the training-loss study; Section 3.5 analyzes the performance after dropping out the key component, and Section 3.6 offers detailed case studies. 3.1
Experiment Setup
3.1.1 Dataset and Task We evaluate the formal reasoning capabilities of the Diffusion-Proof framework by MiniF2FTest (Zheng et al., 2021) and ProofNet-Test (Azerbayev et al., 2023) benchmarks. These datasets are frequently employed in major studies on the LLM formal reasoning field (Xin et al., 2024a; Ren et al., 2025; Wang et al., 2024; Dong and Ma, 2025; Lin et al., 2025b; Wang et al., 2025c). The MiniF2F-Test datasets comprise 244 math problems formalized in Lean4. Its difficulty ranges from high-school competition problems to elementary undergraduate-level problems. The problems include formalized competition problems from IMO, AIME, and AMC, a subset of the Math-500 benchmark (Lightman et al., 2023), and hand-crafted problems with a similar level of difficulty. On the other hand, the ProofNet-test contains 186 theorems derived from college textbooks, covering advanced topics such as real and complex analysis, linear algebra and topology. The task for the LLMs is to generate formal proofs for theorems based on their NL and Lean4 statements using direct code-completion. We do not allow Long CoT thinking process because both Diffusion-Proof and baselines does not support such long context. 3.1.2 Baselines & Evaluation Metric The primary goal of this study is to evaluate the potential of dLLMs in formal theorem proving, particularly their capability to achieve long-range coherent tactics usage. Thus, for a fair comparison, we use Qwen-2.5-Instruct-7B (Qwen et al., 2025), which is fine-tuned on the same training dataset
as dLLM-Prover-7B and employs the same text-totext training method. The SFT version is named Qwen-2.5-Lean-SFT-7B in our experiment. We select this baseline because Qwen-2.5-Instruct-7B is the base model for Fast-dLLM-V2-7B (Wu et al., 2025a), and neither model undergoes additional post-training focused on mathematics or Lean4 coding. Therefore, both models share a comparable foundation in formal reasoning. It makes the performance improvement of Diffusion-Proof a strong indicator of the effectiveness of the diffusion-based framework. We emphasize that the primary goal of this study is to investigate whether dLLMs offer architectural advantages over AR models for formal reasoning, rather than achieving state-of-the-art performance. Therefore, we deliberately control for confounding factors and compare only the generation paradigm. For reference, contemporary SFTonly provers like DeepSeek-Prover-V1.5 achieve approximately 48.2% on MiniF2F with larger-scale training, suggesting the meaningfulness of our framework. To measure the performance, we adopt the standard pass@32 metric applied in almost all previous studies. The details of the evaluation metric can be found in Appendix G. 3.2
Implementation Details
This section outlines the implementation details for the prover, corrector, and baseline models. The prover and baseline models are fine-tuned on the SFT dataset described in Section 2.2 using a learning rate of 1E-5 and a context length of 2,048 tokens. On the other hand, the corrector is trained with a reduced learning rate of 5E-6. All models share the same other training configuration, employing a learning rate scheduler with 3% warmup steps. Training is conducted on 4-card H100 GPUs with a global batch size of 64. Each model requires approximately one day of training. For detailed training and inference setup, please refer Appendix B. 3.3
Results
The main evaluation results is presented in Table 1. It shows that Diffusion-Proof achieves an accuracy rate of 50.00% on MiniF2F and 7.53% on ProofNet. The result surpasses the Qwen-2.5-Lean-SFT-7B baseline by 6.14% and 1.61%, respectively. The baseline records 43.85% on MiniF2F and 5.91% on ProofNet.
Dataset
Data Number
Qwen-2.5-Lean-SFT-7B
Diffusion-Proof
Improvement
ProofNet-Test
186
5.91%
7.53%
1.61%
MiniF2F-Test
244
43.85%
50.00%
6.14%
MiniF2F-Test by problem type IMO AIME AMC Algebra Number Theory Induction
20 15 45 88 68 8
5.00% 33.33% 22.22% 55.68% 58.82% 25.00%
15.00% 33.33% 26.67% 67.05% 63.24% 25.00%
10.00% 0.00% 4.44% 11.36% 4.41% 0.00%
Table 1: Main experiment result of Diffusion-Proof under MiniF2F-Test (Zheng et al., 2021) and ProofNetTest (Azerbayev et al., 2023) with pass@32 metric and 32 corrections for each valid theorem
A detailed analysis of MiniF2F results indicates that Diffusion-Proof outperforms the baseline across most problem types. Notably, it demonstrates relatively significant gains in challenging IMO and AMC problems, solving two additional problems in each category. Furthermore, comparably significant improvements are also observed in Algebra and Number Theory. It highlights the framework’s enhanced formal reasoning capabilities in both fields. On the more challenging ProofNet benchmark, despite the lower absolute improvements, Diffusion-Proof also shows clear progress over the baseline. We also compare Diffusion-Proof with broader baselines and the performance of Diffusion-Proof on harder problems that require longer proofs. Detailed results are provided in Appendix C.1 and C.2. 3.4
Validation Loss Study
In this section, we investigate why dLLMs outperform AR models in formal proof writing based on the validation loss. Using the 190 correct Lean theorem proofs from MiniF2F-Test completed by DeepSeek-Prover-V2 (Ren et al., 2025). We compare the cross-entropy loss of different models under the pure causal mask. For dLLMs, this comparison is achieved by setting the diffusion block size to 1. We evaluate four models: the fine-tuned dLLM (dLLM-Prover-7B), the finetuned AR model (Qwen-2.5-Lean-SFT-7B), the base dLLM (Fast-dLLM-V2-7B), and the base AR model (Qwen-2.5-Instruct-7B). The validation loss distribution is presented in Figure 3, whith detailed plots available in Appendix H. The results reveal that the two base models exhibit nearly identical loss distributions, as well as two fine-tuned models. The statistical analysis shows that the Pearson correlation for SFT models is 0.9846 and for base models, it is 0.9838.
Figure 3: Validation loss for trained dLLM, trained AR LLM, base dLLM, and base AR LLM
The p-value for both correlations is under 10−100 . This demonstrates that, in terms of causal attention loss, the models within each category are almost equivalent. However, the fine-tuned dLLM relatively significantly outperforms the SFT AR model across all benchmarks. We attribute this advantage to the natural diffusion generation. It features iterative refinement in the diffusion block, enhanced long-range coherence, and bi-directional information awareness. The loss comparison highlights the superior capability of dLLMs in formal reasoning. 3.5
Ablation Study in Correction Process
This section presents an ablation study to evaluate the impact of the correction process in the Diffusion-Proof framework. The corrector contributes to solving 4 out of 122 problems in the MiniF2F-Test, namely imo_1962_p2, amc12b_2002_p7, mathd_algebra_215, and mathd_numbertheory_521. It results in a 1.64% improvement in the benchmark. These problems typically involve complex subgoal decomposition and require the corrector to further split objectives into multiple cases to complete the proof. The detailed case study is presented in Section 3.6.1. On the other side, even without the corrector, the
dLLM-Prover-7B still outperforms the baseline by 4.51% on MiniF2F, validating the effectiveness of dLLMs for formal reasoning. However, on the ProofNet-test dataset, the corrector’s local proof fix proves no additional theorems. This is because such a dataset focuses more on advanced knowledge over complex subgoal division or long-range reasoning. With its inherent difficulty, such a dataset is naturally not suitable for a corrector’s local proof fix. We further perform the analysis using the AR model and dLLM-Prover-7B to replace the corrector and to compare in-place correction with top-level correction; the results are shown in Appendix C.3. 3.6
Case Study
This section presents a detailed case study to evaluate the qualitative performance of Diffusion-Proof. We only present analysis here with additional examples provided in Appendix I. 3.6.1
Theorems proved by corrector
This section analyzes the performance of dLLMCorrector-7B in successfully performing local theorem proofs based on a skeleton generated by dLLM-Prover-7B. We select two representative cases, namely mathd_algebra_215 and mathd_numbertheory_521, for the case study. In the case of mathd_algebra_215, both the initial failed proof (Figure 10) and the corrected proof (Figure 9) share the same global structure. The proof begins by establishing the elements of the set S and then demonstrating that these elements satisfy the given conditions. However, the original proof struggles to apply tactics for handling complex algebraic computations. On the contrary, the corrector generates the entire proof in a single diffusion block, enabling a more strategic planning. The process begins with generating the internal have decomposition, followed by proving each subgoal. It demonstrates the corrector’s capability to perform long-range coherent reasoning and tactic usage. Additionally, the final intro h steps mirror the type refinement seen in the latter parts of the proof. It further highlights the model’s bi-directional context awareness, which enables it to complete the proof based on suffix information. In the case of mathd_numbertheory_521, the original proof fails due to incorrect usage of linarith and rw tactics. These tactics are less effective in the domain of natural numbers compared to omega, which is used in the corrected
proof. Leveraging the corrector’s long-range generation capability and large attention block, it identifies the appropriate tactic and applies it correctly. Notably, the proof of h6 is generated before h4 , and the bi-directional awareness of the diffusion corrector allows the model to learn from the suffix generation of the same block directly. This further proves the advantages of the corrector’s large diffusion block in capturing and utilizing contextual information effectively. 3.6.2
Compare to AR baseline model
We analyze two representative cases where dLLMProver-7B succeeds while the AR baseline fails, namely imo_1983_p6 and mathd_algebra_188. The complete examples are provided in Appendix I.2. In the case of imo_1983_p6, both models attempt to prove the inequality by supplying complex conditions to the tactic linearity. The dLLM’s block diffusion generation enables it to take a more comprehensive strategy, providing suitable input for the theorem mul_nonneg. In contrast, the AR model fails to provide adequate inputs, rendering the wrong theorem proof. In the mathd_algebra_188, the AR model applies incorrect tactics in both subgoal proofs, leaving the theorem incomplete. On the other hand, the dLLM employs a more effective approach. It successfully solves the subgoals. This comparison highlights the dLLM’s ability to perform coherent planning, a capability that the AR models lack. 3.6.3
Compare to DeepSeek-Prover-V2
One surprising result from our experiments is that Diffusion-Proof successfully completes the proof for imo_1962_p2. The problem fails the DeepSeekProver-V2-7B (Ren et al., 2025) under pass@32 with Long CoT reasoning. The detail of this example is presented in Appendix I.3. As shown in Figure 16, despite DS-Prover providing sufficient natural language analysis during the Long CoT process, it lacks a detailed proof plan and coherent tactic usage. This deficiency leads to repeated self-corrections in the natural language plan without providing additional insight into Lean beyond direct code writing. Although the model easily proves the condition −1 ≤ x. It fails on the second case, by providing the wrong direction of inequality in h19 , which collapses the entire proof. In contrast, the corrector in Diffusion-Proof demonstrates a more robust and coherent tactic usage. It successfully addresses the long-range dependen-
cies required for this proof. By leveraging its large diffusion block, the corrector can have better planning and execution of complex reasoning steps. This highlights the potential of dLLMs in formal theorem proving, particularly for tasks requiring intricate tactic planning.
4
Related Work
4.1
LLMs For Formal Theorem Proving
In recent years, LLMs have gained prominence in formal theorem proving with Lean4 (Moura and Ullrich, 2021) emerging as a widely used environment for formal verification tasks. Multiple works have contributed millions of records of theorem statements and proofs (Wang et al., 2024; Wu et al., 2024; Lin et al., 2025a; Dong and Ma, 2025), establishing a robust foundation for the domain. In the sense of model training, early advancements in training LLMs for theorem proving introduced SFT frameworks, including Expert Iteration (Polu et al., 2022), Re-Prover (Yang et al., 2024b), TheoremLlama (Wang et al., 2024), DeepSeek-Prover-V1 (Xin et al., 2024a), BFSProver (Xin et al., 2025), and Goedel-ProverV1 (Lin et al., 2025a). Subsequent developments leveraged RL with verifier rewards, leading to the reasoning systems such as MA-LoT (Wang et al., 2025b), Kimina-Prover (Wang et al., 2025a), Goedel-Prover-V2 (Lin et al., 2025b), and DeepSeek-Prover-V2 (Ren et al., 2025). More recently, agentic-RL has been actively explored for multi-agent proving systems, leading to frameworks like GAR (Wang et al., 2025c) and SeedProver-V1.5 (Chen et al., 2025), which further improved the performance in theorem proving. Despite these significant strides, most, if not all, existing approaches rely on AR LLMs, leaving the dLLM largely under-explored in the context of formal reasoning. 4.2
Diffusion LLMs
Diffusion Large Language Models (dLLMs) have emerged as a promising alternative to AutoRegressive (AR) models for text generation. Unlike AR models, which generate tokens sequentially from left to right, dLLMs generate text using a denoising process. It progressively refines the masked tokens through multiple diffusion steps (Nie et al., 2025; Ye et al., 2025). This iterative approach inherently supports long-range coherence, a feature often lacking in AR architectures.
Early foundational efforts, such as LLaDA (Nie et al., 2025) and Dream (Ye et al., 2025), demonstrated the potential of this paradigm. Subsequent advancements, including efficient inference frameworks like dInfer (Ma et al., 2025) and Fast-dLLM family (Wu et al., 2025b) have substantially improved the practical deployment of dLLMs through innovations in KV-cache management and systemlevel optimizations. Additionally, block diffusion techniques (Wu et al., 2025a) extend diffusion models beyond fixed-length generation, enabling greater flexibility. LLaDA 2.0 (Bie et al., 2025) scales dLLMs to 100B parameters and has showcased the viability of these architectures at the frontier of language modeling. Despite their growing application in downstream tasks (You et al., 2025; Dong et al., 2025; Shi et al., 2025), applying dLLMs for formal reasoning is still an underexplored field. This gap highlights an opportunity for further research into applying dLLMs to tasks requiring rigorous logical coherence.
5
Conclusion
This paper presents Diffusion-Proof, a comprehensive training and inference framework for applying diffusion LLM (dLLM) for formal theorem proving. Diffusion-Proof aims to address limitations of Auto-Regressive (AR) models, such as their inherent lack of long-range coherence in proof generation and inability to perform bi-directional aware, in-filling proof corrections. DiffusionProof tries to overcome these challenges by integrating two key components: dLLM-Prover and dLLM-Corrector. The prover employs block diffusion training and generation to enable long-range coherent tactic usage and improve long-range proof planning. The corrector, a large-block diffusion model, performs in-filling proof corrections using bi-directional context, allowing the system to tackle more complex problems. Extensive experiments demonstrate that Diffusion-Proof framework outperforms the AR baseline trained under the same dataset by 6.14% in MiniF2F-Test and 1.61% in ProofNet-Test under pass@32. Notably, with the integration of the corrector, Diffusion-Proof successfully solves an IMO problem that much stronger DeepSeek-Prover-V2-7B cannot handle. Beyond theorem proving, Diffusion-Proof provides a promising approach by highlighting the unique advantages of dLLMs in tasks that require long-range coherence and precise reasoning.
Limitations Despite Diffusion-Proof presenting promising results, there are areas that warrant further exploration as the application of dLLMs in formal reasoning and other downstream tasks is still in its nascent stages. First, this work is conducted with limited computational resources, which restricts the training scale below the state-of-the-art opensource AR provers such as Goedel-Prover-V2 (Lin et al., 2025b) and DeepSeek-Prover-V2 (Ren et al., 2025). Second, the current base model’s limited Long CoT capability prevents a comprehensive exploration of dLLM’s potential for long thinking in theorem proving. Third, this work focuses only on Lean4. Although benchmarks such as MiniF2F include partial formalizations in other theorem provers, training a dLLM prover requires large-scale proof corpora, verification infrastructure, and model-specific preprocessing. Comparable resources are currently much stronger for Lean4 than for theorem provers such as Isabelle in our setting. Finally, this study focuses primarily on the empirical improvements and does not delve into the theoretical foundations of dLLMs. These aspects provide valuable opportunities for future research to scale training further, develop models with enhanced reasoning capabilities, and establish a theoretical framework to further understand and advance the usage of dLLMs in formal reasoning tasks.
References Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. 2023. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433. Tiwei Bie, Maosong Cao, Kun Chen, Lun Du, Mingliang Gong, Zhuochen Gong, Yanmei Gu, Jiaqi Hu, Zenan Huang, Zhenzhong Lan, and 1 others. 2025. Llada2. 0: Scaling up diffusion language models to 100b. arXiv preprint arXiv:2512.15745. Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, and 1 others. 2025. Seedprover 1.5: Mastering undergraduate-level theorem proving via learning from experience. arXiv preprint arXiv:2512.17260. Projet Coq. 1996. The coq proof assistant-reference manual. INRIA Rocquencourt and ENS Lyon, version, 5.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer. Kefan Dong and Tengyu Ma. 2025. Stp: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212. Xuanzhao Dong, Wenhui Zhu, Xiwen Chen, Zhipeng Wang, Peijie Qiu, Shao Tang, Xin Li, and Yalin Wang. 2025. Llada-medv: Exploring large language diffusion models for biomedical image understanding. arXiv preprint arXiv:2508.01617. Nouha Dziri, Ximing Lu, Melanie Sclar, Xiang Lorraine Li, Liwei Jiang, Bill Yuchen Lin, Sean Welleck, Peter West, Chandra Bhagavatula, Ronan Le Bras, and 1 others. 2023. Faith and fate: Limits of transformers on compositionality. Advances in Neural Information Processing Systems, 36:70293–70332. John Harrison. 2009. Hol light: An overview. In International Conference on Theorem Proving in Higher Order Logics, pages 60–66. Springer. Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. 2023. Let’s verify step by step. In The Twelfth International Conference on Learning Representations. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. 2025a. Goedel-prover: A frontier model for open-source automated theorem proving. Preprint, arXiv:2502.07640. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, JuiHui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, and 1 others. 2025b. Goedelprover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613. Yuxin Ma, Lun Du, Lanning Wei, Kun Chen, Qian Xu, Kangyu Wang, Guofeng Feng, Guoshan Lu, Lin Liu, Xiaojing Qi, and 1 others. 2025. dinfer: An efficient inference framework for diffusion language models. arXiv preprint arXiv:2510.08666. Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer. Shen Nie, Fengqi Zhu, Zebin You, Xiaolu Zhang, Jingyang Ou, Jun Hu, Jun Zhou, Yankai Lin, Ji-Rong Wen, and Chongxuan Li. 2025. Large language diffusion models. arXiv preprint arXiv:2502.09992.
Lawrence C Paulson. 1994. Isabelle: A generic theorem prover. Springer. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344. Qwen, :, An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, Huan Lin, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Yang, Jiaxi Yang, Jingren Zhou, and 25 others. 2025. Qwen2.5 technical report. Preprint, arXiv:2412.15115.
Chengyue Wu, Hao Zhang, Shuchen Xue, Zhijian Liu, Shizhe Diao, Ligeng Zhu, Ping Luo, Song Han, and Enze Xie. 2025b. Fast-dllm: Training-free acceleration of diffusion llm by enabling kv cache and parallel decoding. arXiv preprint arXiv:2505.22618. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024a. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333.
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, and 1 others. 2025. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, and 1 others. 2024b. Deepseekprover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152.
Teng Shi, Chenglei Shen, Weijie Yu, Shen Nie, Chongxuan Li, Xiao Zhang, Ming He, Yan Han, and Jun Xu. 2025. Llada-rec: Discrete diffusion for parallel semantic id generation in generative recommendation. arXiv preprint arXiv:2511.06254.
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. 2025. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438.
Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. 2025. Hilbert: Recursively building formal proofs with informal reasoning. arXiv preprint arXiv:2509.22819.
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. 2024a. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075.
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, and 1 others. 2025a. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354. Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, and Tong Zhang. 2025b. Ma-lot: Model-collaboration lean-based long chain-of-thought reasoning enhances formal theorem proving. arXiv preprint arXiv:2503.03205. Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, and Tong Zhang. 2025c. Gar: Generative adversarial reinforcement learning for formal theorem proving. arXiv preprint arXiv:2510.11769. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. 2024. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203. Chengyue Wu, Hao Zhang, Shuchen Xue, Shizhe Diao, Yonggan Fu, Zhijian Liu, Pavlo Molchanov, Ping Luo, Song Han, and Enze Xie. 2025a. Fast-dllm v2: Efficient block-diffusion llm. arXiv preprint arXiv:2509.26328.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2024b. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36. Jiacheng Ye, Zhihui Xie, Lin Zheng, Jiahui Gao, Zirui Wu, Xin Jiang, Zhenguo Li, and Lingpeng Kong. 2025. Dream 7b: Diffusion large language models. arXiv preprint arXiv:2508.15487. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847. Zebin You, Shen Nie, Xiaolu Zhang, Jun Hu, Jun Zhou, Zhiwu Lu, Ji-Rong Wen, and Chongxuan Li. 2025. Llada-v: Large language diffusion models with visual instruction tuning. arXiv preprint arXiv:2505.16933. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110.
A
Discussion
A.1
AI usage
This work utilized Copilot to assist with code writing and OpenAI’s models to correct grammatical issues in the paper. All the ideas of the paper are original. A.2
Potential Risk
This work focuses on applying a new form of model beyond AR LLMs to physics theorem proving tasks; there is no foreseeable potential risk for this paper. A.3
Discussion on Data
The data used in this paper are based on opensource data from previous peer-reviewed works, which adhere to the ethics standards of major conferences, introducing no foreseeable risk of leaking personally identifiable information or offensive content. A.4
Discussion on License and Scientific Artifact Use
The datasets we use are published under the MIT License, and the base model Qwen-2.5 is published under the Apache 2.0 License. When we opensource the model, it follows the Apache 2.0 License, and the dataset follows the MIT License. Additionally, with internal checks, authors agree that the scientific artifact follows the original intention.
B
Additional Implementation Detail
The global batch size is implemented with per-GPU batch size 2 and gradient accumulation 8. Training dLLM-Prover-7B and Qwen-2.5-Lean-SFT-7B each takes approximately 96 H100 GPU-hours, while training dLLM-Corrector-7B takes an additional 48 H100 GPU-hours. During evaluation, the complete Diffusion-Proof pipeline, including whole-proof generation, Lean verification, and correction, takes about 16 hours on our machine. The AR baseline takes about 24 hours without vLLM optimization.
C
Additional Experiment Results
C.1
Compare with Broader Baselines
In this section, we provide a detailed comparison of provers with different sizes and training methods to better demonstrate the position of Diffusion-Proof
in the entire prover ecosystem. The results are demonstrated in Table 2. From these results, we observe that DiffusionProof, trained only on 300k data with standard SFT, outperforms AR-based SFT models on larger datasets and achieves results comparable to earlystage RL methods. This demonstrates the potential of diffusion models for formal theorem proving. However, the lack of the RLVR (Reinforcement Learning with Verifiable Feedback) technique and Long CoT reasoning currently limits our model’s ability to surpass SOTA AR provers. This result demonstrates that diffusion provers provide a stronger foundation for models and point the future direction of developing better RL methods for the field. C.2
Long Proof Subset Comparison
To evaluate whether the gain is concentrated in problems requiring longer formal derivations, we sort MiniF2F-Test problems by the length of released DeepSeek-Prover-V2 proofs and evaluate performance on the longest subsets. As shown in Table 3, Diffusion-Proof solves 5/54 problems on the longest 25% subset and 26/108 problems on the longest 50% subset, compared with 4/54 and 20/108 for the AR baseline. The larger gap on the longest half of the benchmark supports our hypothesis that block diffusion generation is particularly useful when proof construction requires longer-range tactic consistency. More surprisingly, Diffusion-Proof successfully solves one problem (imo_1962_p2) in MiniF2FTest that the more advanced DeepSeek-Prover-V27B (Ren et al., 2025), equipped with Long CoT, fails to prove under pass@32. This further highlights the unique advantage of dLLMs in generating long-range coherent proofs that even more sophisticated reasoning models struggle to complete. C.3
Additional Ablation Study on Correction Process
We further test whether a unified model can replace the proposed dual-model design by using dLLMCorrector-7B for both whole-proof writing and correction. This pure-corrector setup reaches only 40.98% on MiniF2F-Test, compared with 50.00% for the proposed pipeline. The result indicates that large-block correction training improves local infilling behavior but harms first-attempt wholeproof generation, supporting the separation between global proof writing and local correction.
Method
Size
Training / Inference Setting
MiniF2F-Test
TheoremLlama (Wang et al., 2024) Lean-STaR DeepSeek-Prover-V1 (Xin et al., 2024a) DeepSeek-Prover-V1.5 (Xin et al., 2024b) Kimina-Prover-Preview (Wang et al., 2025a) DeepSeek-Prover-V2 (Ren et al., 2025) Diffusion-Proof
8B 7B 7B 7B 1.5B 7B 7B
AR SFT AR SFT / expert iteration AR SFT AR SFT + RL AR SFT + RLVR + Long CoT AR SFT + RLVR + Long CoT dLLM SFT
35.7% 46.3% (pass@64) 46.3% 50.0% 56.2% 70.49% 50.0%
Table 2: Contextual comparison with specialized theorem provers. This table is not a controlled comparison because the systems differ in data scale, RL usage, search, and Long CoT reasoning. MiniF2F Subset
Diffusion-Proof
Qwen-Lean-SFT-7B
Longest 25% Longest 50%
5/54 (9.26%) 26/108 (24.07%)
4/54 (7.41%) 20/108 (18.52%)
Table 3: Performance on MiniF2F-Test subsets with the longest released DeepSeek-Prover-V2 proof lengths. Model / Correction Setting dLLM-Corrector-7B as unified model dLLM-Prover-7B only dLLM-Prover-7B + dLLM-Corrector-7B AR line-level rewrite correction dLLM in-place correction dLLM top-level correction
MiniF2F-Test 40.98% 48.36% 50.00% +1 problem +2 problems +4 problems
Table 4: Ablations for dual-model design and correction strategy on MiniF2F-Test. The lower block reports additional problems solved by each correction method.
We also compare the top-level correction design with an in-place correction baseline that removes the erroneous line and regenerates the remaining proof inside the same subgoal. In-place correction solves 2 additional MiniF2F-Test problems, while top-level correction solves 4. This suggests that regenerating the entire top-level subgoal proof gives the corrector more freedom to revise the local proof trajectory, whereas in-place correction remains constrained by earlier potentially misleading tactic choices. Finally, we equip the AR baseline with a correction mechanism by asking Qwen2.5-Lean-SFT-7B to rewrite from the line before the first error. This corrects only one problem, mathd_algebra_275, which is already solved by dLLM-Prover-7B in whole-proof generation.
D
Error Analysis
We analyze seven representative failed proofs to identify common limitations of Diffusion-Proof. Four examples are caused by overconfident use of arithmetic tactics such as linarith or nlinarith: induction_pord1p1on2powklt5on2, amc12_2000_p20, amc12a_2020_p15, and algebra_2varlineareq_fp3zeq11_
3tfm1m5zeqn68_feqn10_zeq7. In these cases, the generated proof often follows a plausible high-level algebraic plan, but then asks Lean arithmetic tactics to discharge obligations that require missing nonlinear, complex-number, or domain-specific transformations. For example, in amc12a_2020_p15, the model attempts to derive complex-valued polynomial consequences using arithmetic tactics that are not sufficient for the goal. One example, amc12a_2021_p19, is caused by invalid tactic usage. The model invokes simplification tactics with theorem combinations that do not make progress in Lean, indicating that the tactic pattern is locally plausible but not applicable to the current goal state. The remaining two examples, imo_1981_p6 and amc12b_2020_p13, exceed the current model capacity and show repetitive or incomplete proof endings. These failures occur on problems requiring substantially longer decomposition or specialized identities, suggesting that stronger Long CoT reasoning, verifier-guided self-reflection, or additional difficult-proof data may be needed.
E
Training data examples
E.1
dLLM-Prover SFT Data Example
The training input-output example for dLLMProver is presented in Figure 5. E.2
dLLM-Corrector Data Example
The input and output example for dLLM-Corrector is presented in Figure 6. Additionally, we demonstrate the extent to which a single 512-token diffusion block can cover in the example. From the data example, we can observe that the target block for correction is h3 , the training diffusion block covers both prefix and suffix. Through training on the presented data, the corrector model learns to write proofs for subgoals with awareness of bidirectional information.
F
Input-output Examples for corrector
The input example for the corrector is presented in Figure 7, and the output example is in Figure 8. From the example, we can see that the input sequence replaces the original wrong proof in the h1 with a 256 mask token and leaves the corrector to perform in-filling correction. For the output example, we can see the model successfully writes the proof for the decomposed subgoal and learns to fill the extra space for the diffusion block with placeholder tokens. This indicates the success of our training in the corrector, enabling it to perform in-filling correction and complete the proof with placeholder tokens.
G
Evaluation Metrics
The pass@32 evaluation we apply means that, given a theorem statement, the model generates 32 proofs. If one of the proofs is correct, the theorem is considered correctly proved. For each theorem that is valid for correction, we perform an additional five rounds of correction. In the dataset, 18.31% of records are valid for correction. With the 2.54x inference speedup of dLLM compared to the AR models, the GPU hours for baseline and Diffusion-Proof are comparable.
H
Full Validation Loss results
The complete set of plots for validation analysis can be found in Figure 4.
I
Case Study Examples
I.1
Examples for corrector
The corrected theorem proof of mathd_algebra_215 is presented in Figure 9, and the wrong proof is in Figure 10. The corrector’s output of mathd_numbertheory_521 is in Figure 11 and the base proof with tactic failure is in Figure 12. I.2
Example for comparison with AR baseline
The example of imo_1983_p2 and mathd_algebra_188 are presented in Figure 13 and 14 respectively. I.3
Example for comparison with DeepSeek-Prover-V2
The success proof for imo_1962_p2 of DiffusionProof is presented in Figure 15. The DeepSeekProver-V2’s failed proof analysis is demonstrated
in Figure 16, and the example of a wrong proof for DS-Prover is in Figure 17.
Base Autoreg Loss Distribution
Base Diffusion Loss Distribution
4
4
4
2
2
2
2
0
0.25
Cumulative Probability
Loss
1.0
6 4
1.00
Loss
1.25
1.50
0.5
0.4 0.2
1.0
1.0
1.5
iff
0.0
2.0
uto
Loss
1.0
Tra i
Tra i
ne
ne
dD
dA
on
0.5
usi
on usi iff
se A Ba
0.8
0.5
Trained Autoreg Base Autoreg Base Diffusion Trained Diffusion
Base Models Comparison
Autoregressive Models Comparison 2.0
1.75
0.8 0.6 0.4
Trained Autoreg Loss
0.5
0.6
Violin Plot Comparison
2.00
Base Diffusion Loss
1.0
Loss
1.5
0.0
1.0
Trained Diffusion Loss
1.5
0.4
0.6
Trained Models Comparison Trained Autoreg Base Autoreg Base Diffusion Trained Diffusion
2.0
Loss
uto
uto dA ne Tra i
Loss per Sample - All Models
se D
2.0
Ba
1.5
Loss
reg
1.0
reg
0.5
0.2
0.8
0.0
0.0 0.0
0
2.00
2.0
2 0
1.75
Cumulative Distribution Function (CDF)
1.5
8
0.75
1.0
2.0
10
0.50
on
2.00
usi
1.75
iff
1.50
dD
Loss
1.25
Box Plot Comparison Trained Autoreg Base Autoreg Base Diffusion Trained Diffusion
12
1.00
ne
All Models - Overlapped Distribution 14
0.75
on
0.50
Tra i
0.25
usi
0
1.0
reg
0.8
uto
Loss
0.6
se A
0.4
6
reg
0.2
8
4
Loss
0
Frequency
6
iff
6
10
8
se D
8
Frequency
6
Frequency
8
Mean: 0.4088
12
10
10
Frequency
Frequency
12
12
10
14
Mean: 0.7421
14 12
Trained Diffusion Loss Distribution
Mean: 0.7456
Ba
14
Mean: 0.4197
Ba
Trained Autoreg Loss Distribution
1.50 1.25 1.00 0.75 0.50
0.2
1.5
1.0
0.5
0.25 0.0
0.0 0
25
50
75
100
Sample Index
125
150
175
0.2
0.4
0.6
Trained Autoreg Loss
0.8
1.0
0.25
0.50
0.75
1.00
1.25
Base Autoreg Loss
1.50
1.75
2.00
0.0
0.5
1.0
Base Autoreg Loss
1.5
2.0
Figure 4: Full set of plots for validation loss analysis, including detailed distribution for each model, detailed distribution analysis, and correlation study for models.
================MODEL INPUT================ <|im_start|>Complete the following Lean 4 code with explanatory comments preceding each line of code: ```lean4 import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem lean_workbook_plus_79832 (x : R) (h0 : 5 + 3.5 * x = 2.5 * x - 25) : x = -30 := ================TRAINED OUTPUT================ by /To solve the equation \(5 + 3.5x = 2.5x - 25\) for \(x\), we proceed as follows: 1. Rewrite the equation to isolate terms involving \(x\) on one side and constant terms on the other side. 2. Simplify the equation by eliminating the decimals and combining like terms. 3. Solve for \(x\) by isolating it on one side of the equation. -/ -- Rewrite the equation to have the terms involving x on one side and constants on the other side. rw [eq_comm] at h0 -- Normalize the equation by simplifying and combining like terms. ring_nf at h0 ⊢ -- Use linear arithmetic to solve for x. linarith ``` <|im_end|>
Figure 5: Input & output example for SFT data of dLLM-Prover
================MODEL INPUT================ <|im_start|>Complete the following Lean 4 code with explanatory comments preceding each line of code: ```lean4 import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem amc12a_2007_p18 (n : N) (hn : n ̸= 0) (h' : n ̸= 1) (x : N → R) (h0 : ∀ m, x m = Real.sqrt (n ^ (m + 2)) ) : Real.sqrt (1 + 4 * Real.sqrt n) ≤ n * (2 + x n) ^ (n + 1):= by ================TRAINED OUTPUT================ === Diffusion Block Begins have h1 : (n : R) ≥ 2 := by norm_cast omega have h2 : Real.sqrt n ≥ 1 := by apply Real.le_sqrt_of_sq_le nlinarith have h3 : (2 + x n : R) ≥ 3 := by have h4 : (x n : R) = Real.sqrt (n ^ (n + 2)) := by simpa [h0 ] using rfl have h5 : Real.sqrt (n ^ (n + 2)) ≥ 1 := by apply Real.le_sqrt_of_sq_le have h6 : (n : R) ^ (n + 2) ≥ 1 := by apply one_le_pow_of_one_le nlinarith nlinarith nlinarith<|fim_middle|><|fim_middle|><|fim_middle|>(in total 138 placeholder tokens)... have h4 : Real.sqrt (1 + 4 * Real.sqrt n) ≤ (n : R) * (2 + x n) ^ (n + 1) := by apply Real.sqrt_le_iff.mpr constructor · positivity · have h5 : (n : R) * (2 + x n) ^ (n + 1) ≥ (n : R) * 3 ^ (n + 1) := by gcongr <;> nlinarith have h6 : (n : R) * 3 ^ (n + 1) ≥ n * 3 ^ 2 := by apply mul_le_mul_of_nonneg_left · exact pow_le_pow_right (by linarith) (by omega) · nlinarith have h7 : === Diffusion Block Ends (n : R) * 3 ^ 2 ≥ 9 := by nlinarith nlinarith [sq_sqrt (show 0 ≤ (n : R) from by positivity), sq_sqrt (show 0 ≤ (n : R) from by positivity), Real.sqrt_nonneg (n : R), Real.sqrt_nonneg (n : R)] exact h4 <;> norm_num <;> omega ``` <|im_end|>
Figure 6: Input & output example for training data of dLLM-Corrector with diffusion block annotation
Complete the following Lean 4 code with explanatory comments preceding each line of code: ```lean4 import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem mathd_algebra_215 (S : Finset R) (h P0 : ∀ (x : R), x ∈ S ↔ (x + 3)^2 = 121) : k in S, k = -6 := by /Given the set \( S \) defined by the equation \((x+3)^2 = 121\), we need to show that the sum of all elements in \( S \) ,→ equals \(-6\). 1. **Identify the elements of \( S \)**: - The equation \((x+3)^2 = 121\) implies \( x^2 + 6x + 9 = 121 \). - Simplifying this equation, we get \( x^2 + 6x + 9 = 121 \), which simplifies to \( x^2 + 6x - 112 = 0 \). - Solving the quadratic equation \( x^2 + 6x - 112 = 0 \), we find the roots using the quadratic formula \( x = ,→ \frac{-b \pm \sqrt{b^2 - 4ac}}{2a} \): \[ x = \frac{-6 \pm \sqrt{36 + 448}}{2} = \frac{-6 \pm \sqrt{484}}{2} = \frac{-6 \pm 22}{2} \] - This gives us two solutions: \[ x = \frac{16}{2} = 8 \quad \text{and} \quad x = \frac{-28}{2} = -14 \] - Therefore, the elements of \( S \) are \( 8 \) and \( -14 \). 2. **Sum the elements of \( S \)**: - The sum of the elements \( 8 \) and \( -14 \) is \( 8 + (-14) = -6 \). Thus, the sum of all elements in \( S \) is indeed \(-6\). -/ -- We need P to show that the sum of all elements in S equals -6. have h1 : k in S, k = -6 := by <|MASK|><|MASK|><|MASK|><|MASK|><|MASK|><|MASK|>(in total 256 generation mask)... exact h1 ```<|im_end|>
Figure 7: Input example for dLLM-Corrector
Complete the following Lean 4 code with explanatory comments preceding each line of code: ```lean4 import Mathlib import Aesop set_option maxHeartbeats 0 open BigOperators Real Nat Topology Rat theorem mathd_algebra_215 (S : Finset R) (h P0 : ∀ (x : R), x ∈ S ↔ (x + 3)^2 = 121) : k in S, k = -6 := by /Given the set \( S \) defined by the equation \((x+3)^2 = 121\), we need to show that the sum of all elements in \( S \) ,→ equals \(-6\). 1. **Identify the elements of \( S \)**: - The equation \((x+3)^2 = 121\) implies \( x^2 + 6x + 9 = 121 \). - Simplifying this equation, we get \( x^2 + 6x + 9 = 121 \), which simplifies to \( x^2 + 6x - 112 = 0 \). - Solving the quadratic equation \( x^2 + 6x - 112 = 0 \), we find the roots using the quadratic formula \( x = ,→ \frac{-b \pm \sqrt{b^2 - 4ac}}{2a} \): \[ x = \frac{-6 \pm \sqrt{36 + 448}}{2} = \frac{-6 \pm \sqrt{484}}{2} = \frac{-6 \pm 22}{2} \] - This gives us two solutions: \[ x = \frac{16}{2} = 8 \quad \text{and} \quad x = \frac{-28}{2} = -14 \] - Therefore, the elements of \( S \) are \( 8 \) and \( -14 \). 2. **Sum the elements of \( S \)**: - The sum of the elements \( 8 \) and \( -14 \) is \( 8 + (-14) = -6 \). Thus, the sum of all elements in \( S \) is indeed \(-6\). -/ -- We need P to show that the sum of all elements in S equals -6. have h1 : k in S, k = -6 := by -- Identify the elements of S using the given equation. have h2 : S = {8, -14} := by ext x simp [h0 , Set.mem_insert_iff, Set.mem_singleton_iff] constructor · intro h have h2 := h0 x have h3 : x + 3 = 11 ∨ x + 3 = -11 := by apply eq_or_eq_neg_of_sq_eq_sq linarith cases' h3 with h3 h3 · exact Or.inl (by linarith) · exact Or.inr (by linarith) · intro h cases' h with h h · rw [h] norm_num · rw [h] norm_num -- Sum the elements of S. rw [h2 ] norm_num -- The final result is -6<|fim_middle|><|fim_middle|><|fim_middle|>(53 place holder tokens generated in total)... exact h1 ```<|im_end|>
Figure 8: Output example for dLLM-Corrector
theorem mathd_algebra_215 (S : Finset R) (h0 : ∀ (x : R), x ∈ S ↔ (x + 3)^2 = 121) : Σ k in S, k = -6 := by /Given the set \( S \) of all real numbers \( x \) such that \( (x + 3)^2 = 121 \), we need to show that the sum of all elements in \( S \) equals \(-6\). 1. **Identify the elements of \( S \)**: - The equation \( (x + 3)^2 = 121 \) implies \( x + 3 = \pm 11 \). - Therefore, \( x + 3 = 11 \) or \( x + 3 = -11 \). - Solving these equations, we get \( x = 8 \) or \( x = -14 \). 2. **Sum the elements of \( S \)**: - The elements of \( S \) are \( 8 \) and \( -14 \). - The sum of these elements is \( 8 + (-14) = -6 \). -/ -- We need to show that the sum of all elements in set S is -6. have h1 : S = {8, -14} := by -- Identifyify the elements of S. ext x simp [h0 , Set.mem_insert_iff, Set.mem_singleton_iff] constructor · intro h have h2 := h0 x have h3 : x + 3 = 11 ∨ x + 3 = -11 := by apply eq_or_eq_neg_of_sq_eq_sq linarith cases' h3 with h3 h3 · exact Or.inl (by linarith) · exact Or.inr (by linarith) · intro h cases' h with h h · rw [h] norm_num · rw [h] norm_num -- Substitute the known elements of S into the sum. rw [h1 ] -- Calculate the sum of 8 and -14. norm_num
Figure 9: Example of corrector successfully corrected proof for mathd_algebra_215
theorem mathd_algebra_215_failed (S : Finset R) (h0 : ∀ (x : R), x ∈ S ↔ (x + 3)^2 = 121) : Σ k in S, k = -6 := by /Same as above, omitted . . . -/ -- We know that the elements of S are 8 and -14. have h1 : S = {8, -14} := by ext x simp only [h0 , Set.mem_insert_iff, Set.mem_singleton_iff, sq] constructor · intro h have h1 : x + 3 = 11 ∨ x + 3 = -11 := by apply or_iff_not_imp_left.mpr intro h1 apply mul_left_cancel0 (sub_ne_zero_of_ne h1 ) nlinarith cases' h1 with h1 h1 -- Error Tactic · left linarith · right linarith · intro h cases' h with h h h · rw [h] norm_num · rw [h] norm_num -- Substitute the set S with {8, -14} and calculate the sum. rw [h1 ] -- The sum of {8, -14} is 8 + (-14) = -6. norm_num
Figure 10: The problem of mathd_algebra_215 for corrector
theorem mathd_numbertheory_521 (m n : N) (h0 : Even m) (h1 : Even n) (h2 : m - n = 2) (h3 : m * n = 288) : m = 18 := by /Given two integers \( m \) and \( n \) such that \( m - n = 2 \) and \( m \times n = 288 \), we need to show that \( m = 18 \). 1. From \( m - n = 2 \), we can express \( m \) as \( m = n + 2 \). 2. Substitute \( m = n + 2 \) into \( m \times n = 288 \): \[ (n + 2) \times n = 288 \] 3. Simplify the equation: \[ n^2 + 2n = 288 \] 4. Rearrange the equation to form a standard quadratic equation: \[ n^2 + 2n - 288 = 0 \] 5. Solve the quadratic equation using the quadratic formula \( n = \frac{-b \pm \sqrt{b^2 4ac}}{2a} \), where \( a = 1 \), \( b = 2 \), and \( c = -288 \): \[ n = \frac{-2 \pm \sqrt{2^2 - 4 \cdot 1 \cdot (-288)}}{2 \cdot 1} = \frac{-2 \pm \sqrt{4 + 1152}}{2} = \frac{-2 \pm \sqrt{1156}}{2} = \frac{-2 \pm 34}{2} \] 6. This gives two solutions: \[ n = \frac{32}{2} = 16 \quad \text{and} \quad n = \frac{-36}{2} = -18 \] 7. Since \( n \) must be positive integer, we select \( n = 16 \). 8. Substitute \( n = 16 \) back into \( m = n + 2 \): \[ m = 16 + 2 = 18 \] Thus, we have shown that \( m = 18 \). -/ -- From m - n = 2, express m in terms of n have h4 : m = n + 2 := by omega rw [h4 ] at h3 -- Simplify the equation to form a quadratic equation in n have h5 : n = 16 := by -- Solve the quadratic equation n^2 + 2n - 288 = 0 nlinarith -- Substitute n = 16 back into m = n + 2 have h6 : m = 18 := by omega exact h6
Figure 11: Example of corrector successfully corrected proof for mathd_numbertheory_521
theorem mathd_numbertheory_521_failed (m n : N) (h0 : Even m) (h1 : Even n) (h2 : m - n = 2) (h3 : m * n = 288) : m = 18 := by /Same as above, omitted . . . -/ -- From m - n = 2, express m in terms of n have h4 : m = n + 2 := by linarith -- Error Tactic -- Substitute m = n + 2 into m * n = 288 rw [h4 ] at h3 -- Simplify the equation to form a quadratic equation in n have h5 : n = 16 := by -- Solve the quadratic equation n^2 + 2n - 288 = 0 nlinarith -- Substitute n = 16 back into m = n + 2 have h6 : m = 18 := by rw [h5 ] -- Error Tactic linarith -- Conclude the proof by stating the final result exact h6
Figure 12: The problem of mathd_numbertheory_521 for corrector
theorem imo_1983_p6 (a b c : R) (h0 : 0 < a ∧ 0 < b ∧ 0 < c) (h1 : c < a + b) (h2 : b < a + c) (h3 : a < b + c) : 0 ≤ a^2 * b * (a - b) + b^2 * c * (b - c) + c^2 * a * (c - a) := by /To prove that the expression \( a^2 b(a - b) + b^2 c(b - c) + c^2 a(c - a) \) is non-negative, we start by analyzing the given conditions and the expression itself. The conditions are: 1. \( 0 < a \), \( 0 < b \), \( 0 < c \) 2. \( c < a + b \) 3. \( b < a + c \) 4. \( a < b + c \) We need to show that the expression \( a^2 b(a - b) + b^2 c(b - c) + c^2 a(c - a) \) is non-negative. This can be achieved by considering the non-negativity of the terms and the constraints on the variables. -/ -- We need to prove that the expression is non-negative. -- Given the constraints on the variables, we can use the non-negativity of the terms to bound the expression. nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_nonneg (sub_nonneg.mpr h1 .le) (sub_nonneg.mpr h2 .le), mul_nonneg (sub_nonneg.mpr h2 .le) (sub_nonneg.mpr h3 .le), mul_nonneg (sub_nonneg.mpr h3 .le) (sub_nonneg.mpr h1 .le)] theorem imo_1983_p6_failed (a b c : R) (h0 : 0 < a ∧ 0 < b ∧ 0 < c) (h1 : c < a + b) (h2 : b < a + c) (h3 : a < b + c) : 0 ≤ a^2 * b * (a - b) + b^2 * c * (b - c) + c^2 * a * (c - a) := by /Given a triangle \(ABC\) with \(AB = a\), \(BC = b\), and \(CA = c\) where \(a, b, c > 0\), and the conditions \(c < a + b\), \(b < a + c\), \(a < b + c\), we need to prove that: \[a^2 b (a - b) + b^2 c (b - c) + c^2 a (c - a) \geq 0\] To prove this, we use the fact that each term in the expression is a product of squares and differences. Since the squares of real numbers are non-negative, and the differences are also non-negative due to the given inequalities, the entire expression is non-negative. -/ -- Use the non-negativity of squares to prove the inequality. nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_nonneg h0 .1.le h0 .2.1.le, mul_nonneg h0 .2.1.le h0 .2.2.le, mul_nonneg h0 .2.2.le h0 .1.le, mul_nonneg (sq_nonneg (a - b)) h0 .2.1.le, mul_nonneg (sq_nonneg (b - c)) h0 .2.2.le, mul_nonneg (sq_nonneg (c - a)) h0 .1.le, mul_nonneg (sq_nonneg (a - b)) h0 .1.le, mul_nonneg (sq_nonneg (b - c)) h0 .2.1.le, mul_nonneg (sq_nonneg (c - a)) h0 .2.2.le]
Figure 13: imo_1983_p6 proved by Diffusion-Proof while the baseline fails
theorem mathd_algebra_188 (σ : Equiv R R) (h : σ.1 2 = σ.2 2) : σ.1 (σ.1 2) = 2 := by /Given an equivalence \( \sigma \) on the real numbers such that \( \sigma(2) = \sigma(2) \), we need to show that \( \sigma(\sigma(2)) = 2 \). 1. Start with the given condition \( \sigma(2) = \sigma(2) \). 2. Apply \( \sigma \) to both sides of the equation \( \sigma(2) = \sigma(2) \) to get \( \sigma(\sigma(2)) = \sigma(\sigma(2)) \). 3. Since \( \sigma(2) = \sigma(2) \), it follows that \( \sigma(\sigma(2)) = 2 \). -/ -- Start with the given condition σ(2) = σ(2) have h1 : σ.1 2 = σ.2 2 := h -- Apply σ to both sides of the equation σ(2) = σ(2) to get σ(σ(2)) = σ(σ(2)) have h2 : σ.1 (σ.1 2) = σ.1 (σ.2 2) := by simp_all -- Since σ(2) = σ(2), it follows that σ(σ(2)) = 2 have h3 : σ.1 (σ.1 2) = 2 := by simp_all -- The final result is σ(σ(2)) = 2 exact h3 theorem mathd_algebra_188_failed (σ : Equiv R R) (h : σ.1 2 = σ.2 2) : σ.1 (σ.1 2) = 2 := by /Given an equivalence \(\sigma\) between the real numbers, we need to show that if \(\sigma(1) = 2\), then \(\sigma(\sigma(1)) = 2\). By the definition of an equivalence, there exists a function \(\sigma\) such that \(\sigma(1) = 2\) and \(\sigma(\sigma(1)) = 2\). We can use these properties to derive the desired equality. -/ -- Using the symmetry property of the equivalence, we know that σ(2) = σ(1). have h1 := σ.symm_apply_left 2 have h2 := σ.symm_apply_right 2 -- Simplifying the expressions using the given values and the properties of the equivalence. simp_all [Equiv.eq_symm_apply_left]
Figure 14: mathd_algebra_188 proved by Diffusion-Proof while the baseline fails
theorem imo_1962_p2 (x : R) (h0 : 0 ≤ 3 - x) (h1 : 0 ≤ x + 1) (h2 : 1 / 2 < Real.sqrt (3 - x) - Real.sqrt (x + 1)) : -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by /We need to prove that for a real number \( x \) such that \( 0 \leq 3 - x \) and \( 0 \leq x + 1 \), the inequality \( \frac{1}{2} < \sqrt{3 - x} - \sqrt{x + 1} \) holds if and only if \( -1 \leq x < 1 - \frac{\sqrt{31}}{8} \). 1. **Establish the range of \( x \)**: - We need to show that \( -1 \leq x < 1 - \frac{\sqrt{31}}{8} \). 2. **Use the properties of the square root function: - We use the properties of the square root function to derive the inequalities. 3. **Verify the inequalities**: - We verify that the inequalities hold under the given conditions. -/ have h_main : -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by constructor · -- Show that -1 ≤ x have h3 : 0 ≤ Real.sqrt (3 - x) := Real.sqrt_nonneg (3 - x) have h4 : 0 ≤ Real.sqrt (x + 1) := Real.sqrt_nonneg (x + 1) have h5 : 0 ≤ Real.sqrt 31 := Real.sqrt_nonneg 31 have h6 : 0 ≤ Real.sqrt (3 - x) * Real.sqrt (x + 1) := by positivity have h7 : 0 ≤ Real.sqrt 31 * Real.sqrt (3 - x) := by positivity have h8 : 0 ≤ Real.sqrt 31 * Real.sqrt (x + 1) := by positivity have h9 : 0 ≤ Real.sqrt 31 * Real.sqrt (3 - x) * Real.sqrt (x + 1) := by positivity nlinarith [sq_sqrt (show 0 ≤ 3 - x by linarith), sq_sqrt (show 0 ≤ x + 1 by linarith), sq_sqrt (show 0 ≤ 31 by linarith), h2 ] · -- Show that x < 1 - Real.sqrt 31 / 8 have h3 : 0 ≤ Real.sqrt (3 - x) := Real.sqrt_nonneg (3 - x) have h4 : 0 ≤ Real.sqrt (x + 1) := Real.sqrt_nonneg (x + 1) have h5 : 0 ≤ Real.sqrt 31 := Real.sqrt_nonneg 31 have h6 : 0 ≤ Real.sqrt (3 - x) * Real.sqrt (x + 1) := by positivity have h7 : 0 ≤ Real.sqrt 31 * Real.sqrt (3 - x) := by positivity have h8 : 0 ≤ Real.sqrt 31 * Real.sqrt (x + 1) := by positivity have h9 : 0 ≤ Real.sqrt 31 * Real.sqrt (3 - x) * Real.sqrt (x + 1) := by positivity nlinarith [sq_sqrt (show 0 ≤ 3 - x by linarith), sq_sqrt (show 0 ≤ x + 1 by linarith), sq_sqrt (show 0 ≤ 31 by linarith), h2 ] exact h_main
Figure 15: Correct proof of imo_1962_p2 by Diffusion-Proof
### Detailed Proof and Analysis #### Problem Analysis We are given a real number \( x \) with the following constraints: 1. \( 0 \leq 3 - x \) (i.e., \( x \leq 3 \)), 2. \( 0 \leq x + 1 \) (i.e., \( x \geq -1 \)), 3. \( \frac{1}{2} < \sqrt{3 - x} - \sqrt{x + 1} \). We need to prove that: 1. \( -1 \leq x \), 2. \( x < 1 - \frac{\sqrt{31}}{8} \). First, observe that the inequality \( \frac{1}{2} < \sqrt{3 - x} - \sqrt{x + 1} \) is only possible when \( x + 1 \leq 3 x \), i.e., \( x \leq 1 \). This is because: - If \( x > 1 \), then \( \sqrt{3 - x} \) is real only when \( x \leq 3 \), and \( \sqrt{x + 1} \) is real only when \( x ,→ \geq -1 \). However, \( \sqrt{3 - x} - \sqrt{x + 1} \) would be negative for \( x > 1 \), because \( \sqrt{3 - x} < ,→ \sqrt{x + 1} \) (since \( 3 - x < x + 1 \), i.e., \( x > 1 \)).
,→
But we must ensure \( x \leq 3 \) (which is already given) and \( x \geq -1 \) (which is also given). So \( x \) is in \( [-1, 3] \).
,→
#### Step 1: Establish \( x \leq 1 \) Assume for contradiction that \( x > 1 \). Then: 1. \( \sqrt{3 - x} < \sqrt{x + 1} \) (since \( 3 - x < x + 1 \) because \( x > 1 \)), 2. Therefore, \( \sqrt{3 - x} - \sqrt{x + 1} < 0 \), 3. But \( \frac{1}{2} > 0 \), so \( \frac{1}{2} < \sqrt{3 - x} - \sqrt{x + 1} \) would imply \( \sqrt{3 - x} - \sqrt{x + 1} ,→ > \frac{1}{2} \), which is false because \( \sqrt{3 - x} - \sqrt{x + 1} < 0 \). Hence, \( x \leq 1 \). But in Lean, we do not have \( x > 1 \) as a direct assumption. Instead, we use the contrapositive: if \( x > 1 \), then \( \sqrt{3 - x} - \sqrt{x + 1} \leq 0 \), which is \( \sqrt{3 - x} - \sqrt{x + 1} \leq \frac{1}{2} \), contradicting the hypothesis.
,→ ,→
#### Step 2: Prove \( -1 \leq x \) This is already given as \( h1 \). #### Step 3: Prove \( x < 1 - \frac{\sqrt{31}}{8} \) Omitted for simplicity... #### Correct Approach Omitted for simplicity... #### Better Approach Omitted for simplicity... #### Final Simplification Omitted for simplicity... #### Revised Plan Omitted for simplicity... #### Correct Solution Omitted for simplicity... #### Conclusion The problem reduces to verifying that \( x < 1 - \frac{\sqrt{31}}{8} \) is the correct upper bound, which is tedious but ,→ straightforward. ### Step-by-Step Abstract Plan 1. **Establish \( x \leq 1 \)**: - Assume for contradiction \( x > 1 \). Then \( \sqrt{3 - x} < \sqrt{x + 1} \), so \( \sqrt{3 - x} - \sqrt{x + 1} < 0 ,→ \), violating the hypothesis. Hence, \( x \leq 1 \). 2. **Prove \( x \geq -1 \)**: - This is given by \( h1 \). 3. **Prove \( x < 1 - \frac{\sqrt{31}}{8} \)**: - Square both sides of \( \sqrt{3 - x} - \sqrt{x + 1} > \frac{1}{2} \) to find bounds on \( x \), using the fact that ,→ \( x \leq 1 \) and \( x \geq -1 \). ### Lean 4 Proof Sketch with `have` ```lean4 theorem imo_1962_p2 (x : R) (h0 : 0 ≤ 3 - x) (h1 : 0 ≤ x + 1) (h2 : 1 / 2 < Real.sqrt (3 - x) - Real.sqrt (x + 1)) : -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by have h_main_goal : -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by sorry sorry ``` ### Explanation The `have` statement directly encodes the main goal of the proof, which is to prove `-1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8`. ,→ The actual proof of this statement is marked as `sorry` and would require detailed calculations based on the ,→ inequalities and bounds derived in the proof sketch.
Figure 16: Analysis process for DS-Prover-V2 in proving imo_1962_p2
theorem imo_1962_p2_failed (x : R) (h0 : 0 ≤ 3 - x) (h1 : 0 ≤ x + 1) (h2 : 1 / 2 < Real.sqrt (3 - x) - Real.sqrt (x + 1)) : -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by have h_main : -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by constructor · -- Prove -1 ≤ x linarith [h1 ] · -- Prove x < 1 - Real.sqrt 31 / 8 have h3 : x < 1 - Real.sqrt 31 / 8 := by by_contra! h have h4 : x ≥ 1 - Real.sqrt 31 / 8 := by linarith have h5 : Real.sqrt (3 - x) - Real.sqrt (x + 1) ≤ 1 / 4 := by have h6 : x ≥ 1 - Real.sqrt 31 / 8 := by linarith have h7 : Real.sqrt (3 - x) - Real.sqrt (x + 1) ≤ 1 / 4 := by have h8 : 0 ≤ Real.sqrt (3 - x) := by apply Real.sqrt_nonneg have h9 : 0 ≤ Real.sqrt (x + 1) := by apply Real.sqrt_nonneg have h10 : Real.sqrt (3 - x) ≥ 0 := Real.sqrt_nonneg (3 - x) have h11 : Real.sqrt (x + 1) ≥ 0 := Real.sqrt_nonneg (x + 1) have h12 : Real.sqrt (3 - x) * Real.sqrt (x + 1) ≥ 0 := by positivity have h13 : Real.sqrt (3 - x) * Real.sqrt (x + 1) ≥ 0 := by positivity have h14 : (Real.sqrt (3 - x) - Real.sqrt (x + 1)) ^ 2 ≤ (1 / 4) ^ 2 := by have h15 : x ≥ 1 - Real.sqrt 31 / 8 := by linarith have h16 : Real.sqrt 31 ≥ 0 := Real.sqrt_nonneg _ have h17 : Real.sqrt 31 ^ 2 = 31 := Real.sq_sqrt (by positivity) have h18 : x + 1 ≥ 2 - Real.sqrt 31 / 8 := by linarith have h19 : 3 - x ≥ 3 - (1 - Real.sqrt 31 / 8) := by linarith -- Error occurs here have h20 : 3 - x ≥ 2 + Real.sqrt 31 / 8 := by linarith nlinarith [Real.sq_sqrt (show 0 ≤ 3 - x by linarith), Real.sq_sqrt (show 0 ≤ x + 1 by linarith), Real.sqrt_nonneg 31, sq_nonneg (Real.sqrt (3 - x) - Real.sqrt (x + 1)), sq_nonneg (Real.sqrt (3 - x) + Real.sqrt (x + 1) - 5 / 2), sq_nonneg (Real.sqrt (3 - x) - Real.sqrt (x + 1) - 1 / 4)] nlinarith [Real.sqrt_nonneg (3 - x), Real.sqrt_nonneg (x + 1), Real.sq_sqrt (show 0 ≤ 3 - x by linarith), Real.sq_sqrt (show 0 ≤ x + 1 by linarith)] exact h7 linarith exact h3 exact h_main
Figure 17: Failed proof of imo_1962_p2 by DeepSeek-Prover-V2