# Herald: A Natural Language Annotated Lean 4 Dataset

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

## Key facts

- Cited by 59 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 16 of its 37 references that are in the map.
- First posted on arXiv 9 Oct 2024.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [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)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://mlsanity.com/paper/2402.06332/) (2024)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [A New Approach Towards Autoformalization](https://mlsanity.com/paper/2310.07957/) (2023)

## Built on by (most cited first, 30 of 59)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Evaluating Step-by-step Reasoning Traces: A Survey](https://mlsanity.com/paper/2502.12289/) (2025)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward](https://mlsanity.com/paper/2511.03108/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?](https://mlsanity.com/paper/2603.12744/) (2026)
- [Automated Formalization via Conceptual Retrieval-Augmented LLMs](https://mlsanity.com/paper/2508.06931/) (2025)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2506.08321/) (2025)
- [MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics](https://mlsanity.com/paper/2602.02561/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [FormalRx: Rectify and eXamine Semantic Failures in Autoformalization](https://mlsanity.com/paper/2607.04655/) (2026)
- [SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization](https://mlsanity.com/paper/2608.29270/) (2026)

## Abstract (arXiv)

Verifiable formal languages like Lean have profoundly impacted mathematical reasoning, particularly through the use of large language models (LLMs) for automated reasoning. A significant challenge in training LLMs for these formal languages is the lack of parallel datasets that align natural language with formal language proofs. To address this challenge, this paper introduces a novel framework for translating the Mathlib4 corpus (a unified library of mathematics in formal language Lean 4) into natural language. Building upon this, we employ a dual augmentation strategy that combines tactic-based and informal-based approaches, leveraging the Lean-jixia system, a Lean 4 analyzer. We present the results of this pipeline on Mathlib4 as Herald (Hierarchy and Retrieval-based Translated Lean Dataset). We also propose the Herald Translator, 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, outperforming InternLM2-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-world applications. As a direct application of Herald translator, we have successfully translated a template section in the Stack project, marking a notable progress in the automatic formalization of graduate-level mathematical literature. Our model, along with the datasets, are open-sourced to the public.