Although most of the automated theorem-proving 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 $\mathtt{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.

翻译：尽管大多数自动定理证明方法依赖于形式证明系统，但非形式定理证明更能契合大型语言模型在自然语言处理方面的优势。本研究识别出非形式定理证明的主要瓶颈在于缺乏洞察，即难以识别解决复杂问题所需的核心技术。为应对这一挑战，我们提出了一种新型框架，旨在培养这种关键推理能力，使大型语言模型能够进行洞察性推理。我们提出了$\mathtt{DeepInsightTheorem}$，这是一个分层数据集，通过显式提取核心技术和证明草图，以及最终证明，来结构化非形式证明。为充分利用该数据集，我们设计了一种渐进式多阶段SFT策略，模拟人类学习过程，引导模型从基础证明撰写走向洞察性思考。我们在具有挑战性的数学基准上的实验表明，这种洞察感知的生成策略显著优于基线方法。这些结果表明，教会模型识别并应用核心技术能够大幅提升其数学推理能力。