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等形式化系统要求明确表示每个证明状态及连接它们的策略。其次，每个非形式化推理步骤可视为证明状态间的抽象转换，但识别对应的形式化策略常需领域专业知识及对证明语境的精确控制。为弥合此差距，我们提出一个两阶段框架：不直接生成形式化策略，而是先提取状态链（CoS）——一组与非形式化论证逻辑结构对齐的中间形式化证明状态序列；随后生成在状态链相邻状态间转换的策略，从而构建完整形式化证明。该中间表示显著降低了策略生成的复杂性，并提升了与非形式化推理模式的契合度。我们构建了专用数据集与基准进行训练评估，并引入交互式框架以支持从形式化状态生成策略。实验结果表明，我们的方法显著优于现有基线，实现了更高的证明成功率。