We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach is grounded in two key insights. First, informal proofs tend to proceed via a sequence of logical transitions - often implications or equivalences - without explicitly specifying intermediate results or auxiliary lemmas. In contrast, formal systems like Lean require an explicit representation of each proof state and the tactics that connect them. Second, each informal reasoning step can be viewed as an abstract transformation between proof states, but identifying the corresponding formal tactics often requires nontrivial domain knowledge and precise control over proof context. To bridge this gap, we propose a two stage framework. Rather than generating formal tactics directly, we first extract a Chain of States (CoS), a sequence of intermediate formal proof states aligned with the logical structure of the informal argument. We then generate tactics to transition between adjacent states in the CoS, thereby constructing the full formal proof. This intermediate representation significantly reduces the complexity of tactic generation and improves alignment with informal reasoning patterns. We build dedicated datasets and benchmarks for training and evaluation, and introduce an interactive framework to support tactic generation from formal states. Empirical results show that our method substantially outperforms existing baselines, achieving higher proof success rates.

翻译：本文研究了在有限计算资源约束下，将自然语言表达的非形式化数学证明转化为Lean4形式化证明的问题。我们的方法基于两个关键洞见：首先，非形式化证明通常通过一系列逻辑转换（如蕴含或等价关系）推进，而无需明确指定中间结果或辅助引理；相比之下，Lean等形式化系统要求对每个证明状态及连接它们的策略进行显式表示。其次，每个非形式化推理步骤可视为证明状态间的抽象转换，但识别对应的形式化策略常需领域专业知识并对证明上下文进行精确控制。为弥合这一鸿沟，我们提出一个两阶段框架：不直接生成形式化策略，而是先提取状态链（Chain of States, CoS）——即与非形式化论证逻辑结构对齐的中间形式化证明状态序列；随后生成在状态链相邻状态间转换的策略，从而构建完整的形式化证明。该中间表示显著降低了策略生成的复杂度，并提升了与非形式化推理模式的契合度。我们构建了专用数据集与基准用于训练和评估，并引入交互式框架以支持从形式化状态生成策略。实验结果表明，本方法显著优于现有基线，实现了更高的证明成功率。