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

Seiji Hattori, Takuya Matsuzaki, Makoto Fujiwara
9/10/2025
cs.CL

No confident code implementation found for this paper.

Abstract

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4

82% match2024

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

81% match2025

FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory

80% match2025

Steering LLMs for Formal Theorem Proving

80% match2025

Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving

79% match1 repo92024

Hilbert: Recursively Building Formal Proofs with Informal Reasoning

79% match2025

Cite this paper

@article{hattori2025natural,
  title  = {Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure},
  author = {Seiji Hattori and Takuya Matsuzaki and Makoto Fujiwara},
  year   = {2025},
  eprint = {2509.09726},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2509.09726v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2509.09726.svg)](https://codeofpaper.com/paper/2509.09726)

Discussion