# Translating Informal Proofs into Formal Proofs Using a Chain of States

arXiv: https://arxiv.org/abs/2512.10317 · HTML: https://mlsanity.com/paper/2512.10317/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 33 references that are in the map.
- First posted on arXiv 11 Dec 2025.

## Builds on (most cited first, 25 of 25)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving](https://mlsanity.com/paper/2412.20735/) (2024)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)

## Built on by (most cited first, 3 of 3)

- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence](https://mlsanity.com/paper/2608.26310/) (2026)

## Abstract (arXiv)

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.