# Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 17 references that are in the map.
- First posted on arXiv 10 Sep 2025.

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)

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

- [ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization](https://mlsanity.com/paper/2605.22885/) (2026)

## Abstract (arXiv)

This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and summarization capabilities of LLMs. For evaluation, it was applied to formal proof data created in accordance with natural language proofs taken from an undergraduate-level textbook, and the quality of the generated natural language proofs was analyzed in comparison with the original natural language proofs. Furthermore, we will demonstrate that this method can output highly readable and accurate natural language proofs by applying it to existing formal proof library of the Lean proof assistant.