Formal proofs in theorem provers like Lean are machine-verifiable but difficult for humans to read. Translating them to natural language while preserving accuracy and readability is challenging, especially for multi-step proofs with complex dependency structures.

The method leverages LLM informalization (verbalization of formal proof steps) and recursive summarization along the proof structure. Individual proof steps are informalized into natural language, then the proof's dependency graph is traversed to recursively summarize sub-proofs into coherent narratives. A premise library and template system provide context for the informalization. The method is evaluated on formal proofs in Lean created from undergraduate textbook proofs.

With both template and premise library, the method achieves 89.05% correct translations, with 5.15% misinformation, 3.87% unnecessary mentions, and only 0.40% untranslated expressions. Without the premise library, correctness drops to 83.09%. The method produces highly readable natural language proofs that closely match the structure of original textbook proofs.