Learning to Reason with Insight for Informal Theorem Proving Yunhe Li∗1 Hao Shi∗2 Bowen Deng∗1 Wei Wang∗3 Mengzhe Ruan1 Hanxu Hou4 Zhongxiang Dai5 Siyang Gao1 Chao Wang13 Shuang Qiu†1 Linqi Song†1 1 City University of Hong Kong 2 Tsinghua University 3 Ke Holdings Inc. 4 Shenzhen University of Advanced Technology 5 Chinese University of Hong Kong, Shenzhen {uuen.li,bowdeng2-c,cs.mzr}@my.cityu.edu.hk [email protected] {wwgoing, houhanxu}@163.com [email protected] [email protected] {siyangao,shuanqiu,linqi.song}@cityu.edu.hk
arXiv:2604.16278v1 [cs.AI] 17 Apr 2026
Abstract
et al., 2022). 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 Welleck et al. (2022) and Zhang et al. (2025b), 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 A. 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, our work first introduces DeepInsightTheorem, a newly con-
Although most of the automated theoremproving approaches depend on formal proof systems, informal theorem proving can align better with large language models’ (LLMs) strength in natural language processing. In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight, namely the difficulty of recognizing the core techniques required to solve complex problems. To address this, we propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning. We propose DeepInsightTheorem, a hierarchical dataset that structures informal proofs by explicitly extracting core techniques and proof sketches alongside the final proof. To fully exploit this dataset, we design a Progressive Multi-Stage SFT strategy that mimics the human learning process, guiding the model from basic proof writing to insightful thinking. Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines. These results demonstrate that teaching models to identify and apply core techniques can substantially improve their mathematical reasoning.
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 (Zheng et al., 2022; Liu et al., 2023a; Tsoukalas et al., 2024) or by using specialized languages (Welleck ∗ †
Equal contribution. Corresponding author.
1
structed hierarchical dataset that substantially extends the prior DeepTheorem framework (Zhang et al., 2025b), with the extraction of common core techniques. Then, we propose a novel progressive multi-stage training strategy correspondingly, which is carefully designed to emulate key aspects of the human learning process, thereby training LLM for insightful reasoning. Through extensive experiments, we demonstrate that this insightaware 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, insightdriven mathematical reasoning. The primary contributions of our work are summarized as follows:
the vocabulary when it is working. To train a generation policy πθ to be a theorem-prover, the training datasets are collected from many resources of math corpus and commonly formed as theoremproof pairs (q, p). For Supervised Fine-Tuning (SFT) on such a dataset, the objective is to solve maxθ Eq∼D,p∼DP (q) πθ (p|q), where D is the distribution of the math problems in the training set and DP (q) is the distribution over the valid proofs of each question in the training set. 2.1
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 xn+1 = U xn for n ≥ 0. This Picard iteration constructs the sequence x0 , x1 = U x0 , x2 = U 2 x0 , . . .”.
• We demonstrate the importance of core techniques in informal theorem proving, showing that models’ high perplexity in informal theorem proving largely arises from difficulties in recognizing and applying the core techniques. • We introduce the notion of mathematical insight and propose an insight-guided reasoning paradigm, which can improve mathematical reasoning when paired with a well-designed method. • We construct a novel hierarchical dataset, named DeepInsightTheorem, by explicitly extracting core techniques from base datasets, which facilitates both technique review and insight-driven reasoning.
• 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 τ on the set of integers Z..., shifting the language and tools entirely from number theory to topology.” Formally, we denote the space of techniques as T ⊂ S that contains all possible techniques in those three classes. Generally, we can then write each proof p of q as an ordered sequence
• We design a progressive, multi-stage training scheme that effectively leverages the hierarchical structure of DeepInsightTheorem to enhance informal theorem proving, and we validate its effectiveness through extensive experiments.
2
Notion of Insight
Preliminary
We consider the context of informal mathematical proof generation. Let V be the vocabulary, which is a finite discrete set. The text sequence space S is defined as the union S of lthe product spaces of any finite power S ≜ ∞ l=0 V . We can then denote the space of theorems as a subspace Q of S which contains all well-defined math problems for theorem-proving. For any q ∈ Q, we denote the space of proofs with respect to q as P(q) ⊂ S that contains all valid proofs of q. The LLM Mθ is an auto-regressive network which will predict the next token’s distribution over
p = (r1 , t1 , r2 , t2 , · · · , rk ),
(1)
where ti ∈ T , ri 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 2
Figure 1: The top figure illustrates the construction of DeepInsightTheorem, and the bottom figure depicts our progressive multi-stage SFT procedure.
4
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.
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 π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 (Qwen Team, 2025) for the well-known Baire Category Theorem in General Topology, tokens with spiking entropy consistently signal the presence of core techniques:
We evaluated several powerful commercial LLMs with a non-thinking mode1 , including Gemini 2.5 Flash (Gemini Team, 2025) and DeepseekR1 (DeepSeek-AI, 2025), by prompting them to provide insights for math competition problems randomly sampled from Putnam and FIMO datasets (See Appendix F 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 C.1). Here, depth indicates the insight is specific and technically accurate, rather than a generic, highlevel 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.
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.
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.
3
Figure 2: The generated proof of the Baire Category Theorem generated by Qwen2.5-14B-Instruct. From light grey to deep warm color, the token entropy increases. Most tokens are of low entropy, composing basic mathematical reasoning. Tokens with a spiking entropy indicate core techniques.
As discussed above, the model π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 πTP (ti |ui , q) < δ
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.
(2)
4.2
for some small constant δ > 0 and any ti ∈ T , where ui := (r1 , t1 , · · · , ri ) denotes the prefix before ti 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 ti from the question q bounded by δ: X πTP (ti |q) = πTP (ti |ui , q)πTP (ui |q) < δ.
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:
ui
Similarly, by recursively applying (2), for the probability of generating a valid full proof p for q via πTP , we have πTP (p|q) ≤ δ 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 B. We can interpret the value πTP (ti |q) as the insightfulness of πTP in identifying technique ti ∈ T . A higher value indicates stronger insight in recognizing ti 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
• 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 4
for a proof p via a policy πθ parameterized by θ: πθ (t, p|q) = πθ (t|q)πθ (p|t, q),
corpora and strict decontamination against major benchmarks (e.g., MATH (Hendrycks et al., 2021), AIME (AIME Dataset), miniF2F (Zheng et al., 2022)). 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 Zhang et al. (2025b) for further details.
(3)
where t = (t1 , · · · , tk ). In (3), we first identify the required core techniques t via πθ (t|q) before generating the proof p. The proof p is then generated conditioned on the identified techniques t via πθ (p|t, q). Consequently, the performance of πθ depends critically on how well the first factor πθ (t | q) is learned. In the following sections, we construct a well-curated dataset and propose a novel multi-stage method to optimize θ such that both πθ (t | q) and πθ (p | 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:
DeepInsightTheorem. 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: q, (t1 , . . . , tm ), | {z s }, p . | {z } {z } |
πθ (t, s, p|q) = πθ (t|q)πθ (s|t, q)πθ (p|s, t, q), (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
core techs
sketch
proof
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 ti . 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.
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 (Zhang et al., 2025b) dataset, a recently introduced, large-scale resource for informal mathematical theorem proving.
• 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 highlevel 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.
Base Dataset. DeepTheorem (Zhang et al., 2025b) provides a robust foundation of 121K high-quality informal theorem-proof pairs at roughly IMOlevel difficulty. It is constructed through a rigorous pipeline, including collection from diverse
We refer to the resulting dataset as DeepInsightTheorem, highlighting the insight-driven hierarchical structure derived from DeepTheorem. See the 5
Methods
FIMO
Putnam
HMMT
Qwen2.5-7B Llama3-8B
15.73 12.50
37.01 36.69
12.59 9.98
Table 1: Evaluation results for models solely trained on DeepInsightTheorem
5.2
Figure 3: Distribution of core technique counts
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 theoremproof 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 πθ (p|q) and πθ (ri |r≤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 sketchconditioned generation and finally techniqueguided 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:
top of Figure 1 for an overview, and Figure 6 for a concrete example. Chain-of-Thought in Insight. 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. Acquisition-Application Transition. 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 F. Key Statistics. 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 8.
• Stage 1 (Apprentice): (q, p). We first train the model on plain theorem-proof pairs to acquire basic proof-generation ability. This stage cor6
responds to a novice learner studying complete solutions.
cate any logical errors. • Completeness. Verify whether all necessary steps are included to fully prove the theorem.
• 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.
• Clarity. Assess whether the proof is clear, unambiguous, and well-explained. We use DeepSeek-R1 (DeepSeek-AI, 2025) 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 threedimensional scores. The specific weighting scheme and the full prompts used for this evaluation are provided in Appendix F. 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 3 in Appendix C.2 for details. 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.
• Stage 3 (Expert): (q, {ti }, 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 techniquedriven reasoning paradigm. This multi-stage training strategy is illustrated in Figure 1 bottom. Overall, the progressive multistage 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 {ti }). Since each mapping is not yet adequately learned by the model, continued training does not cause overfitting.
6
7
Experiments
We conduct experiments on two open-source model families: Qwen2.5 (Qwen Team, 2025) and Llama3 (Llama Team, 2024). For each family, we start from their respective base models (e.g., Qwen2.5-Base, Llama3.2-Base).
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 (Zhang et al., 2025b), our evaluation is conducted on a set of challenging benchmarks to test the model’s reasoning capability. Specifically, we use theoremproving problems drawn from FIMO (Liu et al., 2023a), PutnamBench (Tsoukalas et al., 2024), and a newly constructed theorem-proving subset of the Harvard-MIT Mathematics Tournament (HMMT) (Tournament, 2025). To assess the quality of the generated proofs, we apply the evaluation framework in DeepTheorem but omit a separate “correctness” judgment, which is not applicable to our task. Our evaluation centers on the following three core dimensions of the proof text itself (Zhang et al., 2025b):
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 theoremsketch-proof stage. The motivation for this design is that the core part of our hierarchical structure is the insight and the conceptual jump from
• Logical Validity. Check whether each step follows logically from the preceding step and indi7
Models Qwen2.5-1.5B
Methods Base Two-stage Three-stage
FIMO 11.17 11.81 12.57
Putnam 25.39 28.72 27.06
HMMT 11.25 11.80 13.68
Avg. 15.94 17.44 17.77
Qwen2.5-3B
Base Two-stage Three-stage
11.92 12.85 13.34
31.87 34.86 35.69
12.69 11.98 14.06
18.83 19.90 21.03
Qwen2.5-7B
Base Two-stage Three-stage
15.27 16.33 18.03
36.75 43.34 41.67
14.82 15.59 17.78
22.28 25.09 25.83
Llama3.2-1B
Base Two-stage Three-stage
5.04 4.19 6.25
14.61 18.26 18.26
4.48 5.78 7.60
8.04 9.41 10.70
Llama3.2-3B
Base Two-stage Three-stage
9.29 11.08 10.72
23.90 24.73 26.73
7.04 9.27 8.89
13.41 15.03 15.45
Llama3-8B
Base Two-stage Three-stage
13.48 14.70 14.62
37.68 40.51 38.51
12.25 14.15 14.30
21.14 23.12 22.48
Table 2: Evaluation of models trained with our methods and the baseline by Deepseek-R1
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.
implies that insight-guided thinking can help break the reasoning ability ceiling for small models. Our framework is competitive with RLfinetuned SOTA models. The comparison can be seen on Table 5 in Appendix C.2. These results demonstrate that, despite relying solely on SFT, our model already achieves performance that is competitive with those SOTA models of same size and extensive post-training. This further implies a highly potential advantage over those SOTA models when there is an appropriate RL approach implemented on our model.
Moreover, we evaluate the theorem-proving performance for several open-source models. These state-of-the-art (SOTA) LLMs typically have been further enhanced via RL-based post-training. We compare them with Qwen2.5-7B model fine-tuned with our approach. 7.1
Main Results
7.2 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”.
Our framework achieves better performance. The main results are presented in Table 2 and Table 3. Table 2 presents the scores from DeepSeek-R1, while Table 3 shows the average scores from both DeepSeek-R1 and o3-mini. 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 C 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
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.” 8
Models Qwen2.5-1.5B
Qwen2.5-3B
Qwen2.5-7B
Llama3.2-1B
Llama3.2-3B
Llama3-8B
Methods Base Two-stage Three-stage Base Two-stage Three-stage Base Two-stage Three-stage Base Two-stage Three-stage Base Two-stage Three-stage Base Two-stage Three-stage
FIMO 12.63 13.09 14.35 12.92 15.05 14.99 16.89 18.39 19.31 6.72 6.91 8.49 10.46 11.98 12.54 15.61 16.70 15.98
Putnam 26.66 30.06 30.21 32.94 35.00 35.94 37.76 45.20 43.35 16.20 20.78 21.55 24.43 24.69 27.51 38.65 42.76 41.61
HMMT 12.79 13.42 15.30 17.04 18.88 20.21 15.52 17.76 18.49 4.25 6.76 8.02 8.84 11.09 10.77 13.67 16.51 16.64
Avg. 17.36 18.86 19.95 24.30 28.31 28.71 23.39 27.12 27.05 9.06 11.48 12.69 14.58 15.92 16.94 22.64 25.32 24.74
Table 3: Average evaluation scores of models trained with our methods and the baseline by Deepseek-R1 and o3-mini
Clarity: “The steps are well-explained and clear.”
ing to identify core techniques. Comprehensive evaluations show consistent improvements over strong baselines on challenging benchmarks.
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.
8
References DeepSeek-AI. 2025. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. CoRR. Kefan Dong, Arvind Mahankali, and Tengyu Ma. 2024. Formal theorem proving by rewarding llms to decompose proofs hierarchically. Preprint, arXiv:2411.01829. Google Gemini Team. 2025. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. Technical report, Google. Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. 2024. ABEL: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. Runquan Gui, Zhihai Wang, Jie Wang, Chi Ma, Huiling Zhen, Mingxuan Yuan, Jianye Hao, Defu Lian, Enhong Chen, and Feng Wu. 2025. Hypertree planning: Enhancing llm reasoning via hierarchical thinking. Preprint, arXiv:2505.02322.
Conclusion
This paper studies informal theorem proving and identifies core techniques as a key bottleneck in model training. To address this, we build a hierarchical dataset DeepInsighTheorem and a progressive curriculum-style SFT framework that trains LLMs for insightful reasoning by explicitly learn-
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the math dataset. NeurIPS.
9
Jiewen Hu, Thomas Zhu, and Sean Welleck. 2025a. minictx: Neural theorem proving with (long)contexts. Preprint, arXiv:2408.03350.
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. 2022. Naturalprover: Grounded mathematical proof generation with language models. Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA.
Jinwu Hu, Dongjin Yang, Langyu Bian, Zhiquan Wen, Yufeng Wang, Yaofo Chen, Bin Xiao, Yuanqing Li, and Mingkui Tan. 2025b. Beyond fast and slow: Cognitive-inspired elastic reasoning for large language models. Preprint, arXiv:2512.15089.
Ling Yang, Zhaochen Yu, Bin Cui, and Mengdi Wang. 2025. Reasonflux: Hierarchical llm reasoning via scaling thought templates. Preprint, arXiv:2502.06772.
Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. 2025. Lean-star: Learning to interleave thinking and proving. Preprint, arXiv:2407.10040.
Ziyu Ye, Jiacheng Chen, Jonathan Light, Yifei Wang, Jiankai Sun, Guohao Li, Mac Schwager, Philip Torr, Yuxin Chen, Kaiyu Yang, Yisong Yue, and Ziniu Hu. 2024. Reasoning in reasoning: A hierarchical framework for (better and faster) neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24.
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, , and Qun Liu. 2023a. FIMO: A challenge for- mal dataset for automated theorem proving. CoRR. Chengwu Liu and 1 others. 2023b. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295.
Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhenwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, and Dong Yu. 2025a. DEEPTHEOREM: Advancing llm reasoning for theorem proving through natural language and reinforcement learning.
Pan Lu, Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, and James Zou. 2025. Solving inequality proofs with large language models. Preprint, arXiv:2506.07927.
Ziyin Zhang and 1 others. 2025b. Deeptheorem: Advancing llm reasoning for theorem proving through natural language and reinforcement learning. arXiv preprint arXiv:2505.23754.
Gabriel Poesia, David Broman, Nick Haber, and Noah D. Goodman. 2024. Learning formal mathematics from intrinsic motivation. Preprint, arXiv:2407.00695.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations (ICLR). ArXiv:2109.00110.
Haoran Sun and Shaoning Zeng. 2025. Hierarchical memory for high-efficiency long-term reasoning in llm agents. Preprint, arXiv:2507.22925. AIME Dataset. AIMO Validation AIME Dataset. Url: https://huggingface.co/datasets/AI-MO/aimovalidation-aime.
Pei Zhou, Jay Pujara, Xiang Ren, Xinyun Chen, HengTze Cheng, Quoc V. Le, Ed H. Chi, Denny Zhou, Swaroop Mishra, and Huaixiu Steven Zheng. 2024. Self-discover: Large language models self-compose reasoning structures. Preprint, arXiv:2402.03620.
Llama Team. 2024. The llama 3 herd of models. Technical report, AI @ Meta. Qwen Team. 2025. Qwen2.5 technical report. Technical report, Qwen. Harvard-MIT Mathematics Tournament. 2025. Hmmt dataset and resources. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami tayush Thakur, and Swarat Chaudhuri. 2024. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Process- ing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada. Guan Wang, Jin Li, Yuhao Sun, Xing Chen, Changling Liu, Yue Wu, Meng Lu, Sen Song, and Yasin Abbasi Yadkori. 2025. Hierarchical reasoning model. Preprint, arXiv:2506.21734.
10
A
Related Work
ment learning to dynamically select appropriate reasoning strategies. Another line of work lies in modifying model architectures to support hierarchical processing such as Wang et al. (2025), Sun and Zeng (2025). In addition, several works focus on hierarchical reasoning for theorem proving. For example, Dong et al. (2024) proposes a reinforcement learningbased training algorithm that incentivizes LLMs to hierarchically decompose theorems into lemmas. Ye et al. (2024) decomposes complex theoremproving 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 ReasonFlux (Yang et al., 2025). 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.
Formal theorem proving. Formal automated theorem proving (ATP) relies on proof assistants such as Lean, Coq, and Isabelle (Zheng et al., 2022, Liu et al., 2023a, Tsoukalas et al., 2024), where correctness is enforced by a strict formal system. Recent work integrates large language models with formal proof environments to combine naturallanguage generation with machine-checkable verification (Gloeckle et al. (2024), Hu et al. (2025a), Lin et al. (2025), Poesia et al. (2024)). Representative benchmarks include miniF2F for crosssystem olympiad-level evaluation (Zheng et al., 2022), as well as more challenging datasets that target IMO-/Putnam-style mathematics (Liu et al., 2023b; Tsoukalas et al., 2024). 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. 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 naturallanguage theorem–proof corpora (Welleck et al., 2022), and NaturalProver studies grounded proof generation in reference/retrieval settings (Welleck et al., 2022). Tencent’s DeepTheorem further advances IMO-level informal proving with largescale data and reinforcement-learning-style training recipes (Zhang et al., 2025b). Lu et al. (2025) focuses specifically on inequality proofs. Despite this progress, many systems remain largely endto-end and do not explicitly identify or control the core techniques that drive a proof.
B
Proof Details Omitted in Section 4.1
Recall that πTP (p|q) is the probability of π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 πTP (ti |ui , q) < δ for all i ≤ k, by Bayes’ rule, we have πTP (p|q) Y = [πTP (ri |ti−1 , ui−2 , q)πTP (ti |ui , q)] i≤k
Hierarchical Reasoning. Hierarchical reasoning for LLMs decomposes complex problems into manageable sub-problems, enhancing reasoning accuracy and efficiency in complex scenarios. HyperTree Planning (Gui et al., 2025) constructs a structured, high-level outline before generating details. ReasonFlux (Yang et al., 2025) goes beyond raw text generation by scaling "thought templates". SELF-DISCOVER (Zhou et al., 2024) enables LLMs to compose reasoning structures from atomic modules. CoGer (Hu et al., 2025b) draws on Bloom’s taxonomy to classify query complexity into four levels and trains an agent via reinforce-
≤
Y i≤k k
≤δ ,
δ · πTP (ri |ti−1 , ui−2 , q)
(5) (6)
where the prefix ui is defined by ui := (r1 , t1 , · · · , ri ). Note that (5) is obtained by the assumption πTP (ti |ui , q) < δ for all i ≤ k and (6) is due to πTP (ri |ti−1 , ui−2 , q) ≤ 1.
11
O3-mini’s Evaluation-Deepseek-r1 1. mixed 2. mixed 3. incomplete Below is an explanation for each answer: 1. Mixed: The insight mentions several techniques—substitution (setting y = 1 or x = 1), exploring injectivity/surjectivity, and even hinting at Cauchy-type ideas as a route to establishing linearity. However, these ideas remain quite standard for this type of functional equation problem. They are useful, but the answer doesn’t pinpoint any single, non-trivial transformation or method that clearly stands out as a breakthrough insight; it rather relies on a collection of standard tactics. Thus, while not entirely shallow, the ideas include both non-shallow observations and standard, almost routine deductions. 2. Mixed: The insight does provide some accurate general directions, which are key in many functional equation proofs. However, the description remains somewhat vague and does not detail enough concrete, non-trivial steps. This mix of accurate generalizations and lack of detailed construction leads to a "mixed" evaluation. 3. Incomplete: While the insight mentions common techniques, it does not capture all potential core ideas needed to solve the problem. There could be additional subtleties—such as a rigorous step-by-step approach to prove that f must be affine or specific manipulations that pivot the equation to reveal the structure f (x) = x + 1. Therefore, the core techniques mentioned are not fully comprehensive to cover all aspects of the solution; they provide an initial guide but remain incomplete.
Figure 4: o3-mini’s evaluation response for the insight generated by Deepseek R1
12
O3-mini’s Evaluation-Gemini2.5-Flash 1. mixed 2. simple scratch 3. incomplete Below is the explanation for each: 1. Mixed: The insight mentions exploring properties like injectivity, surjectivity, particular substitutions (e.g., x = 1, y = 1), and fixed points, and notes that the structure of the equation suggests multiplicative features. While these are useful starting points, they represent standard techniques in functional equation problems. They do hint at a deeper structure but do not provide a concrete key step that addresses the heart of obtaining f (x) = x + 1. Thus, there exists a mix of non-trivial ideas combined with basic, common observations. 2. Simple Scratch: The insight lists several exploratory steps but does so in a rather vague manner without a precise roadmap tailored to this particular question. The ideas are on the right track but lack the detail needed for a detailed, step-by-step core technique application. 3. Incomplete: While the insight addresses several common techniques for approaching functional equations, it does not cover all the essential steps needed to rigorously derive f (x) = x + 1. Additional deeper reasoning, such as deducing specific values (like evaluating f (1)) and showing uniqueness or employing clever substitutions that eventually simplify the functional relationship, is necessary. Thus, the list of techniques provided is not comprehensive enough to fully solve the problem without filling in significant logical and algebraic deductions.
Figure 5: o3-mini’s evaluation response for the insight generated by Gemini 2.5 Flash
13
Question: Let X be a non-negative random variable and g : [0, ∞) → [0, ∞) be a monotone nondecreasing function such that g(x) → ∞ as x → ∞. If g(X) is integrable, i.e., E[g(X)] < ∞, prove that limx→∞ g(x)P (X > x) = 0. Response: <tech> Let’s analyze the conditions in this question. The monotonicity and divergence of g naturally suggest linking the tail event {X > x} to the growth of g(X), forming a crucial inclusion that leverages g’s behavior. The integrability of g(X) prompts Markov’s inequality to bound the tail probability by an expectation, exploiting the non-negativity and finite mean. The pointwise convergence to zero, combined with the integrable bound g(X), calls for the Dominated Convergence Theorem to justify limit-interchange, which is indispensable since the expectation structure captures the asymptotic decay. Therefore, the potential techniques are summarized as: <construction>: Event inclusion {X > x} ⊆ {g(X) ≥ g(x)} via monotonicity of g <theorem call>: Markov’s inequality and Dominated Convergence Theorem <transformation>: no </tech> <sketch> 1. Use the monotonicity and divergence of g to establish {X > x} ⊆ {g(X) ≥ g(x)}, implying P (X > x) ≤ P (g(X) ≥ g(x)). 2. Apply Markov’s inequality to the nonnegative integrable g(X), yielding g(x)P (X > x) ≤ E[g(X)1{g(X)≥g(x)} ]. 3. Observe pointwise convergence g(X)1{g(X)≥g(x)} → 0 due to g(x) → ∞, and dominate by g(X). 4. Invoke the Dominated Convergence Theorem to show E[g(X)1{g(X)≥g(x)} ] → 0. 5. Conclude limx→∞ g(x)P (X > x) = 0 via the squeeze theorem on 0 ≤ g(x)P (X > x) ≤ E[g(X)1{g(X)≥g(x)} ]. </sketch> <proof> Since g is monotone nondecreasing, for any x ≥ 0, the condition X > x implies g(X) ≥ g(x). This gives the event inclusion: {X > x} ⊆ {g(X) ≥ g(x)}, which, by monotonicity of probability, yields: P (X > x) ≤ P (g(X) ≥ g(x)). As g(X) is nonnegative and E[g(X)] < ∞, Markov’s inequality for a = g(x) > 0 (for large x since g(x) → ∞) states: E[g(X)1{g(X)≥g(x)} ] P (g(X) ≥ g(x)) ≤ . g(x) Multiplying by g(x) and using the earlier inequality, we obtain: g(x)P (X > x) ≤ g(x)P (g(X) ≥ g(x)) ≤ E[g(X)1{g(X)≥g(x)} ]. Fix ω ∈ Ω. As x → ∞, g(x) → ∞ so g(x) > g(X(ω)) for large enough x, forcing 1{g(X(ω))≥g(x)} = 0. Thus: lim g(X(ω))1{g(X(ω))≥g(x)} = 0, ∀ω. x→∞
Moreover, 0 ≤ g(X)1{g(X)≥g(x)} ≤ g(X), and E[g(X)] < ∞ by hypothesis. Convergence Theorem: lim E[g(X)1{g(X)≥g(x)} ] = E
x→∞
h
By the Dominated
i lim g(X)1{g(X)≥g(x)} = E[0] = 0.
x→∞
Finally, sandwiching with: x→∞
0 ≤ g(x)P (X > x) ≤ E[g(X)1{g(X)≥g(x)} ] − −−− → 0, we conclude limx→∞ g(x)P (X > x) = 0 as required. </proof>
Figure 6: A data example from DeepInsightTheorem
14
C
Additional Experimental Results
C.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 F 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.
Figure 7: Max scores in evaluation across benchmarks.
Question: Let R+ be the set of positive real numbers. Determine all functions f : R+ → R+ such that, for all positive real numbers x and y,
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.”
f (x + f (xy)) + y = f (x)f (y) + 1, the final answer is f (x) = x + 1.
C.2
Parameter Settings in Section 7
Insights generated by Deepseek-R1: 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.
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. Methods
FIMO Putnam HMMT
Qwen2.5-7B 14.98 Llama3-8B 13.29
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.
36.05 38.84
15.24 11.99
Avg. 22.09 21.37
Table 4: Evaluation of baseline with max length 8092
D
Data Construction
As we discussed before, the construction of our data is based on the DeepTheorem (Zhang et al., 2025a) 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
We see that most of the insights generated by both Gemini 2.5 Flash and DeepSeek-R1 for this 15
Models
FIMO
Putnam
HMMT
Avg.
Qwen2.5-Inst-7B
15.29
42.39
17.86
25.12
Qwen2.5-Math-Inst-7B
17.01
41.06
16.57
24.92
DS-Prover-v1.5-RL-7B
17.39
42.00
13.68
24.36
DS-Prover-v2-7B
16.25
41.50
15.43
24.39
Ours (2-stage)
16.33
43.34
15.59
25.09
Ours (3-stage)
18.03
41.67
17.78
25.83
Table 5: Evaluation score comparison against Open-Source Baselines
Benchmark
Num.
F
FIMO Putnam HMMT
71 166 76
We present all prompts on the remaining pages.
Table 6: The number of questions in each benchmark
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 10,4751 pieces of hierarchical data with rigorous structure as shown in Figure 6. The distribution of each class of techniques is summarized in Figure 8. Maximizing Data Utility. A fundamental principle of DeepInsightTheorem is its self-contained nature. The creation of the hierarchical structure (q, {ti }, 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.
E
Evaluation
Table 6 is a simple statistic on the number of questions in three benchmarks we use for evaluation. Note that in Zhang et al. (2025a), they manually expanded each benchmark with variants of each question. Here we do not need such a design.
16
Prompt Templates
Figure 8: Top technique distribution for each class in DeepInsightTheorem
Figure 9: Max scores in evaluation across benchmarks.
Insight Generation Now you are tested the insight this math question: {question} From now on you can not go on thinking and expanding the proof step by step. Instead, try to infer the most potential core techniques that would be used in this question by ONLY analyzing the conditions in the question. You can only have a short and quick guess without detailed and long deduction. The core techniques may refer to specific mathematical construction, use of known theorem or existing results or smart and subtle mathematical transformations, instead of those fundamental logic deduction. Output: Latex formatted core precise techniques in your prediction for around 3 sentences.
17
Insightfulness Evaluation The core techniques in math proof may refer to specific mathematical construction, use of known theorem or existed results or smart and subtle mathematical transformations for particular question, instead of those fundamental mathematical and logic deduction details. Now you have the following question: {}. And a given insight which contains the prediction of core techniques to this question: {} Now you need to review and evaluate this insight from the following aspects: 1. see if there exists an idea in this insight that is highly key to the solution, which in general is likely to be found or realized after several thinking steps, or the other steps in the solution are far easier after dealing with this core idea. Note that such idea can not vaguely hints without providing concrete methods and identifying the core non-trivial step. And hence determine whether the insight is shallow quick guess or deep identification. 2. see if the core ideas described in the insight is accurate enough. Check if the idea gives the precise techniques key and adapted particularly to the question. It does not need to be containing details but accurately describe mentioned techniques. And hence determine whether the idea is a simple scratch or an accurate expression. 3. see if the core techniques mentioned in this insight are all core techniques for the question. check whether the question can be solved by filling basic mathematical and logical deductions ONLY under the core techniques in the insight. And hence determine whether the insight is comprehensive or incomplete. –output: For 1, if all ideas in the insight are not shallow quick guess, and there are no flaws in the whole insight, then output ’deep identification’. If there are also some ideas that are shallow quick guess, or even there are some flaws in this insight, output ’mixed’. Note that mixed means there indeed exist non-shallow ideas, but also other standard observations. Otherwise, if there are all shallow quick guess or just spread out standard general techniques in the insight without an accurate orientation, then output ’shallow quick guess’. For 2, if all ideas in the insight are satisfied, then output ’detailed expression’. If all are not satisfied, output ’simple scratch’. otherwise output ’mixed’. For 3, if all ideas in the insight are enough core ideas for the question, then output ’comprehensive’. If not, output ’incomplete’. format: 1. ’deep identification’/ ’shallow quick guess’/’mixed’ 2. ’detailed expression’/’simple scratch’/’mixed’ 3. ’comprehensive’/’incomplete’/’mixed’
18
Data Construction Analyze the mathematical problem and solution below: Problem: {question} Solution: {response} Perform these tasks: 1. First identify 1-3 core mathematical techniques used in the solution by considering if there are some specific constructions, theorem or existed results calling and smart mathematical transformations, where the smart transformation may not be known results and are subtle and hard to note. Note that the core mathematical techniques are not those basic logic deductions. They need to be crucial to the solution. Then Write the analysis for each technique on how a person can realize such technique when reading the question. The analysis should be from several aspects, including how the problem settings or assumptions suggest this technique, how it might be potentially useful to prove the result and why it might be crucial to the whole proof. The analysis should be like an insightful and experienced math professor’s thoughts when he is trying to solve the question. The whole analysis should start with ’Let’s analyze the conditions in this question.’ The analysis contains 2-3 sentences for each technique. The analysis should avoid mentioning the solution. Make sure the logic of the analysis is coherent. After analysis, write the extracted techniques following the analysis through ’Therefore, the potential techniques are summarized as...’, with three tags: <construction>: identify the specific construction used in the solution if any; <theorem call>: specify the theorem or any existed results used in the solution if any; <transformation>: specify the smart mathematical transformations used in the solution if any. If there are no such techniques, just specify ’no’ after the tag, but you must write the tag <construction>, <theorem call> and <transformation> even there are no such techniques. Do not write one technique under two tags both. The whole technique analysis, e.g., the analysis and technique extraction, should be with LaTeX inline math ($... $ ) where appropriate. 2. Create a proof sketch integrating these techniques analyzed from task 1, which serves as a high-level proof organization: - Format: Numbered steps in LaTeX - Each step: 1 sentence with key mathematical reasoning - Include essential formulas in math mode - Example: ’\\begin{{enumerate}}\\item Assume $P$ is countable: $P = \\{{x_1, x_2, \\. . . \\}}$\\end{{enumerate}}’
19
Data Construction (cont’d) [t] 3. Based on the original given solution, improve the solution by elaborating each step in the proof sketch, making it well-organized. 4. Output: - mathematical techniques: string (LaTeX formatted) - proof sketch: string (LaTeX enumerated steps) - solution: string (LaTeX formatted) The mathematical techniques are enclosed within <tech></tech>, the proof sketch is enclosed within <sketch></sketch> and the solution is enclosed within <proof></proof>, respectively, i.e., <tech> mathematical technique analysis here </tech> <sketch> proof sketch here </sketch> <proof> solution here </proof>
20
Proof Evaluation The following question asks to prove a statement. The question: {question} The test subject’s solution: {response} Your task is to evaluate the proof’s quality and assign a score from 0 to 1 based on three criteria: logical validity (40%), completeness (30%), and clarity (30%). Instructions: 1. Analyze the proof step by step. 2. For each criterion: - Logical Validity: Check if each step follows logically from the previous one. Flag any logical errors. - Completeness: Verify if all necessary cases and steps are included to prove the theorem. - Clarity: Assess if the proof is clear, unambiguous, and well-explained. 3. Assign a sub-score (0 to 1) for each criterion and compute the total score using the weights: (0.4 × validity) + (0.3 × completeness) + (0.3 × clarity). 4. Provide a brief explanation (2-3 sentences) summarizing any errors or issues and justifying the score. Output: - Your total score: float; - Your sub-scores and corresponding brief explanation: - Sub-score: float; - Brief explanation: string (LaTeX formatted) The total score is enclosed in <score></score>, and the sub-scores with corresponding explanation are enclosed in <exp></exp>, e.g., - Format: ’<score> your final scores here. Just write a single number here. </score> <exp> "validity": your sub-score for validity here explanation: your explanation for validity score here "completeness": your sub-score for completeness here explanation: your explanation for completeness score here "clarity": your sub-score for clarity here explanation: your explanation for clarity score here </exp>’
21