1 Introduction↩︎

Automated theorem proving (ATP) has long been a central goal in the field of artificial intelligence, serving as a key benchmark for evaluating machine reasoning. Recent progress in Large Language Models (LLMs) has greatly changed the field of ATP. Most previous research has attempted to solve this problem by combining LLMs with formal proof engines like Lean, Coq, and Isabelle [1]–[3] or by using specialized languages [4]. In contrast, informal theorem proving aims to generate proofs using natural language and standard mathematical notation, often formatted in LaTeX. This setting aligns well with the strengths of modern LLMs.

However, only a limited number of studies have investigated informal theorem proving, including [4] and [5], and the area remains highly underexplored. Most existing research has focused on framework construction, while paying little attention to the proof generation mechanism and the key bottlenecks of LLM-based informal theorem proving. Additional related work will be discussed in Appendix 8.

Inspired by how human experts prove theorems, we argue that informal theorem proving would require first forming a big-picture view of the proof before eventually completing the full proof. We refer to this early-stage, high-level cognitive act of identifying a set of pivotal ideas or essential technical tools as insight. Such pivotal ideas or technical tools identified in this process are termed core techniques, typically involving the substantive theoretical machinery, e.g., a specific lemma, theorem, or corollary, rather than merely the elementary routine logical steps. In this paper, we emphasize the importance of insight and core techniques in informal mathematical proofs. Specifically, we identify that the primary bottleneck in proof generation resides in the recognition of these core techniques. We further demonstrate that to improve a model’s mathematical reasoning ability, it is feasible and effective to adopt a principled two-phase procedure: (1) extract core techniques by reviewing the proof from a training corpus (the acquisition phase); (2) develop insightful reasoning for a specific problem by identifying the underlying core techniques and then constructing proofs based on them during inference (the application phase).

Empirically, to achieve this, we propose DeepInsight, a unified training framework that integrates data construction, progressive SFT, and reinforcement learning. Our work first introduces DeepInsightTheorem, a newly constructed hierarchical dataset that substantially extends the prior DeepTheorem framework [5], with the extraction of core techniques. We then propose a novel progressive multi-stage training strategy, which is carefully designed to emulate key aspects of the human learning process, thereby training LLM for insightful reasoning. Finally, we introduce sec:InsightPO, a policy optimization algorithm that uses this hierarchical structure to provide rewards for core technique identification, proof sketching, and proof completion.

Through extensive experiments, we demonstrate that this insight-aware method significantly outperforms standard baselines. These results confirm that explicitly training the model to acquire proof insight by extracting core techniques enables it to move beyond mere text imitation toward more faithful, insight-driven mathematical reasoning. The primary contributions of our work are summarized as follows:

• We identify core technique recognition as a key bottleneck in informal theorem proving and formalize it through the notion of mathematical insight.

• We construct DeepInsightTheorem, a hierarchical dataset with core-technique, proof-sketch, and the full proof to facilitate model post-training for informal theorem proving.

• We propose a novel training pipeline, DeepInsight, tailored to the hierarchical structure of DeepInsightTheorem, consisting of a progressive multi-stage SFT and sec:InsightPO, a new policy optimization method with structured verifier rewards capturing insight correctness.

• We evaluate our framework on challenging benchmarks and against strong baselines for mathematical reasoning, and observe clear and consistent improvements over prior methods.

2 Preliminary↩︎

We consider the context of informal mathematical proof generation. Let \(\mathcal{V}\) be the vocabulary, which is a finite discrete set. The text sequence space \(\mathcal{S}\) is defined as the union of the product spaces of any finite power \(\mathcal{S} \triangleq \bigcup_{l=0}^{\infty} \mathcal{V}^l.\)

We can then denote the space of theorems as a subspace \(\mathcal{Q}\) of \(\mathcal{S}\) which contains all well-defined math problems for theorem-proving. For any \(q\in \mathcal{Q}\), we denote the space of proofs with respect to \(q\) as \(\mathcal{P}(q) \subset \mathcal{S}\) that contains all valid proofs of \(q\).

The LLM \(M_{\theta}\) is an auto-regressive network which will predict the next token’s distribution over the vocabulary when it is working. To train a generation policy \(\pi_{\theta}\) to be a theorem-prover, the training datasets are collected from many resources of math corpus and commonly formed as theorem-proof pairs \((q, p)\). For Supervised Fine-Tuning (SFT) on such a dataset, the objective is to solve \(\max_\theta ~ \mathbb{E}_{q \sim \mathcal{D}, p\sim\mathcal{D}_{ P(q) } } \pi_\theta(p | q)\), where \(\mathcal{D}\) is the distribution of the math problems in the training set and \(\mathcal{D}_{ P(q) }\) is the distribution over the valid proofs of each question in the training set.

2.1 Notion of Insight↩︎

For a mathematical proof question, insight is a cognitive act of identifying a set of pivotal ideas (e.g., “apply the Pigeonhole Principle”, “utilize a specific invariant xxx” ) through the given conditions to capture the essence of the solution. We refer to such pivotal ideas as core techniques in this paper. Insight is not the proof itself, but instead refers to a preliminary, high-level perception and foresight of the core techniques required to construct the proof. Generally, we group these techniques into three main categories that cover the most common and essential technical patterns in math proofs:

• Construction: Introducing auxiliary objects, e.g., “Define the sequence \(x_{n+1} = U x_n\) for \(n \geq 0\). This Picard iteration constructs the sequence \(x_0, x_1 = U x_0, x_2 = U^2 x_0, \dots\)”.

• Theorem Call: Invoking a known lemma, theorem, or any existing result, e.g. “By using Cantor’s Theorem.”

• Mathematical Transformation: Performing a reformulation that recasts the problem in a new framework, e.g., “Define a topology \(\tau\) on the set of integers \(\mathbb{Z}\)..., shifting the language and tools entirely from number theory to topology.”

Formally, we denote the space of techniques as \(\mathcal{T} \subset \mathcal{S}\) that contains all possible techniques in those three classes. Generally, we can then write each proof \(p\) of \(q\) as an ordered sequence \[\label{p} p = (r_1, t_1, r_2, t_2, \cdots, r_k),\tag{1}\] where \(t_i \in \mathcal{T}\), \(r_i\) denote an elementary reasoning statement between successive techniques, and \(k\) is the total number of techniques in the proof.

3 Motivating Example: Insightfulness Evaluation of Off-the-Shelf LLMs↩︎

Expert mathematicians can often quickly form a big-picture view of a proof when facing a novel problem, drawing on insights cultivated through experience. In contrast, general-purpose LLMs often fail to reliably form such high-level ideas at the outset of proof generation, and are not as adept as experts at identifying the pivotal technique early.

We evaluated several powerful commercial LLMs with a non-thinking mode¹, including Gemini 2.5 Flash [6] and DeepSeek-R1 [7], by prompting them to provide insights for math competition problems randomly sampled from Putnam and FIMO datasets (See Appendix 15 for detailed prompts). We then use o3-mini to review and evaluate the insights generated by these models from the dimensions of depth and completeness (Appendix 10.1). Here, depth indicates the insight is specific and technically accurate, rather than a generic, high-level statement or a vague direction, while completeness measures whether all core techniques required for the solution are identified. Our results show that, in terms of depth, both models largely failed to provide specific and accurate insights, instead producing shallow guesses or vague hints at some directions. In terms of completeness, they always see just one or two low-hanging ideas while missing more central techniques.

4 Methodology↩︎

4.1 Challenge of Identifying Core Techniques↩︎

The main body of a proof is largely composed of some basic, easy-to-learn mathematical reasoning statements. For a theorem-proving LLM denoted by \(\pi_{\text{TP}}\) generating the proof for a problem, the uncertainty remains low until a core technique needs to be recognized. This likely arises for two main reasons. First, core techniques are intrinsically harder to identify. Second, since basic reasoning steps constitute a large fraction of the proof, LLM training may overly emphasize these basic reasoning details rather than core technique recognition.

As illustrated in Figure 2, in the proof generated by Qwen2.5-14B-Instruct [8] for the well-known Baire Category Theorem in General Topology, tokens with spiking entropy consistently signal the presence of core techniques:

Construction: “Constructing a Sequence of ...” to construct a sequence of nested open sets.

Theorem call: “Using completeness...” to apply the completeness of the ground space.

Mathematical transformation: “Consider the closures...” to transfer the issue of open sets to their closures.

Note that the above three techniques are defined in Section 2.1. The rest of the proof is based on basic elementary reasoning statements that connect these core techniques, making the overall argument complete and smooth.

As discussed above, the model \(\pi_{\text{TP}}\) struggles to decide which core technique to apply, as evidenced by the token-level entropy spikes at positions where a core technique is introduced. To further formalize this, we assume \[\label{etp} \pi_{\text{TP}}(t_i |u_i, q) < \delta\tag{2}\] for some small constant \(\delta >0\) and any \(t_i \in \mathcal{T}\), where \(u_i := (r_1,t_1,\cdots,r_i)\) denotes the prefix before \(t_i\) and \(i\) indexes the \(i\)-th technique in a proof of form 1 . This reflects the difficulty or the high uncertainty of identifying correct techniques. Consequently, we have the probability of directly predicting a core technique \(t_i\) from the question \(q\) bounded by \(\delta\): \(\pi_{\text{TP}}(t_i | q) = \sum_{u_i} \pi_{\text{TP}}(t_i |u_i, q) \pi_{\text{TP}}(u_i | q) < \delta.\) Similarly, by recursively applying 2 , for the probability of generating a valid full proof \(p\) for \(q\) via \(\pi_{\text{TP}}\), we have \(\pi_{\text{TP}}(p|q) \leq \delta^k,\) where \(k\) is the total number of techniques appearing in the proof. This indicates that the ability to complete a proof is restricted by the uncertainty. A detailed derivation is in Appendix 9. We can interpret the value \(\pi_{\text{TP}}(t_i | q)\) as the insightfulness of \(\pi_{\text{TP}}\) in identifying technique \(t_i\in \mathcal{T}\). A higher value indicates stronger insight in recognizing \(t_i\) as the appropriate technique to apply.

Therefore, the successful realization of core techniques is crucial for generating valid proofs in theorem proving. Core techniques also serve as more appropriate memory anchors for key pattern recognition in complex mathematical reasoning. This prompts a necessity of enhanced learning to bridge the gap between the question and the core techniques required to solve it.

4.2 Insight Acquisition and Application↩︎

It is critical to figure out the core techniques for the proof of a specific question if we want an LLM to grasp the essence of such a proof. After identifying the relevant techniques, the remaining challenge is to integrate these core techniques into a coherent solution, which relies primarily on the fundamental mathematical reasoning capability.

This reflects a shift in the underlying reasoning pattern for an LLM. In human learning, when presented with a problem and its corresponding proof, beginners typically need to carefully study and review the entire solution to gradually identify and understand the core techniques involved. Subsequently, when faced with similar problems later, they will first form an initial idea about the core techniques and then use the intuition to construct the proof.

Our framework comprises the following two complementary cognitive processes, mirroring how humans consolidate and review learning materials:

• Acquisition phase: extract core techniques by reviewing proofs in a training corpus;

• Application phase: develop insightful reasoning by first predicting the core techniques and then generating proofs by applying these techniques.

We consider the following generation process for a proof \(p\) via a policy \(\pi_{\theta}\) parameterized by \(\theta\): \[\label{insight} \pi_{\theta}( t, p | q) = \pi_{\theta}(t | q)\pi_{\theta}(p | t, q),\tag{3}\] where \(t = (t_1 ,\cdots, t_k )\). In 3 , we first identify the required core techniques \(t\) via \(\pi_{\theta}(t | q)\) before generating the proof \(p\). The proof \(p\) is then generated conditioned on the identified techniques \(t\) via \(\pi_{\theta}(p | t, q)\). Consequently, the performance of \(\pi_{\theta}\) depends critically on how well the first factor \(\pi_{\theta}(t \mid q)\) is learned. In the following sections, we construct a well-curated dataset and propose a novel multi-stage method to optimize \(\theta\) such that both \(\pi_{\theta}(t \mid q)\) and \(\pi_{\theta}(p \mid t, q)\) are trained effectively, which corresponds to the acquisition phase. Subsequently, during the application phase, we apply 3 for proof generation.

Furthermore, we can consider a more refined generation process: \[\label{insight-sketch} \pi_{\theta}(t, s, p | q) = \pi_{\theta}(t | q) \pi_{\theta}(s | t, q) \pi_{\theta}(p | s, t, q),\tag{4}\] where \(s\) denotes a proof sketch generated conditioned on the identified core techniques \(t\). In this scenario, the proof \(p\) is generated conditioned on both the core techniques \(t\) and the sketch \(s\). This hierarchical decomposition will make the model first commit to a high-level thinking structure before generating a full proof, reflecting a natural human problem-solving process. Furthermore, we follow the dual phases of insight acquisition and application for effectively generating mathematical proofs. Next, we show how to instantiate these processes in practice via more concrete procedures.

5 Training an Insightful LLM↩︎

5.1 Dataset Construction↩︎

We construct a hierarchical dataset to train an insightful LLM that can explicitly identify and subsequently generate the core techniques to guide the proof of a given problem. We design the dataset to provide a supervision signal that mirrors human review and consolidation. To ensure high quality and sufficient difficulty, we build our data based on the DeepTheorem [5] dataset, a recently introduced, large-scale resource for informal mathematical theorem proving.

DeepTheorem [5] provides a robust foundation of 121K high-quality informal theorem-proof pairs at roughly IMO-level difficulty. It is constructed through a rigorous pipeline, including collection from diverse corpora and strict decontamination against major benchmarks (e.g., MATH [9], AIME [10], miniF2F [1]). Since DeepTheorem already covers many commonly used datasets for theorem-proving training and is built through a rigorous, high-quality construction pipeline, using it as the base dataset allows our subsequent hierarchical annotation to inherit these desirable properties, resulting in a curated dataset with strong overall quality. We refer readers to [5] for further details.

Since LLMs struggle to extract core techniques on their own (Section 4.1), we augment model training with a richer supervision signal by explicitly providing core techniques. Building upon DeepTheorem’s theorem-proof data pairs \((q,p)\), we perform additional annotations to transform each proof into a hierarchical representation as follows: \[\bigl( q,\; \underbrace{(t_1,\ldots,t_m)}_{\text{core techs}},\; \underbrace{\makebox[2.9em][c]{s}}_{\text{sketch}},\; \underbrace{\makebox[2.2em][c]{p}}_{\text{proof}} \bigr).\] This process involves a meticulous, LLM-assisted analysis to extract deep information from proof \(p\), following a dedicated prompt to design each component as follows:

• Core Techniques \(t_i\). Instead of only listing the core techniques, we first include a guiding statement as “Let’s analyze the conditions...”, then those core techniques are introduced with heuristic language, for example: “The condition ... tells us to construct an auxiliary function...” or “... suggests using xxx Theorem.”. The core techniques are themselves finally summarized at the end of this component according to those three main classes.

• Proof Sketch \(s\). We insert an intermediate component between the core techniques and the full proof. This sketch outlines a proof strategy based on the identified core techniques, bridging high-level insights and low-level derivations to encourage a smooth and coherent reasoning flow.

• Proof \(p\). The original, detailed proof from the base dataset serves as the ground-truth instantiation.

We refer to the resulting dataset as DeepInsight-Theorem, highlighting the insight-driven hierarchical structure derived from DeepTheorem. See the top of Figure 1 for an overview, and Figure 6 for a concrete example.

. A key design consideration in the construction of DeepInsightTheorem is to avoid presenting the core techniques as an isolated list. Instead, we frame insight generation with a short, analytical preamble that serves as a localized micro chain-of-thought for analyzing the question. This encourages a more accurate insight prediction than directly outputting a list of techniques.

There exists a subtle but crucial logical shift between acquisition and application phases, even though the two processes are basically similar. The former is backward-looking: “Analyzing this proof, we see that xxx is the core tech.”, while the latter is forward-looking: “Given these problem conditions, xxx might be a core tech.” These two processes by our design are integrated into our LLM-assisted data annotations. Therefore, we need to carefully tune the prompt for the LLM to ensure the smoothness of the transformation. The specific prompt shows how the two processes are integrated, as for each problem, this prompt on one hand encourages the LLM to analyze the corresponding proof through summarization and extract the core techniques as required, and on the other hand shifts perspective to play the role of an expert encountering the problem for the first time, integrating these core techniques into the thought process of analyzing the problem. The prompts used are detailed in Appendix 15.

. Our curated dataset contains approximately 100K problems. On average, each proof involves 3.6 core techniques, with more complex problems frequently combining four or more, as illustrated in Figure 3. A distribution of core technique counts is shown in Figure 10.

5.2 Progressive Multi-Stage SFT↩︎

The next step concerns applying the core techniques summarized above. Thanks to the hierarchical structure of DeepInsightTheorem, the model can already be trained to produce hierarchical outputs, generating a core technique analysis first (Section 5.1). Then the decompositions in 3 naturally suggest a two-phase training paradigm: the acquisition phase trains the LLM on the original theorem-proof pairs \((q,p)\), while the application phase continues training on the insight-induced data.

We empirically demonstrate the necessity of this two-phase design by comparing training solely on DeepInsightTheorem against the baseline. Results for Qwen2.5-7B and Llama3-8B are reported in Table 1. The comparison indicates that directly training on DeepInsightTheorem does not necessarily allow the LLM to benefit from the insight structure. One of the reasons is that a higher value of 3 assumes a training on theorem-proof data to enlarge \(\pi_{\theta}(p | q)\) and \(\pi_{\theta}(r_i | r^{\le i-1}, t, q)\) respectively. Without first training on theorem-proof pairs, the model may lack the basic mathematical reasoning and proof-writing competence required to exploit technique-level guidance. From a learning perspective, this can also be viewed as a mismatch with the natural progression of human learning: teaching a novice the expert’s high-level reasoning pattern before solidifying foundational proof-writing skills can create a substantial comprehension gap.

Inspired this analysis, we adopt a multi-stage training strategy for fine-tuning LLMs. Specifically, we propose a three-stage curriculum that progresses from direct proof generation to sketch-conditioned generation and finally technique-guided reasoning, which we refer to as Apprentice, Journeyman, and Expert. Below we outline the main stages of our progressive multi-stage SFT, each conducted on the same dataset but using different components of DeepInsightTheorem:

• Stage 1 (Apprentice): \((q, p)\). We first train the model on plain theorem-proof pairs to acquire basic proof-generation ability. This stage corresponds to a novice learner studying complete solutions.

• Stage 2 (Journeyman): \((q, s, p)\). We then train the model on theorem-sketch-proof triples, encouraging it to condition proof generation on a high-level sketch. This introduces an intermediate, coarse-to-fine abstraction and reflects a more advanced learner who can follow and internalize the step-wise logical structure rather than merely reproducing surface forms.

• Stage 3 (Expert): \((q, \{t_i\}, s, p)\). Finally, we train on the full hierarchical structure, so that the model learns to predict core techniques from the problem and leverage them to derive the sketch and the final proof. This stage explicitly learns a direct mapping from the question to its core techniques, resembling an expert’s technique-driven reasoning paradigm.

This multi-stage training strategy is illustrated in Figure 1 bottom. Overall, the progressive multi-stage design structurally decouples the learning objectives, yielding a clear and focused target for each training stage. Each stage’s training primarily emphasizes the mapping from the problem to the newly introduced component (e.g., \(p\), then \(s\), then \(\{t_i\}\)). Since each mapping is not yet adequately learned by the model, continued training does not cause overfitting.

5.3 Insight Policy Optimization↩︎

After the progressive multi-stage SFT, the model has learned to generate proofs in the hierarchical format of DeepInsightTheorem. We further propose sec:InsightPO, a GRPO-style reinforcement learning algorithm tailored to this framework. The key idea is to align reinforcement learning with our structured data format: instead of assigning only an outcome reward to the entire proof, the verifier evaluates whether the generated insights, proof sketch, and final proof form a coherent hierarchy, providing a hierarchy-aware reward that reflects both the quality of the identified insight and the validity of the resulting proof. This structured reward is then used in group-relative policy optimization, encouraging the model to improve not only final proof writing but also the intermediate insight and planning behavior that supports difficult theorem proving.

12pt

6 Experiments↩︎

In this section, we conduct experiments on two open-source model families: Qwen2.5 [8] and Llama3 [11]. For each family, we start from their respective base models.

6.1 Experiment Details↩︎

Standard SFT. For each base model, we establish a baseline by performing standard SFT on the question-proof pairs for 3 epochs.

Progressive Multi-Stage SFT. We implement two variants of our proposed progressive training strategy as follows:

• Full Three-Stage Training: This variant follows the complete curriculum described in Section 5.2. For a given base model, we first fine-tune it on the theorem-proof pairs for 3 epochs, then on the theorem-sketch-proof for another 3 epochs, and finally on the full hierarchical data for a final 3 epochs.

• Two-Stage Training: This is a streamlined variant where we skip the intermediate theorem-sketch-proof stage. The motivation for this design is that the core part of our hierarchical structure is the insight and the conceptual jump from generating a full proof to generating a proof sketch might be relatively small in terms of reasoning difficulty. Therefore, removing the proof sketch part may not affect training and could also help save some token cost.

sec:InsightPO Post-Training. Building on top of the three-stage SFT models, we conduct sec:InsightPO post-training as described in Section 5.3. We use DeepInsightTheorem as the training set and DeepSeek-R1 as the verifier. The verifier evaluates insight quality, logical validity, completeness, and clarity with weights of 30%, 30%, 25%, and 15%, respectively. For each dimension, the verifier outputs a score from \(\{0, 0.1, 0.2, \ldots, 1.0\}\); rather than using only the argmax score token, we extract the logits over the 11 score values, apply softmax normalization, and use the probability-weighted expected score \(\sum_{i=0}^{10} p_i(i/10)\) as the dimension score before computing the weighted total. We train for 400 steps with batch size 128, group size 16, and a maximum rollout length of 8192 tokens. Following prior work on group-relative policy optimization [7], we do not apply KL regularization. The full verifier prompt is provided in Appendix 15, and the test score dynamics during sec:InsightPO training are shown in Figure 8 in Appendix 10.

Evaluation Protocol. We evaluate generated proofs with an LLM-as-Judge protocol detailed in Appendix 11. The automatic evaluation scores final proofs along logical validity, completeness, and clarity, and aggregates judgments from DeepSeek-R1 and o3-mini to reduce single-judge bias. Since our training and evaluation both rely on LLM-based verification, we further conduct a stratified human audit as a calibration and sanity-check mechanism. Human reviewers inspect sampled outputs across model families, benchmarks, and score ranges, checking whether the proof realizes the intended insight and whether any essential derivation is missing.

Moreover, we compare our method with two groups of baselines. The first group contains several open-source models, many of which have been further enhanced via RL-based post-training; we compare them with our fine-tuned Qwen2.5-7B model. The second group contains three structural mathematical reasoning baselines, including SELF-DISCOVER, Least-to-Most Prompting, and Plan-and-Solve Prompting. These baselines are all trained on prompt-proof pairs \((q,p)\). More baseline settings are detailed in Appendix 10.2.

6.2 Main Results↩︎

Our framework achieves better performance. The main results are presented in Table 2 and Table 6. Table 2 shows the average scores from both DeepSeek-R1 and o3-mini, while Table 6 presents the scores from DeepSeek-R1. These results show that after training for insightful hierarchical reasoning, for both variants of our proposed progressive training strategy, the models of different sizes demonstrate superior performance to base models on all three benchmarks. This verifies that, via insightful reasoning, the model’s reasoning capability improves.

In addition, Figure 7 in Appendix 10 reports the best scores for each benchmark, which are pushed higher when incorporating insight, especially for smaller backbones such as the 1.5B model. This implies that insight-guided thinking can help break the reasoning ability ceiling for small models.

sec:InsightPO further boosts performance across all models. As shown in the “DeepInsight” rows in Table 6 and Table 2, sec:InsightPO post-training on top of the three-stage SFT models yields consistent and substantial improvements on all benchmarks. For the Qwen2.5-7B model, sec:InsightPO achieves an average score of 34.32, representing a relative improvement of 32.9% over the three-stage SFT baseline.

Our framework outperforms SOTA models. The comparison can be seen in Table 5 in Appendix 10.3. These results demonstrate that, after only SFT, our model already achieves performance that is competitive with those of SOTA models of the same size and extensive post-training, and notably outperforms them after sec:InsightPO training. For the details of evaluation, please see Appendix 11.

Comparisons with structured prompting baselines. The results further show that generic decomposition or planning improves over plain SFT but remains consistently below DeepInsight. This suggests that the main gain does not come only from asking the model to produce a plan at inference time, rather, it comes from explicitly learning theorem-specific insight hierarchies during training and then refining them with sec:InsightPO . Detailed settings and results are provided in Appendix 10.2.

7 Conclusion↩︎

In this paper, we propose DeepInsight, a complete training framework consisting of: (1) DeepInsightTheorem, a hierarchical dataset with explicitly extracted core techniques; (2) a progressive curriculum-style SFT strategy that trains LLMs for insightful reasoning; and (3) sec:InsightPO, a GRPO-style reinforcement learning algorithm with a probability-weighted LLM verifier and hierarchy-aware rewards. Comprehensive evaluations show consistent and substantial improvements over strong baselines on challenging benchmarks.

8 Related Work↩︎

8.0.0.1 Formal theorem proving.

Formal automated theorem proving (ATP) relies on proof assistants such as Lean, Coq, and Isabelle ([1] [[2] ][3]), where correctness is enforced by a strict formal system. Recent work integrates large language models with formal proof environments to combine natural-language generation with machine-checkable verification ([12], [13], [14], [15]). Representative benchmarks include miniF2F for cross-system olympiad-level evaluation [1], as well as more challenging datasets that target IMO-/Putnam-style mathematics [3], [16]. While formal approaches offer strong verifiability, they often face (i) a substantial gap between human mathematical exposition and formal languages, and (ii) a large proof search space that benefits from stronger decomposition, planning, and retrieval.

8.0.0.2 Informal theorem proving.

Informal theorem proving generates proofs directly in natural language and standard mathematical notation (e.g., LaTeX), which aligns well with typical LLM pretraining. NaturalProofs constructs natural-language theorem–proof corpora [4], and NaturalProver studies grounded proof generation in reference/retrieval settings [4]. Tencent’s DeepTheorem further advances IMO-level informal proving with large-scale data and reinforcement-learning-style training recipes [5]. [17] focuses specifically on inequality proofs. Despite this progress, many systems remain largely end-to-end and do not explicitly identify or control the core techniques that drive a proof.

8.0.0.3 Hierarchical Reasoning.

Hierarchical reasoning for LLMs decomposes complex problems into manageable sub-problems, enhancing reasoning accuracy and efficiency in complex scenarios. HyperTree Planning [18] constructs a structured, high-level outline before generating details. ReasonFlux [19] goes beyond raw text generation by scaling "thought templates". Plan-and-Solve Prompting [20] first asks the model to form an explicit plan before producing the final answer, while Least-to-Most Prompting [21] decomposes a difficult problem into simpler subproblems and solves them sequentially. SELF-DISCOVER [22] enables LLMs to compose reasoning structures from atomic modules. CoGer [23] draws on Bloom’s taxonomy to classify query complexity into four levels and trains an agent via reinforcement learning to dynamically select appropriate reasoning strategies. Another line of work lies in modifying model architectures to support hierarchical processing such as [24], [25].

In addition, several works focus on hierarchical reasoning for theorem proving. For example, [26] proposes a reinforcement learning-based training algorithm that incentivizes LLMs to hierarchically decompose theorems into lemmas. [27] decomposes complex theorem-proving tasks into small, achievable subgoals to abstract formal proof steps.

The key idea in these works is to decompose a complex problem into smaller parts, which corresponds to the proof-sketch component (Section 5.1) in our work. Our hierarchical method instead identifies core techniques, operating at a higher level than a sketch. The work most similar to ours is Reason-Flux [19]. However, it depends on constructing and retrieving from a template library for theorem proving, which does not endow the LLM itself with intrinsic hierarchical thinking capabilities. In our work, the LLM has been trained to develop insightful thinking, which essentially empowers the LLM with high-level thinking patterns.

9 Proof Details Omitted in Section 4.1↩︎

Recall that \(\pi_{\text{TP}}(p|q)\) is the probability of \(\pi_{\text{TP}}\) generating a valid proof \(p\) for question \(q\). The general form of a proof is shown in 1 . We let \(k\) be the number of core techniques in a proof \(p\). Since we assume \(\pi_{\text{TP}}(t_i |u_i, q) < \delta\) for all \(i\leq k\), by Bayes’ rule, we have \[\begin{align} & \pi_{\text{TP}}(p|q) \nonumber\\ & = \prod_{i\leq k} \left [ \pi_{\text{TP}}(r_i |t_{i-1},u_{i-2}, q) \pi_{\text{TP}}(t_i |u_i,q) \right ] \nonumber \\ & \leq \prod_{i\leq k} \delta \cdot \pi_{\text{TP}}(r_i |t_{i-1},u_{i-2}, q) \tag{5} \\ & \le \delta^k, \tag{6} \end{align}\] where the prefix \(u_i\) is defined by \(u_i := (r_1,t_1,\cdots,r_i)\). Note that 5 is obtained by the assumption \(\pi_{\text{TP}}(t_i |u_i, q) < \delta\) for all \(i\leq k\) and 6 is due to \(\pi_{\text{TP}}(r_i |t_{i-1},u_{i-2}, q)\leq 1\).

None

None

None

10 Additional Experimental Results↩︎

10.1 Experiments in Section 3↩︎

We conduct an experiment on how insightful the recent advanced commercial LLMs can be. We choose Gemini 2.5 Flash and DeepSeek-R1 to generate insights of several problems. The problems are chosen from four categories including algebra, analysis, combinatorics and number theory, each contains 10 mathematical competition level questions from Putnam and FIMO dataset. The insight generation prompt is listed in Appendix 15 titled ‘Insightfulness Evaluation’. Then we evaluate these generated insight by o3-mini through the prompt titled ‘Insight Evaluation’. The results show that most of the insights are basically listing the general standard techniques according to the conditions in questions and can not grasp the essential approaches. See a randomly chosen evaluation result of the following question. The evaluations for both models are shown in Figure 4 and Figure 5.

Question: Let \(\mathbb{R}^{+}\)be the set of positive real numbers. Determine all functions \(f: \mathbb{R}^{+} \rightarrow \mathbb{R}^{+}\) such that, for all positive real numbers \(x\) and \(y\), \[f(x+f(x y))+y=f(x) f(y)+1,\] the final answer is \(f(x)=x+1\).

: The functional equation involves terms like \(f(x + f(xy))\) and \(f(x)f(y) + 1\), suggesting the use of **substitution techniques** such as setting \(y = 1\) or \(x = 1\) to simplify and obtain relations involving \(f(1)\). A potential approach is to **explore injectivity/surjectivity** by fixing one variable and comparing expressions, then using **Cauchy-type ideas** after establishing \(f\) is linear or affine. The structure \(f(x + f(xy)) - f(x)f(y) = 1 - y\) hints at eventually proving \(f\) is of the form \(ax + b\) and then determining constants via substitution into the original equation.

Insights generated by Gemini 2.5 Flash: The presence of \(f(x+f(xy))\) and \(f(x)f(y)\) suggests looking for properties like injectivity, surjectivity, or particular values of \(f\). Substituting specific values (e.g., \(x=1\), \(y=1\)) or analyzing the fixed points of \(f\) might be crucial. The term \(f(xy)\) combined with \(f(x)f(y)\) often points to multiplicative properties or comparison with Cauchy’s functional equation variants.

We see that most of the insights generated by both Gemini 2.5 Flash and DeepSeek-R1 for this question are merely generic analysis, without getting to the essence. The insights generated by Gemini are even less accurate, and can even be regarded as “simple scratch.”

10.2 Additional Baseline Settings↩︎

We evaluate three additional baselines under the same theorem-proving setting as our main experiments. The full prompts for these baselines are provided in Appendix 15, under “Plan-and-Solve Baseline Prompt”, “Least-to-Most Prompt”, and “SELF-DISCOVER Prompt”. For Plan-and-Solve, the model is prompted to first write a concise proof plan and then generate the final proof conditioned on that plan. For Least-to-Most Prompting, the model is prompted to decompose the theorem into a sequence of easier subclaims, solve them in order, and combine the intermediate results into the final proof. For SELF-DISCOVER, the model is prompted to select and compose general reasoning modules into a task-specific reasoning structure before generating the proof.

For fairness, all three baselines start from the same standard SFT checkpoint trained only on prompt-proof pairs \((q,p)\). They are applied only at test time on Qwen2.5-7B and Llama3-8B. All generations use the same benchmark split, decoding budget, proof extraction rule, LLM-as-judge protocol, and human-audit calibration as our main experiments. Table 3 reports the resulting comparison.

8pt

10.3 Parameter Settings in Section 6↩︎

Here we provide main parameters setting for our experiments. For both model series, we use the learning rate of 2e-5, and training batch size 256. The maximal sequence length is set to be 4096 for all experiments on the base dataset, and 8192 for all on DeepInsightTheorem. We also conducted additional experiments with the baseline’s max sequence length set to 8192 for completion. See Table 4 for details.

15pt

12pt

11 Evaluation↩︎

Since our task involves generating informal mathematical proofs by natural language, we adopt an LLM-as-Judge evaluation protocol. Following the established practice in DeepTheorem [5], our evaluation is conducted on a set of challenging benchmarks to test the model’s reasoning capability. Specifically, we use theorem-proving problems drawn from FIMO [2], PutnamBench [3], and a newly constructed theorem-proving subset of the Harvard-MIT Mathematics Tournament (HMMT) [28].

To assess the quality of the generated proofs, we apply the evaluation framework in DeepTheorem but omit a separate “correctness” judgment, which is a fabricated verifiable answer constructed by DeepTheorem that is yet unrelated to the quality of proof itself and hence not applicable to our task. Our evaluation centers on the following three core dimensions of the proof text itself [5]:

• Logical Validity. Check whether each step follows logically from the preceding step and indicate any logical errors.

• Completeness. Verify whether all necessary steps are included to fully prove the theorem.

• Clarity. Assess whether the proof is clear, unambiguous, and well-explained.

We use DeepSeek-R1 [7] as the judge model. For each generated proof, the judge is prompted to analyze and score it on a continuous scale from 0 to 1 for each of the three dimensions above. The final score for a proof is calculated as a weighted average of these three-dimensional scores. The specific weighting scheme and the full prompts used for this evaluation are provided in Appendix 15.

Using only one LLM as a judge may introduce bias in evaluation. To address this, we also incorporate o3-mini as another LLM judge and combine the scores from both judges to evaluate the performance of our method. See Table 2 in Appendix 10.3 for details.

In addition to multi-judge aggregation, we use a lightweight human-audit protocol to reduce systematic bias in LLM-as-Judge evaluation. We stratify generated proofs by model family, benchmark, and LLM-judge score range, and then sample a small subset for expert inspection. Human reviewers evaluate the same dimensions used by the verifier: insight quality, logical validity, completeness, and clarity. For insight quality, reviewers check whether the generated core techniques capture the key mathematical idea rather than merely restating surface conditions. For proof quality, reviewers check whether the proof sketch and final proof correctly realize the stated techniques and whether any essential derivation is missing. The audited subset is used to calibrate verifier behavior by comparing human scores with LLM scores, checking score deviations across dimensions, and identifying cases where the verifier systematically over-rewards verbose or superficially plausible proofs. As shown in Figure 9, the statistics are computed on a single stratified audit pool aggregated across FIMO, PutnamBench, and HMMT

Finally, since the model trained by our method would generate a formatted output containing three components, we extract only the final proof component for evaluation to ensure a fair comparison with baseline methods.

12 Data Construction↩︎

As we discussed before, the construction of our data is based on the DeepTheorem [29] by annotating each piece of data with the assistance of DeepSeek-R1 to help generate the core techniques and corresponding proof sketches. After the generation process, we apply a filtering process to remove some data that failed to be annotated due to some reasons like temporary API calling failure or annotated with an undesired structure. Also we notice some repeated questions in the base dataset hence we also remove those redundant ones.

Finally, we collect 104,751 pieces of hierarchical data with rigorous structure as shown in Figure 6. The distribution of each class of techniques is summarized in Figure 10.

. A fundamental principle of DeepInsightTheorem is its self-contained nature. The creation of the hierarchical structure \((q, \{t_i\}, s, p)\) is achieved solely through the analysis of the information already embedded within the original proofs. By doing so, we increase the informational density of each training example, offering a powerful pathway to improve data efficiency when scaling high-quality mathematical proof data.

13 Benchmark Statistics↩︎

Table 7 is a simple statistic on the number of questions in three benchmarks we use for evaluation. Note that in [29], they manually expanded each benchmark with variants of each question. Here we do not need such a design.

14 Qualitative Case Study↩︎

We present a qualitative case study to demonstrate the improved evaluation results. It compares the output generated by the Qwen2.5-7B model trained on DeepInsightTheorem with the baseline output for a sample problem from HMMT. The chosen problem is “2025-02-combinatorics-04”.

Evaluation of Our Method. We achieved a score of 0.9 for this problem with a minor completeness issue.

Logical Validity: “The algorithm is correct and would work, no logical flaw in the structure.”

Completeness: “the algorithm is complete and the answer is stated, but the computation is omitted. It’s partial.”

Clarity: “The steps are well-explained and clear.”

Evaluation of the Baseline. The baseline produces a low-quality proof, receiving a score of 0.19.

Logical Validity: “The proof is logically invalid due to an incorrect reduction to only right and up moves, a flawed bijection in Step 3 and the contradiction between Step 4 and Step 5.”

Completeness: “The proof is incomplete as it misses paths using diagonal moves, does not account for variable path lengths, and fails to properly handle the no-revisit constraint.”

Clarity: “The proof has a structured outline, but the marking system in Step 3 is ambiguous, and the numerical inconsistency creates confusion.”

In summary, our method helps the model establish a solid logical ability and cultivate its insight to plan for the reasoning path.

15 Prompt Templates↩︎

We present all prompts on the remaining pages.

References↩︎

---

1. Long chain-of-thought reasoning often make the model first go over the whole proof and then summarize the core techniques, which is against the thinking pattern of insight. Therefore, it is more appropriate to disable the thinking mode.↩︎