Abstract
Verifiable formal languages like Lean have profoundly impacted mathematicalreasoning, particularly through the use of large language models (LLMs) forautomated reasoning. A significant challenge in training LLMs for these formallanguages is the lack of parallel datasets that align natural language withformal language proofs. To address this challenge, this paper introduces anovel framework for translating the Mathlib4 corpus (a unified library ofmathematics in formal language Lean 4) into natural language. Building uponthis, we employ a dual augmentation strategy that combines tactic-based andinformal-based approaches, leveraging the Lean-jixia system, a Lean 4 analyzer.We present the results of this pipeline on Mathlib4 as Herald (Hierarchy andRetrieval-based Translated Lean Dataset). We also propose the HeraldTranslator, which is fine-tuned on Herald. Herald translator achieves a 93.2%accuracy (Pass@128) on formalizing statements in the miniF2F-test and a 22.5%accuracy on our internal graduate-level textbook dataset, outperformingInternLM2-Math-Plus-7B (74.0% and 7.5%) and TheoremLlama (50.1% and 4.0%).Furthermore, we propose a section-level translation framework for real-worldapplications. As a direct application of Herald translator, we havesuccessfully translated a template section in the Stack project, marking anotable progress in the automatic formalization of graduate-level mathematicalliterature. Our model, along with the datasets, are open-sourced to the public.