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

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.

## introduction mathematical proofs written in a formal language that computers can verify are known as formal proofs. these are primarily written in languages used by theorem proving assistants such as isabelle @xcite , rocq @xcite , and @xcite . autoformalization is a technology that automatically converts human-written proofs (natural language proofs) into formal proofs. it reduces the burden of manually formalizing mathematical theorems. moreover, in the domain of natural language theorem proving using large language models (llms) (e.g., @xcite @xcite , autoformalization enables us to programmatically verify the logical validity of generated content, thereby contributing to the improvement of automated theorem provers. in recent years, with the advancement of llms, research into autformalization as a machine translation task has become active (e.g., @xcite @xcite . however, challenges persist due to the lack of natural language proofs paired with formal proofs for model training. consequently, its target remains primarily on high school level mathematics, such as minif2f @xcite , where the emphasis is on arithmetic operations rather than mathematical reasoning. this paper proposes an auto-informalization method that translates formal proofs into natural language proofs, addressing the challenge of limited training data for autoformalization. to achieve this, we need to solve the following challenges: generation of natural reference expression mathematical proofs frequently refer to predefined concepts, theorems, and assumptions made in the course of a proof. in formal proofs, these references are made using arbitrarily named labels. however, simply using these labels during translation cannot produce natural reference expressions as those written by humans. abstraction to human-readable proofs it is possible to mechanically translate each piece of a formal proof into corresponding natural language expression, as all operations in formal language have clear meanings. however, a natural language proof constructed by mechanically translating and concatenating individual pieces often results in an unnatural and incomprehensible output. to achieve a natural translation, it is essential to include information that is both necessary and sufficient for human readers by an appropriate abstraction. to tackle the above problems, we combine the following three components: construction of a premise library our method performs translation using a premise library, which is created by converting definitions and propositions within a formal mathematics library (mathlib) into natural language descriptions in advance. these descriptions are included in the prompt for step-wise informalization to encourage the generation of natural reference expressions. ## related work this section introduces several recent studies on autoformalization and informalization that are particularly relevant to our research. @xcite proposed a method to construct a large-scale dataset of pairs of formal proposition and natural language proposition by informalizing formal propositions written in isabelle and lean using gpt-4. while our proposed method also involves prompt-based informalization, it differs from jiang et al.'s approach in that their method targets only formal propositions, whereas our research focuses on formal proofs. although prior work such as @xcite and @xcite has addressed the translation of formal proofs into natural language proofs, there has been relatively little research on approaches that utilize llms. @xcite proposed a method for constructing high-quality paired datasets of formal and natural language proofs. their approach uses static analysis tools to extract information such as code comments, similar propositions, and dependent propositions from lean's formal proof library, and then provides this information to the llm as auxiliary input to facilitate the translation of formal proofs. in addition, they aim for high-quality step-wise informalization and natural language proof generation by manually creating explanatory sentences for each tactic's logical structure and incorporating them into the prompt, thereby helping the llm capture the relationship between proof steps and goals. while our method is inspired by theirs, it differs in two ways. first, instead of guiding the llm with explanatory text, we directly control the form of step-wise informalization by applying rule-based template generation. second, whereas their method generates natural language proofs by concatenating step-wise results, our approach recursively summarizes these results according to the structure of the formal proof, producing text that is more readable and closer in style to human-written proofs. ## theorem proving assistant a theorem proving assistant refers to software that provides a formal language for writing mathematical proofs and an automated verification system for proofs written using that formal language. we explain the gist of lean's formal proof using the proposition "the sum of two even numbers is an even number" and its proof. a proof of this proposition is given as follows: if a and b are even numbers, then there exist some r 1 , r 2 such that @xmath0, @xmath1. this means that a + @xmath2. therefore, a + b is also an even number. figure 2 presents a formalization of this proof. in a lean formal proof, we first declare a proposition to prove using the theorem command. in figure 2 , it is declared that for any natural numbers a, b, if a and b are even, then a + b is also even (line 1-2). next, we introduce variables and hypotheses using the intro tactic (line 3). since even numbers are defined as even x ⇔ ∃r. @xmath3, the following hypotheses are introduced: r1 r2 : n, h1 : @xmath4, and h2 : @xmath5. the proof goal then becomes to prove even (a + b). we then declare a sub-proposition to be proven using the have tactic (line 4), namely that a + @xmath6. then, the proof goal temporarily changes from even (a + b) to a + @xmath7, while the hypotheses remain the same. the subsequent three rw tactics (line 5-8) rewrite on the proof goal using the propositions in the library and hypotheses. the first tactic rewrites (r1+r2)+(r1+r2) to r1+r1+ r2+r2 using the commutative and associative laws of addition. the next tactic rewrites a+b on the lefthand side of the goal using the two hypotheses h1 and h2 introduced by the intro tactic, and finally, by again using the associative law of addition, the left and right sides of the goal are made to have the same form, completing the proof of the subproposition. finally, the proof of the initially declared proposition is completed using the exact tactic (line 9). here, @xmath8, thus completing the proof. note that this given in the exact tactic refers to the proposition declared with the have command, which in this case refers to a + @xmath9. in lean, propositions are thus proven by repeatedly applying tactics and changing the state of the proof, i.e., the goal proposition and the established hypotheses. ## method our proposed method translates formal proofs written in lean 4 syntax into natural language proofs through five stages: off-line generation of premise library (4.1), information extraction (4.2), stepwise informalization (4.3), dependency structure analysis (4.4), and summarization (4.5). figure 1 provides an overview of the method. ## conclusion we proposed a natural language translation method for formal proofs by informalizing each proof step with template and premise library, and summarizing the result recursively, thereby generating human-readable natural language proofs. we applied the proposed method to formal proofs formalized according to university-level mathematical proofs and demonstrated that it can generate readable proofs that capture 86% of the key points. we also showed that the proposed method can generate high-quality natural language proofs from mathlib's formal proofs, i.e., even from those without corresponding natural language proofs.