Herald: A Natural Language Annotated Lean 4 Dataset
Authors: Guoxiong Gao
Yutong Wang
Jiedong Jiang
Qi Gao
Zihan Qin
Tianyi Xu
Bin Dong
Venue: ICLR 2025 Poster (2025)
Keywords: Lean 4
Autoformalizing
LLM
Retrieval Augmented Generation
Dataset
Primary area: datasets and benchmarks

Abstract: 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 96.7\% accuracy (Pass@128) on formalizing statements in the miniF2F-test and a 23.5\% accuracy on our internal graduate-level textbook dataset, outperforming InternLM2-Math-Plus-7B (73.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.

Published as a conference paper at ICLR 2025
HERALD: A NATURAL LANGUAGE ANNOTATED LEAN 4 DATASET
Guoxiong Gao
Yutong Wang?*
Jiedong Jiang"
Qi Gao
Zihan Qin'
Tianyi Xu! Bin Dong 15t
!Peking University NNational University of Singapore CCetter for Data Science, Peking Uni- versity "Beijing International Center for Mathematical Research and the New Cornerstone Sci- ence Laboratory, Peking University *Center for Machine Learning Research, Peking University samggx@stu.pku.ee edu. en, e11247918 1t1991uu.mmm. mus edu emailboxofjjjlepku edu. Lthanggnnsttu.pku.ee. edw.ppuwweeddcoooom.oo cn, dongbinemath.pkuu edu.cc
.us.edu
qigēstu. pka.edus
xutianyi@hbi .wu. edu. on
ABSTRACT
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 dual augmentation strategy that combines tactic-based and informal- leveraging the Lean-jixia system, a Lean 4 analyzer. We present the results of this pipeline on Mathlib4 as Herald (Hierarchy and Retrieval-basee Translated Lean Dataset). We also propose the Herald Translator, which is fine-tuned on Herald. Herald translator achieves a 96.7% accuracy (Pass @ 128) on formalizing statements in the miniF2F-test and a 23.5% accuracy on our internal graduate- level textbook dataset, outperforming MieemLLM--Math-luuse
approaches,
(73.0% and 7.5%) and TheoremL.ama (50.1 1% and 4.0%). Furthermore, we propose a section-level translation framework for real-world applications. As direct application of Herald translator, we have successfully translated a template section in the Stack project, marking notable progress in the automatic formalization of grad mathemattcal literature. Our model, along with the datasets, are open open-sourced to the public |
Keywords: Lean 4, Autoformalizing, LLM, Retrieval Augmented Generation, Dataset
INTRODUCTION
In modern mathematics, the increasing complexity proofs has made peer review more difficult. Errors in proofs often go unnoticed for extended periods, as critical flaws are usually subtle and require expert scrutiny. As solution, formal mathematical languages, also known as Interactive Theorem Provers (ITP), such as HOL. Light (Harrison) 1996), Coq (Barras et al. 1999), Isabelle (Paulson 1994). and Lean (Moura & Ullrich| 2021). allow for automated verification of proofs, reducing the risk of human oversight.
However, writing proofs in these formal languages requires significant effort and expertise. Mathe- maticians must navigate through unfamiliar theorem libraries and often engage in repetitive tasks due
Equal contribution.
i Corresponding author.
'The model can be found at http:///wwgggnnnc..cooo///ttttts
The code of Herald and LeanSearch can be found at translatoo

---

Published as a conference paper at ICLR 2025
to the strict requirements of formal languages, which can be burdensome for those accustomed to writing high-level, natural language proofs.
This highlights the importance of autoformalization, which seeks to translate natural language (NL) reasoning into formal language (FL), with the reverse process referred to as autoinformalization. making 'natural' and 'informal' interchangeable in our text. Utilizing large language models (LLMs) a promising approach to this task, as LLMs can learn reasoning patterns from large corpora of natural language mathematics, apply them to NL-FL translation, and add necessary reasoning steps in formal logic.
However, the scarcity of parallel data between natural and formal languages, which consists of one-to-one pairs aligning natural language with its formal language counterpart, limits the progress of LLM-based translation approaches. To address this scarcity, existing works explore methods such as using LLMs to annotate Lean corpora (Wang et al. 2024) and Expert Iteration (Ying et al. 2024a Xin al. 2024a). Yet, these methods do not fully leverage the detailed structural information provided by the Lean 4 compiler and the pyramid architecture of the Lean repository.
In this work, we introduce Herald (Hierarchy and Retrieval-based Translated Lean Dataset), a dataset created by applying our augmentation pipeline to Mathlib4. During statement informalization, we provide the L.L with rich contextual information, especially theorem dependencies, and follow a hierarchical approach where dependent theorems are informalized before the target one, ensuring comprehensive natural language annotations. For proof informalization, we further enhance the LLM's understanding by offering term explanations for each translation step, supported by our NL-FL statement dataset. Additionally, we synthesize more formal statements by decomposing tactic-wise proofs into smaller steps, generating 580k valid statements from 1 110k original Mathlib4 theorems. We also utilize LLMs to generate NL counterparts for synthesized formal statements, further augmenting our NL-FL corpus.
Based on the Herald dataset, we fine-tuned model for NL-FL statement translation. To validate the generated formalized statements, we apply both Lean compiler and LLM back-translation checks. Our model achieves 96.7% accuracy on miniF2F-test (Zheng et al., 2022) and 23.5 23.5% accuracy on our internal graduate-level textbook dataset, outperforming InternL M lath-Plus-7B (Ying et al. 2024b) (73.0% and 7.5%) and TheoremL (Wang et al.) (2024) (55.0% and 4.0%).. To demonstrate the model's effectiveness autofornalization. we apply the Herald translator to section of the Stack Project (See Appendix F.I. using DeepSeek-Prover-VV
(Xin et al. 2024b) to complete the proofs.
In conclusion, our contributions are as follows:
aware pipeline for augmenting NL-FL datasets from any Lean project. The inclusion of additional context and a hierarchical process breaks down formalization into manageable steps, improving L.M performance and enabling formalization at the project level, rather than focusing on individual theorems or files.
We propose a
We present the Herald dataset, generated from our pipeline on Mathlib4, containing 580k valid statements and 44k NL-FL theorem pairs.
We release the Herald translator model, fine-tuned the Herald dataset, achieving 96.7% accuracy on miniF2F-test and 23.5% on our internal graduate- dataset, significantly outperforming MMemLLMM-MathhPluss (73.0% and 7.5%) and TheoremLlama (55.0% and 4.0%).
RELATED WORK
The field of auto-formalization has advanced notably with the integration of LLMs. Early efforts, like Wang et al. (2018), trained specialized neural models for statement fitooffommlizztion. Recent studies, including Wu al. (2022). Patel et al. (2023). and Zhou et al. (2024), employ LLMs with few-shot in-context learning, while Agrawal et al. (2022) introduces input-dependent fhot learning. Additionally, Azerbayev et al. (2023) and Diang al. (203a) fine-tune LLMs on natural language-formal language pairs to improve accuracy without in-context learning.
Auto-formalization
2

---

Published as a conference paper at ICLR 2025
(4) NL-FL Dulanet Gananation
LUU lnfernal
Mil onsamation
Dacaal GENL4L
Lovel Crta
H vil bxtedioo
Bih Tralo
LIN Uiiiemmater
Lean Valker
LAS Horra intariaiion
Shep sas
PoadFaax
(1) Nuto-tomaiizaton
Catument Pood
Hoddl Thandkrrr
Protfit M. Conrent
Figure I: Overview of our approach. (a) NL-FL Dataset Generation: We extract statements from Mathlib4 and informalize them by providing the LLM with rich contextual information, particularly dependent theorems, and proceed in dependency-level order ensure the LLM has access to all relevant natural language annotations. The same pipeline is applied to the proof corpus, aided by the NL-FL statement dataset generated in the previous step. Additionally, we augment the statement corpus in two ways: by breaking down tactic-wise proofs in Mathlib4. with results validated through the Lean compiler, and by using LLMS to generate equivalent NI. statements. (b) Autoformalization Pipeline: We train a statement formalizer on the Herald dataset. During formalization, FL statements are first generated by the Herald translator and then fed into powerful automatic theorem prover (e.g., DeepSeek Prover V1.5) to obtain the final formalized corpus.
Extending beyond statements, nutoo-formalzztioon of proofs presents more complex challenge. Jiang et al.] (2023b) and Xin et al.) (2024c) propose frameworks that use in-context learning to generate formal proof sketches from LLM-produced natural language proofs. These sketches are then complemented by auto-theorem- proovin tools such as sledgehammer Isabelle to fill any gaps. Wang et al. (2024) and [haoo et al. (2024) generate complete formal proofs with natural language in-line comments using fine-tume tuned LLMs, with Wang et al." (2024) also capable of translating both natural language statements and proofs.
NL-FL dataset generation The pursuit of auto-formalization faces significant challenges primarily due to the shortage of high-quality and high-quantity NL-FL pairs as training data. Current efforts in generating these pairs still face substantial limitations.
Several approaches (Jiang et al. 2023a Lin et al. 2024 Wang et al. 2024 Ying et al. 2024a) have recently attempted address this issue by leveraging LL generate NL.FF pairs. Specifically, MMA (Jiang et al.. (203a) uses L.MMs to generate 88K NL. statements, starting from formal statements extracted by the Lojo framework. Lean-STaR (Lin al. 2024) takes a different approach by generating NL 'proof thoughts' at each step of formal proof, producing 52,438 NL proof thoughts based on theorems in the LeanDojo library. TheoremLlama (Wang et al. 2024) enhances the process by introducing a bootstrapping technique where NL proofs are integrated into Lean4 code to create training dataset. Lean Workbook (Ying al.) 2024a) proposes a novel pipeline that iteratively generates and filters synthetic data to translate natural language mathematical problems (extracted from math contest forums) into Lean statements and vice versa.
Despite these efforts, the primary limitation of all the aforementioned methods lies in the intrinsic weaknesses LLMs when applied to mathematics and logical reasoning. As a result, the generated NL-FL pairs are prone to errors, which can propagate through datasets and impair the performance of models trained on them. In this paper, we introduce a novel Retrieval Augmented Generation (RAG) pipeline specifically designed to ensure both the accuracy and naturalness of the natural language generated from formal mathematical statements and make our dataset more reliable for training nuto-formalization models.
3

---

Published as a conference paper at ICLR 2025
3 METHODOLOGY
In this section, we outline our methodology for constructing and utilizing the Herald dataset to improve LLMs' ability to translate mathematical statements and proofs between NL and FL.. Our approach centers around generating high-quality NL-FL pairs from Mathlib4 through providing LLM with sufficient structural information, followed by strategic augmentation techniques address data scarcity and distribution imbalance. Section 3.J explains the generation process of NL-FL data, while Sections 3.2 and 3.3 describe our augmentation strategies and the training of our statement formalization model on the Herald dataset. These steps collectively contribute to enhancing the autoformalization performance of L.LMs within the Lean4 environment.
3.1 NL-FL DATA GENERATION
This subsection details the process behind creating the Herald dataset, a large-scale collection of NL- FL language pairs specifically designed to enhance the performance of LLMs in autoformalization. Using Mathlib4 our source of formal statements and proofs, apply RAG approach to produce high-quality natural language translations. The Herald dataset consists of 580k NL.FFL statement pairs and 45k NL-FL proof pairs, making it one of the largest resources for training models translating between natural and formal mathematical languages. This section describes the detailed extraction and augmentation methodologies that were employed construct this dataset.
3.1.1 STATEMENTS INFORMALIZATION
Structured Information and Contextual Augmentation The first step in our methodology in- volves extracting essential components from Lean code that encapsulate formal statements. We utilize Lean-Jixia] static analysis tool specifically designed for Lean to extract structured information from Mathlib4. Lean-Jixia parses Lean files to extract key metadata, including theorem declarations, proof structures, and dependency relationships. We select five main components enhance the FL to NL translation process: head statements, kind, docstrings, neighbor statements, and dependent theorems. These additional structures provide mathematical context and background information for the LLM, thereby reducing the burden on the LLM to infer the mathematical background indepen- dently. For an overview of each component, please refer to Appendix [B] By utilizing this information, the LLM can better understand the FL statement and follow the principles of NL statements when translating FL. statements into NI. statements.
Dependency Level and Translation Order We identify critical issue where the lack of natural language translations for dependent definitions often led to incorrectly fabricated translations of these dependencies, thereby affecting the translation of the original theorem. To address this, utilize Lean-Jixia to extract the dependency graph of all statements, forming a directed acyelic graph (DAG). We stratify all statements into levels based on their distance the root nodes, which statements not dependent on any others. Statements in each level only depend on those in lower levels. By translating statements in the level order, we ensure that the natural language translations of dependent theorems are available during the translation process, thereby providing missing dependent information that does not exist in the formal statements.
Retrieving Related Instances Following previous work (Gao et al. 2024) on the semantic search engine of Mathlib4, we identified the theorem most similar to the one to be translated through 1, 1,000 manually annotated examples. To elaborate, we represent the formal language of the manually annotated theorems as embeddings. The human-annotated theorem that is closest in distance to the theorem be translated in this embedding space is then placed in the instruction set of the LLM, thereby enhancing the quality of translation.
By calculating the proximity between the embedding of the theorem that requires translation and the embeddings of the annotated examples, we can effectively determine the most relevant precedent or analogous theorem.
Incorporating the closest matching theorems into the LLM''s instructions functions as a contextual anchor, which guides the model in understanding the specific mathematical domain and terminology
hhaps://gittuhh.o//esaaaa/// JinnJ
4

---

Published as a conference paper at ICLR 2025
Formal theorem:
theorem addorderdf did nattard Tyye") [AdoGroup 61
addDrderör Nat.ooadd
Retrieved Humer-Amndtated Examples:
ordarct _attaardddd Type*]
Human Annotated NL-FL Statement Pairs
Search Engine
orderOe Net.card
The order of an element in group divides the cardinaliy the group.
2. theoren Addbubrroup. cacd addoubgroug dvd card for Type")
[AddGroup of la AddBubg coup Kal-.cand Iu Naa. taed edditive subgroup divides
group.
Figure 2: Illustration of how related instances retrieved: NL-FL statement examples embedded and stored a vector database. The statement being informalized is treated as query and embedded by the same model, which designed to account for mathematical similarity. The vector database then retrieves a list of relevant theorems based on cosine similarity of the embeddings.
relevant to the new theorem. This context-aware guidance ensures that the LLM's translation maintains the technical precision and conceptual integrity of the original theorem.
Human Feedback Iteration Human feedback is integral to refining and improving the translation process. We collect feedback from five human experts, all PhD students pure mathematics with extensive expertise in Lean. These experts observe translation examples across various mathematical branches, identifying common issues the natural language translations. They summarize these issues into principles and illustrative examples, which then incorporated into the prompts used to guide the translation models. The iteration took place over six rounds of feedback and refinement, culminating in the development of over dozen principles. By integrating these principles into the prompts, we ensure that the translations align with the precise and concise language habits of human mathematicians.
3.1.2 PROOPS INFORMALIZATION
In the previous section, we detailed the methodology for generating NL-FL statement pairs from Mathlib4. This section extends our approach include the generation of NL-FL proof pairs, leveraging the same structure of principles and tools.
Stepwise Translation and Integration The initial step in generating NL-FL proof pairs involves extracting proof line information using Lean-Jixia. Lean 4 supports two styles of proof': tactic-based and term-based. A detailed comparison of these styles is provided in Appendix A Term-based proofs, though concise, often present a series of formal theorems without a clear expression of logical reasoning. This makes them less effective in enhancing LLMs' inference capabilities during training, as they lack the logical chain that aids comprehension. Therefore, we focus on extracting and translating tactic-hased proofs. We begin by translating each line of the formal proof into natural language. Once each line is translated, these individual translations are combined to form complete informal proof.
This approach allows us to supplement the formal proof with extensive Lean information that would otherwise be missing, such as the proof state before and after each proof step. This additional context helps the LLM understand how each proof step contributes to the overall proof, thereby enhancing the model's comprehension and the accuracy of the NL translations.
Structured Information for Proof Translation In addition to the structured information provided during the translation of statements, we further extract more detailed components for the translation of proofs and utilize the previous statement translation results. These additional components include: formal statement, informal statement, tactic information, and proof states. For an overview each component, please refer Appendix B

---

Published as a conference paper at ICLR 2025
Tactic Explanation A significant limitation of LLMs in translating mathematical proofs is their lack of understanding of the logical relationships between the proof steps and the goal. To address this issue, employ human annotation to explain the logical structure inherent in each type of tactic. By adding these detailed explanations of the logical structure into the prompts, we significantly enhance the logical coherence of the natural language translations of mathematical proofs.
3.2 AUGMENTATION
When training models on NL-FL pairs in the context of Lean two major challenges arise: Data Scarcity and Distribution Imbalance. The limited availability of NL-FL. pairs leads to model over fitting, while the deformalization process often produces informal statements that deviate from the natural distribution found in textbooks, resulting in rigid, repetitive, or overly precise content that hinders generalization.
To address these challenges, we introduce 2 innovative augmentation techniques designed to both expand the dataset, and align more closely with the real-world distribution of mathematical statements, proving to be highly effective in practice.
3.2.1 TACTIC-BASED AUGMENTATION
Natural language theorem proving presents a significant challenge due to the inherent complexity of proofs, where theorems are often established through the interplay various lemmas, techniques, and proof strategies. Learning the 'global' properties of theorems from such complex proofs is difficult because the entire structure is often too intricate for direct modeling. However, we observe that during the proof process, each proof step- coep-fften seetic-addressee smaller, localized 'statement', which simpler and more easily understood isolation. fact, each such local statement is fully captured by the prove state (or tactic state) in Lean's interactive prover. Given this insight, developed
Let Sa ci be the riewets on TinE Pt. 37 3
esaeail de typeel (hing (Nostristal #f
remple (Stng (Nentrietal the
a piant in
wuluome ruluanset, he.
b
Kire
Lean compling to led Type not proposition
thea)
alanancs
a 15, then there extst an stemett $t.15 thet is beth the camele (spea] [Reetrovtat 1) (he a b.d, bix
(editt-sotre (h, N0l3
a
Formal Proof
Extracted Proof State
Valdated NL-FL Statement Pair
Figure 3: Demonstration of Tactic Augmentation Strategy
augmentation strategy based on extracting prove states from Lean 4. Typically, the proof of theorem comprises of prove states tactic states. For each prove state, which contains the conditions and the goal at that specific proof step, we construct a new formal language statement.
This augmentation strategy (Figure ensures that each generated informal statement is aligned with a concrete, localized mathematical goal, making it both provable and semantically valid. In this way, from each proved theorem, we can generate multiple statements that is not only mathematically sound but also more straightforward and reflective of the structure found in real-world theorems.
Deduplication Nevertheless, in proofs involving many closely related tacties, consecutive tactic states can result in augmented statements that are highly similar to each other. Directly incorporating all of these similar statements into the training set risks overfitting the model. To address this, we randomly sample a subset of the augmented statements, equivalent in number to the original theorems, ensuring that the augmented dataset retains diversity and avoids excessive repetition of similar content.
3.2.2 AUGMENTATION VIA AATHENATTICS-PRETRAATTT LLM
Our second method (Figure 4 capitalizes on LLMs pre-trained on extensive mathematical corpora. To ensure that the augmented natural language statements maintain both semantic consistency and variability, we employ LLM pre-traie pre-trained on extensive mathematical data. This allows us to generate multiple equivalent informal statements for each formal statement.

---

Published as a conference paper at ICLR 2025
Asgumandatin Group?
of
Logical Equivalence
Asgumandation Group?
wll The wrin Y drripe
Original statement:
Cancept Sabutiztion
Fir ad the becaocic orto Yous draigs
positive number. The infnite sum of the sequence 1 convergent.
Asgimmntation Group 3
Teutbook Style
Asgimendation Group 4 BB 71E 8.5 (5RL WE
Multi-linguistic
Figure 4: Demonstration of LLM Informal Augmentation
We implement four specific augmentation strategies:
Logical Equivalence Rewriting For each formal statement, we generate several logically equiva- lent informal statements. For example, we might rewrite "If AA, then BB" as "BB holds given AA."
Abstract Concept Substitution In some cases, lengthy or detailed informal statements can be rephrased using more abstract or higher-level mathematical concepts. For example, the statement 'For given matrix A, there exists matrix B, such that AB = BA = I' would be replaced with more concise, abstract expression or concept like 'A non-degenerate'.
Omission of Implicit Condition In natural language mathematical discourse, particularly in textbooks and research papers, certain conditions are often omitted because they are considered obvious or conventionally understood by the reader. For example, a theorem might not explicitly mention the requirement that a function be continuous if that is implied by the context.
Multi-linguistic Translation We generate additional informal statements by translating the formal statements into Chinese, French and Russian. This results in a set of informal statements that represent how theorems might be articulated in different language.
This approach benefits from the LLM's ability to capture and reproduce the natural distribution of mathematical language, as it has been pre-trained vast amount of mathematical text.
In this way, our approach can be viewed as a resampling of the original dataset. Furthermore, after generating the augmented statements, again sample number of statements equivalent to the original theorems, ensuring that the augmented dataset remains representative of the natural language distribution in mathematical texts and avoids over-representation of any specifie phrasing style.
3.3 TRAINING STATEMENT FORMALIZING MODEL ON THE HERALD DATASET
After establishing the Herald dataset (Table T). we then perform Supervised Fine- Tine-Tunig (SFT) on pre-trained LLM using this combined dataset. Training on NL-FL datasets can enhance the LLM's ability to translate natural language mathematical propositions into Lean4 propositions. Mixing in an appropriate proportion general natural language data can prevent potential overfitting phenomena and catastrophic forgetting. This balanced approach ensures that the model maintains its general language understanding while developing specialized skills in formal mathematical translation.
Mathlib4 Original Statements
Augmented Statements
Mathlib4 Proofs
Number of NL-FL pairs
291k
580k
44k
Table 1: Statistics of Herald dataset and Mathlib4
7

---

Published as a conference paper at ICLR 2025
4 EXPERIMENTS
We conduct extensive experiments to evaluate the Herald dataset and translator. In Section we test the Herald translator three statement datasets from different topics and compare its performance with other formalization models. Section (.2ioon|422assee 4.2 the quality of the Herald dataset through expert inspection, while in Section 4.3 apply our autoformalization pipeline section of the Stack Project and analyze the results. Ablation study on the two augmentation methods is presented in Appendix
4.1
STATEMENT FORMALIZING MODEL
4.1.1
DATASET AND TRAINING
We selected SeepSeek-Prover V1.5-Base 7B as base model due its extensive training formal programming languages like Lean, which provides a strong foundation for formal reasoning tasks.
Our data preparation process involved several key steps ensure comprehensive and balanced dataset. We began by collecting 580k NL-FL pairs from the Herald dataset. From this, we cre- ated two datasets: one for translating informal to formal (NL-FL mathematical statements and another for the reverse direction (FL-NLL). This process yielded total of 1.16M examples. The distribution of examples followed 1:2:1 ratio among original statements, lactic-augmented data, and
data. To further enhance model performance and mitigate overfitting or catastrophic forgetting, we combined our NL-FFL and FL.+NL datasets with the OpenHermes2.55 dataset (Teknium) 2023). general-doman dataset. The final training data maintained 2:2:1 ratio among NL-FL, NL, and OpenHermes2.5 examples, respectively, for fine-tuning.
Our fine-tuning process consisted of two stages: first, we conducted 2000-step warm-up using the OpenHermes2.5 dataset, followed by training on the mixed dataset. We used a learning rate 4e-5 with cosine decay schedule across 5 training epochs.
4.1.2 VALIDATION PIPELINE
For validation, we adopt the pipeline from the Lean Workbook (Yin et al. 2024a), which includes several key steps:
1. Translation: Using our trained model to translate informal statements from the test set into formal statements.
2. Validation:
Using REPL (Read-Eval-Prins Loop) based framework verify that the translated Lean 4 statements are valid and pass compiler checks. This step ensures that our translations are syntactically correct Lean4.
3. Back-translation: For statements that pass the validation in step 2, used InternLM2- Math-Plus-7B to translate the formal statements back to natural language to assess the preservation of meaning.
4. NLI check: We use the DeepSeek Chat v2.5 model to compare the back-translated state- ments with the original informal statements, ensuring that our translations are mathematically accurate and preserve the intended meaning.
For a detailed discussion and case study of the validation pipeline's 's effects, especially the NLI check, please refer Appendix D We conducted human evaluations the auto-formalization results of ProofNet (Azerbayev et al, (222)). The results indicate that while the pipeline is not perfectly accurate for evaluating informal-ue formalll alignment, remains a common practice in the field and one the few practical approaches for large-scale automated evaluation at this time.
We perform 128 parallel translations and consider the translation successful any of these passes both the compiler check and the nil check. Our results will be shown in the next subsection.
4.1.3 RESULT
To evaluate the performance of our model, we conducted comprehensive tests comparing Herald with several models similar settings. Our test suite included diverse range of datasets:
8

---

Published as a conference paper at ICLR 2025
miniF2F
Model
Extract Theorem
College CoT
test
valid
TlaoremLlama
50.1% %
55.6%
4.0%
2.9%
InternLM2-MMth-PMM Plus-7B
73.0%
80.1%
7.5%
6.5%
-inttrtinstructt
28.2%
31.6%
3.6%
1.8%
Herald
96.7% %
96.3%
23.5 %
16.0% %
Table Performance comparison of different models across various datasets. The last two datasets (Extract Theorem and College CoT) are shuffled subsets of 200 samples each.
miniF2F (heng et al., 2022) A widely-used benchmark dataset for formal mathematics.
Extract Theorem A custom dataset compiled by extracting theorems from advanced undergraduate- level textbooks using OCR on scanned materials. It covers a wide range of mathemati- cal topics and includes multilingual content.
College CoT A curated dataset derived from digital mathematics resources across the internet, with content verified and filtered using a large language model (LLM) to ensure quality and relevance.
These datasets were carefully chosen to assess the models' capabilities across various levels of difficulty and categories of mathematics. For representative examples in the Extract Theorem and College CoT dataset, please refer to Appendix G
Note: For models lacking header generation capability, we manually added generic header. In cases where models couldn't 't output stable Lean statements, we truncated their generation to obtain maximal possible statement (derived from generated proof or Lean code) for testing purposes.
We present the main experimental results in Table From the table, we observe that the Herald translator achieves success rate of 96.3% on MiniF2F- Valid, 96.7% on MiniF2F-Test. 23.5% on Extract Theorem, and 16.0% on College COT, demonstrating significant improvement the MiniF2F dataset breakthrough on two new datasets, outperforming baselines. These results indicate that the Herald translator excels at formalizing natural language statements, particularly in challenging tasks and high-level mathematics. A case study the Herald translator's anto-formalization results presented in Appendix D
4.2 SUMMARY CASE STUDY HERALD QUALITY EXAMINATION
To assess the mathematical rigor and language style in the Herald dataset, we conducted several case studies. For comprehensive result, Appendix
In summary, the informal data in Herald demonstrates significant advantages in mathematical rigor and alignment with formal proofs. Lean-jixia extracts more complete Lean information (c.g., theorem names, variables), which aids in generating more precise theorem descriptions.
For statements, the relevant definitions expanded and explained in natural language, enhancing the connection between natural language mathematics and Mathlib4. The language style is natural, with the logic of the statement properly expressed in the translation. However, there are instances where notations and formulas are either well-written in commonly used mathematical forms or poorly copied from formal language. Translating more abstract and diagram-based theorems remains challenge.
The accuracy of statement translation contributes to the accuracy of proof translation. By starting with a stepwise translation, ensure that the LLM-generated proof faithfully reflects the proof strategy used the formal proof. Unlike a verbatim translation of each tactic's function, the proof connects these steps with logical reasoning. Formal theorems used in the proof also explained. The level detail in the translated proofs is closer to formal language rather than natural language. Similar to statements, some notations well-written, while others copied from formal language.

---

Published as a conference paper at ICLR 2025
4.3 AUTOFORMALLIZATION PRACTICE
To evaluate the performance of our Herald translator in real-world formalization tasks, we applied the proposed autoformalization pipeline (Figure (b)) to a section of the Stacks Project, using DeepSeck Prover 1.5 (Xin et al., 2024b) as the prover: The Stacks Project (Stacks Project Authors) (018)) is an open-source, collaborative online encyclopedia focused on modern algebraic geometry and related fields, making it an ideal test case for complex formalization challenges.
To demonstrate the capabilities of the Herald translator in auto-formalizing modern mathematics, we selected the Normal Extensions section (Stacks Project Authors, 2018 (Tag 09HL) from the Field Theory chapter of the Stacks Project. This section was successfully formalized into runnable Lean 4 source file, showcasing the effectiveness of our pipeline. For more details on the Stacks Project, see Appendix and for the formalized output, refer to Appendix
The generation was completed efficiently using 16-pass setting, with human checks revealing only two necessary theorem modifications: correcting the conclusion in two of the auto-formalized theorems, and removing unnecessary condition in one of them. Notably, the model demonstrated strong understanding of the content, achieving both mathematical and programming correctness. For prover configuration,
DeepSeek- Procck----re--ee VI.5-RL RMaxTS with 4 512 sample budget), which successfully proved only one two-line theorem relying on an existing lemma from Mathlib4. This highlights the need for more capable prover model handle advanced topics, a key focus of our future work.
5 CONCLUSIONS
In this paper, we present Herald, a crructural-informatte aware pipeline for generating rich NL-FL dataset from Lean projects, specifically Mathlib4. Our approach augments the traditional process by providing hierarchical, context-rich annotations, ensuring that dependencies are fully accounted for before translating target theorems. This methodology not only facilitates better natural language explanations but also breaks down complex formal proofs into more manageable components, improving the performance of LLMs in the formalization process.
We release the Herald dataset, which includes 580k valid statements and 44k NL-FL theorem pairs, providing significant resource for formalization research. Additionally, we fine-tuned statement formalizer on this dataset, which achieves state-of-the-an art accuracy- 96.7% on the miniF2F-test and 23.5% on graduate-level texthook dataser-substantte substantially outperforming existing baselines such as InternL.22-Maine MM2-MMth-Pluu-77 and TheoremL By applying our translator to section of the Stack Project and leveraging the DeepSeek Prover V1.5, we further demonstrate the practical viability of our approach in auto-formalization.
Our work contributes to the field in several ways: the development of scalable NL-FL dataset generation process that incorporates hierarchical dependencies, the introduction of the Herald dataset, and the release of nligh-performin translation model. These contributions mark significant step toward automating formalization tasks at project-wide scale, and we believe the methodologies and resources presented here will facilitate further advancements in the field of mathematical formalization and L.Ld- theorem proving.
6 ACKNOWLEDGEMENTS
This work is supported in part by the New Cornerstone Investigator Program and in part by Ubiquant.
REFERENCES
Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint 4rX1v:2211.07524, 2022.
Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. Proofnet: A benchmark for autofor- malizing and formally proving undergraduate-level mathematics problems. In Second MATH-AI Workshop, 2022.
10

---

Published as a conference paper at ICLR 2025
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and formally proving undergraduate- mathematics. arXiv preprint arXhv:2302.124333 2023.
Bruno Barras, Samuel Boutin, Cristina Comes,, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Sean-Christopha Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, 1999.
Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4, 2024.
wwtp://wwww....//..p/.p.....aaa 2203 1233.13310
John Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, 1996.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:231 .03755, 2023a.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representa- fions, 2023b.
Haohan Lin, Zhiqing Sun, Yiming Yang. and Sean Welleck. Lean-star: Learning to interleave thinking and proving, 2024. URL https::/ arxiv. org/ /ttp://400..00000.
The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
Leonardo de Moura and Sebastian Ullrich. The Lean theorem prover and programming language. In 28th International Conference Automated Deduction, 2021.
Ulf Norell. Dependently typed programming in agda. In Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI '09, pp. 1-2, New York, NY, USA, 2009. Association for Computing Machinery. ISBN 9781605584201. doi: 10.1145/1481861. 1481862. BRLLhttps:// doi orw.orgggoo 100. 1145/1411188 861 1481861448822
Nilay Patel, Jeffrey Flanigan, and Rahul Saha. new approach towards autoformalization. arXiv preprint 1r.10:231..07957, 2023.
Lawrence C Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
Zhihong Shao, Peiyi Wang, Qihao Zhu, Ruaxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. Math Pushing the limits of mathematical reasoning open language models. arXiv preprint arXiv:2402.03338 2024.
The Stacks Project Authors. Stacks Project. https::/ math. www.:aaathhhollaiaa.aaaam wwwwmoia......m edu 2018.
Teknium. Openhermes 2.5: An open dataset of synthetic data for generalist I1m assistants, 2023.
Philip Wadler. Propositions as types. Communications of the Acm, 58(11):75-88) 2015.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pp. 255-270. Springer, 2018
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang, Theoreml- lama: Transforming general- -prrpose llms into lean4 experts. arXiv preprint arXiv.2407.03203 2024.
Yuhuai Wu, Albert Qiaochu Jiang. Wenda Li. Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Proceedings of the 36th International Conference Neural Information Processing Systems, 2022.

---

Published as a conference paper at ICLR 2025
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prowee Advancing theorem proving in Ilms through large-scale synthetic data. arXiv preprint 14331 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover--l 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint 081.22400..0855, 2024b.
Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. LEGO-prover: Neural theorem proving with growing libraries. The Twelfth International Conference on Leurning Representations, 2024c.
Huaiyuan Ying. Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook:
A large-scale lean problem set formalized from natural language math problems, 2024a. URL https::/arxiv. org/
wwwggg/aa.... abs/ 2406 03847
Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong. Kuikun Liu, Ziyi Wang, et al. InternLMM-aate Open math large language models toward verifiable reasoning. arXiv preprint arXivv2402.0633: 2024b.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A cross-system benchmark for formal olympiad-lvvel mathematics. In The Tenth International Conference on Learning Representations, 2022.
Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinherger, and Yuhuai Wu. Don't ' trust: Verify- grroidiggounnnng Ilm quantitative reasoning with autoformalization. In The Twelfth International Conference Learning Representations, 2024.
12

---

Published as a conference paper at ICLR 2025
A INTRODUCTION TO FORMAL LANGUAGES
There various approaches and tools of formalized mathematics. Among them, type-theory based theorem provers are prominent. They include Lean (Moura & Ullrich] 2021). Coq (Barras et al.
1999). Agda (Norell 2009), Isabelle (Paulson 1994), and many others.
Type-theory based provers utilize Curry-Howard Isomorphism, or the Coppsition-ass-Type paradigm (Wadler 2015) encode mathematical statements as types. In this paradigm, proofs for statement P are no different from programmatic value of type P. The practice of writing mathematical proofs thus unified with the practice of programming.
Interactive theorem provers also have a distinct tactic mode, where the prover keeps track of currently available hypotheses and the goal be proved. A set of concise, mid- to high-level commands called tacties can be used to manipulate the state. When all goals are solved, the proof is considered to be complete and the prover automatically generates the low-level code. The tactics are often designed to reflect common patterns in natural language proofs, making it easier for the users to write and understand proofs.
Thus, in tactic mode, the user simply writes sequence of tactics to describe the steps (i.e., the tactic-based proof) required to prove the problem hand, rather than manually writing down the detailed term-based proofs.
Lean (Moura & Ulirich 2021) is an interactive, type-theory based prover. Lean is designed to be highly extensible via its metaprogramming capability, enabling Lean-Jixin to extract important metadata accurately and concisely.
Mathlib4 (mathlib Community 2020 is community-drin effort to build unified library of mathematics Lean 4. It has a substantial part of modern mathematics formalized. Hence it can act reliable source for LLMs learn research- mathematics.
Below a comparison of the two styles:
example (p q r Prop) ::p: AAAA
example (p q r PŁop) (h P A r) : A = := by reases with (bp, hg, hr) constructor exact hg constructor exact hp exact hr
r) : q A A == Antri h.right. intro hefe
right)
Figure 5: Term-based Proof
Figure 6: Tactic-based Proof
Tactic-based proofs are usually more informative and closer to natural language proofs. Besides, one has access to proof states in tactic mode, which contains valuable information to help the informalization process.
B STRUCTURED INFORMATION IN LEAN FOR RAG
Here, we provide a detailed explanation of each component of the structured information we provide to the LLM, which is used to enhance the FL to NL translation process in data generation. During proof translation, all structured information (excluding kind) for statements provided, along with additional components to further assist the LLM.
COMPONENTS FOR STATEMENT TRANSLATION
Head statements. These include foundational theorems. definitions, and other significant state- ments within the mathematical field relevant to the theorem. The extraction of head statements ensures that the context and background of the theorem well-understood by the L.M..
13

---

Published as a conference paper at ICLR 2025
Kind. The kind of statement, which be theorem, instance, definition. s structure, class, inductive, class Inductivde or opaque, provides essential infor- mation about the nature of the statement. This classification aids the LLM in applying appropriate translation strategies tailored to the specific type of mathematical entity being processed. Different prompts are employed for translating different kinds of statements, adapting to the varying language habits of mathematical statements.
Docstrings often contain NL explanations written by humans, which crucial for translating formal statements into more understandable language. The LLM is trained to leverage these docstrings effectively, ensuring that all relevant mathematical information is included while filtering out implementation notes that are not pertinent to the translation.
Neighbor statements in the Lean code, including those with similar names located within the same namespace or file, are indicative of related theorems or definitions. By considering these neighbor statements, the LLM can better understand the interconnectednesss of mathematical concepts and ensure that the translation reflects these relationships.
Dependent theorems. The inclusion of dependent theorems is crucial for maintaining the logical integrity of the translation. These theorems form the basis upon which the main theorem is built, and their inclusion ensures that the LLM can accurately reflect the proof"s logical flow and dependencies.
ADDITIONAL COMPONENTS FOR PROOF TRANSLATION
Formal Statement. The formal statement being proved.
Informal Statement. The informal translation of the formal statement generated by LLM provides a natural language overview. This natural language translation is precisely the result generated as described the previous section.
Tactic Information. Details about the tactics used, including their effect in proving the theorem and how they should be translated into natural language. This is provided for each proof step.
Proof States. Intermediate proof states presenting the current goal after using a tactic and how values of variables change by using the tactic, ensuring a comprehensive view of the proof's progression.
C ABLATION STUDY
In this section, we conduct an ablation study on the two augmentation methods. We trained 5 models on different composition of datasets. These training sets share the same "original" set which denotes the informal-forma pairs chosen from the translated Mathlib4 dataset, and we ablate the augmented datasets by adjusting different ratios between the "original" set and augmented statements to assess the effectiveness of our methods.
Dataset ratio
Dataset size
MiniF2F-test
ProofNet-valid
Extract-Theorem
1:0:0
145k
86.8%
50.0%
15.0%
1:1:1
435k
91.4%
68.3%
17.5%
1:2:0
435k
95.1%
74.7%
19.0%
1:2:1
580k
93.2%
78.6%
20.5%
1:2:1
1160k
96.7%
81.6%
23.5%
Table 3: Performance comparison of Herald translator trained on different size and composition of datasets across various datasets. Dataset ratio represents 'original tac aug inf aug', original denotes the informal-forma pairs chosen from the translated Mathlib4 dataset, tac aug refers to the tactic-based augmented statements, and inf _au corresponds to the informal augmented statements. The penultimate model is trained on NL-FF dataset, and the last model, our model in the main experiment, trained on NL-FL and FL-NL datasets.
14

---

Published as a conference paper at ICLR 2025
As shown in 3 augmentation methods effectively enhance model performance, particularly on more challenging datasets such as ProofNet. The model trained solely on the original informal- formal pairs (1:0:0) achieves a respectable aceuracy of 50.0% the ProofNet- validd dataset, 86.8% on the MiniF2F-test dataset, and 15.0% on the Extract- Exxract-Thheoren Theorrm dataset, which underscores the quality of the informalized Mathlib4 dataset.
The introduction of augmented datasets significantly boosts model performance across all datasets. The model trained with 1:1:1 ratio shows a notable improvement, achieving 68.3% on ProofNet- valid, 91.4% on MiniF2F-test, and 17.5% on Extract-Theoremt The 1:2:0 ratio model, which includes more tactic-based augmented statements, further enhances performance, reaching 74.7% on ProofNet-valid, 95. 1% on MiniF2F-test,, and 19.0% on Extract-Thhoree The model trained with 1:2:1 ratio on both NI,+FI. and FI.-NII datasets outperforms the model trained with 1:2:1 ratio on only NL datasets, with accuracies of 81.6% on ProofNet-valid, 96.7% 76.7% on MiniF2F-test, and 23.5% on Therre.. This result indicates that increasing the size of the training set, while maintaining a balanced augmentation ratio, leads to substantial improvements in model performance, especially on more challenging datasets.
D DISCUSSION AND CASE STUDY FOR VALIDATION PIPELINE
In this section, we discuss the soundness and fairness of our validation pipeline and analyze examples of passing and failing the validation pipeline.
DISCUSSION
It is important to note that even the strictest LLM NLI checking introduces false positives. The NLI check consists of two steps: back translation and semantic comparison. During back translation, LLMs are less capable than humans at detecting subtleties in formalized statements, such filling back opened namespaces and disambiguating overloading notations. This may result in errors in back translation. During semantic comparison, the LLM may fail decide correctly due to a lack of mathematical understanding and the various possibilities of stating mathematics in neutral language. Consequently, formalized results passing the NLI check may fail reflect the mathematical meaning of the original natural language statement (i.e., false positives). Therefore, NLJ checking is not as reliable as human expert evaluation.
However, while NLI checking is not perfectly accurate for evaluating informal-to-fone it remains a common practice in the field (e.g.. see Ying al. (0024)) and one of the few practical approaches for large-scale automated evaluation at this time. It is not practical to apply human evaluation dataset with more than 1k formalization results, It is also worth noting that NLI check may introduce false negatives, i.e., results rejected by the NLI check that are actually correct.
alignment,
For our application of the NLI checking pipeline, the most important goal create a fair perfor- mance test between different models. As we will see in the following experiments, both the baseline model and our model achieve similar results in terms of the proportion of false-positive cases.
To provide more illustrative result on false positive cases and fairness mentioned in the above discussion, we conducted an experiment to evaluate the results passing the validation pipeline.
EXPERIMENT RESULTS
We choose the ProofNet dataset to conduct our experiment. The ProofNet dataset consists of problems drawn from popular undergraduate mathematics textbooks, selected based on the following criteria: self-containment, ease formalization, and low risk of train-test overlap.
We perform 128 parallel translations of the ProofNet validation set (with 185 natural language statements) using the validation accepted if any of these passes both the compiler check and the nil check and we only collect the first passed formalization for human evaluation.
and Herald model. The translation is considered as
The validation-passed auto-forman ootalioomaiiztiion outcomes are categorized by human experts into three distinct groups: correct translations, minor errors, and major errors. A correct translation must accurately reflect the mathematical meaning of the natural language statement. In cases where the original statement is ambiguous, we allow the formalized statement to adopt any mathematically valid interpretation. If the formalized result deviates from the original statement but can be easily
15

---

Published as a conference paper at ICLR 2025
corrected by altering single formal definition restructuring single logical relation within the hypothesis or statement, it is classified as a minor error. All other cases are classified as major errors. In section D.I. we will present examples of these three categories.
Model
Validation Passed
Correct Translation
Minor Error
Major Error
InternL Math-Plls-771 Plus-7B
72
42
12
18
Herald
151
101
24
26
Table 4: Human evaluation results of validation passed statements.
As shown in Table 4 other baseline models also suffer from false positives, with comparable false positive rates, making the comparison fair.
For more thorough inspection, in subsection D.2 we will present examples that are rejected by the Lean validation step and the NLI validation step. For false negative cases, given the substantial number of translation attempts, it is impractical to manually detect all such cases. Therefore, we will only provide one example in subsection D.2.3
During the evaluation process, we also identified some potential mathematical inaccuracies or inaccurately truncated problems within the ProofNet dataset, which are detailed in Appendix D.3
D.1 RESULTS ACCEPTED BY THE VALIDATION PIPELINE
D.1.1 CORRECT TRANSLATION
Rudin 3ex2rcise___00
INFORMAL STATEMENT
Suppose {pm} } is Cauchy sequence in metric space X, and some sequence {pni} converges to point p E X. Prove that the full sequence }pn} converges to
GENERATED FORMAL STATEMENT
import Mathlib
open Filter
open Topology Filter
theorem full fu oww.osuussuueeeeeeeeeeeeeeee (X Type*)
[MetricSpace X] {p
: X) (s N + x) (hs CauchySeq s) (1 N N) (hl Tendsto at atTop]
(hpl Tendsto (s 1) atTop N p) Tendsto atTop N p) := sorry
ANALYSIS
This an example where Herald translator correctly translated the subtle condition "some sequence {pmr)" 1 in natural language. To be subsequence, the index nıl must tend to infinity, which reflected the condition (h1 : Tendsto 1 atTop atTop).
Axler exercise 12
INFORMAL STATEMENT
Suppose T E L(V) is such that every vector in V is eigenvector 7' Prove that T' is scalar multiple the identity operator.
GENERATED FORMAL STATEMENT
16

---

Published as a conference paper at ICLR 2025
import Mathlib
open LinearMap
open Submodule
--Ne are to prove that every vector is an eigenvector, then a scalar multiple of identity
theorem isEigenvector_spe (V Type*) [AddConnGroup V] [Field K]
[Module K v]
V + +[K] V) (h v V, E : K,
3 K, 4
: V, k v = = == by sorry
ANALYSIS
In this example, the formalized condition (h V v, k k. for "every vector in V is an eigenvector" and the formalized result k K, v V, k v v for "T is scalar multiple of the identity opera- tor" differ only in the order of quantifiers. The Herald translator handled this difference in the order of quantifiers appropriately.
v)
=
D.1.2 MINOR ERROR
Freland-Rosed exercise_
INFORMAL STATEMENT
Show that 1729 is the smallest positive integer expressible as the sum of two different integral cubes in ways.
GENERATED FORMAL STATEMENT
import Mathlib open Finset
theorem smallest two way sum of cubes 1729 IsLeast in N 3 b d E, # a b"3 o d'3 A
a 33 1729 := sorry
ANALYSIS
In natural language, treat 1729 a 63 and 1729 b3 + a as the same cube decomposition. Therefore, the condition a * is not sufficient to guarantee two distinct cube decompositions.
Rudin eexeeeeeeeee se_1_19
INFORMAL STATEMENT
Suppose a, R* Find E R and such that [ 2|x b) if and only [x -c
Prove that 3c 4b and 3r = 2 a).
GENERATED FORMAL STATEMENT
import Mathlib open Topology Filter Set
19 theorem problem 1_99 (a
b
R)
R,
1x al 2.
1x + 1x
cl
b
2 lb
by sorry
ANALYSIS
17

---

Published as a conference paper at ICLR 2025
There is logical flaw in the formalized statement. The formalized statement is equivalent to saying that if 3c = 4b a and 3r = 2 al. then r and c satisfy the previous conditions. However, the converse direction, namely that any and satisfying the previous conditions must also satisfy 3c 4b - and 3r = 2|b - al. is not translated.
D.1.3 MAJOR ERROR
Dummit-Foom
INFORMAL STATEMENT
Prove that x²2 x² is irreducible in Q(2r,))
GENERATED FORMAL STATEMENT
import Mathlib
open Ideal Ideal. Quetient Finset
theorem irreducible pow tww_two tto__ttw_______ee_eo add ___oo__wo_____ www__uub_oet Irreducible 2 Y
Polynomial Q) := sorry
ANALYSIS
This is major error that difficult to detect. Lean can automatically deduce the type of variables x Y Q-coefficient polynomials, allowing this statement to pass the Lean check. However, we intended X Y to be the special generators the ring polynomials (also the ring polynomials in two variables instead of one). This is indeed an incorrect formal statement.
Dummit Commit-Footer lexercisee serccisse_st 1eteercieee_______
INFORMAL STATEMENT
Prove that if H/ is nontrivial normal subgroup of the solvable group G then there is nontrivial subgroup of with < G and abelian.
GENERATED FORMAL STATEMENT
import Mathlib
section exercise_3_4
--Prove that if $H$ is nontrivial normal subgroup of the solvable
group $GS then there nontrivial subgroup SAS of SH$ with lunihd GS and SA$ abelian.
-e will use the fact that group of order $p_1 $p_1"(e_ [ Vodots p_ ke has nontrivial subgroup of order $p_ ie_ where $ ps are primes and $e 05.
--we proceed by induction on the derived series of ses.
--If $G$ is abelian, then itself is a nontrivial normal subgroup of itself, and we can take $A GS.
--If SG$ is nonabelian, then $G$ has nontrivial normal subgroup $H$ of its center $2 (G) by lemma
--By induction hypothesis, $5$ has a nontrivial abelian subgroup $as of it.
-ininee $A \leq H$ and (leg (6) 8, have 1leg ( $.
18

---

Published as a conference paper at ICLR 2025
-ince \leq & and Yunlhd 68, we have $4 Yunlhd GS.
-TThus, we have found nontrivial abolian subgroup SAS of sGe with $A tunlhd GS.
--Now, we need to show that SA$ is nontrivial.
--If $A$ is triviai, then SA$ is cyelic group of order $0s.
--However, this contradicts the fact that subgroup of SHS, which is nontrivial group.
-Thus, $A$ must be nontrivial.
end exercise_3_44
ANALYSIS
We present this extremely unusual bad output here. This is the only output that did write single line of Lean code with mathematical meaning. All the outputs are written in Lean comments (thus containing no errors and passing the Lean check). The comments are indeed related the original problem, thereby circumventing the NLI check.
D.2 RESULTS REJECTED BY THE VALIDATION PIPELINE
The following examples are collected from all 128 formalization attempts of a statement. Therefore, there are multiple outputs corresponding one single informal statement.
D.2.1
EXAMPLES REJECTED BY LEAN CHECK
Munkres exercise_32_1
INFORMAL STATEMENT
Show that a closed subspace of a normal space is normal.
GENERATED FORMAL STATEMENT
import Mathlib
open Set Filter Function Topology List
theorem "itormaa_subsppce__t isclossed (X Type*) [Topol ogi ca Space X]
[NormalSpaal Space X] Set (hS IsClosed S) @Normalspace
by sorry
ANALYSIS
The formal statement uses @Normalppace but does not provide sufficient explicit arguments.
GENERATED FORMAL STATEMENT
import Mathlib
open Set Pi Pilter Function Topology
theorem isNormal subspace of normalSpace (t [NormalSpace XI (S : Set X) (hS IsClosed S) IsNormal :- sorry
Topologicallpace X]
ANALYSIS
The predicate IsNormal does not exist in Mathlib. This is model-crrated predicate.
19

---

Published as a conference paper at ICLR 2025
D.2.2 EXAMPLES REJECTED BY NLI CHECK
Munkres exercise_32_1
INFORMAL STATEMENT
Show that a closed subspace of a normal space is normal.
GENERATED FORMAL STATEMENT
import Mathlib
open Set Filter Function Topology List
theorem munkres_32_1 (x Type*) ["opologicallppaee X] {5 NormalSpace X] (T Set S) (hT IsClosed T)
NormalSpace S := sorry
BACK TRANSLATION
Let X be topological space; let S be subspace of X. Suppose that X is normal. Show that $ normal.
NLI OUTPUT
Upon examining the two problems, find the following differences:
** "Scope of the Subspace**:
**Prblem 1*0; Specifies that the subspace must be člosed:
**Problem 2* Does not specify any conditions on the subspace S other than being a subspace of X.
These differences indicate that the problems are asking for different proofs or considerations due to the condition of the subspace in each problem.
different
ANALYSIS
The NLI check identifies that the condition S' is closed is missing, thereby rejecting the translation. Note that during the back translation, the unused variable T is automatically dropped.
GENERATED FORMAL STATEMENT 2
mport Mathlib
open Set Filter Function Topology List
theorem munkres_32_1 (Y Type*) [Topologi cal Space X]
[Topol ogi ca Space
[NormalSpace X| ( Y + (hf Continuous : NormalSpace := sorry
BACK TRANSLATION 2
Let X and Y be topological spaces; let S be closed subset of X. Suppose that X is normal (or TT). and that Y is normal (or T.). Let ff be continuous map S into Y. Prove that S is normal (or T.).".
NLI OUTPUT 2
20

---

Published as a conference paper at ICLR 2025
Let's analyze the statements in each problem:
**Probemm 1:*
Statement 1: A closed subspace of normal space is normal.
**roblem 2:**
Statement 1: Let X be normal space.
Statement 2: Let be a metric space.
Statement 3: If Y X is continuous mapping, then Y is normal space.
Comparing the statements:
Problem focuses the property of closed subspace within normal space, asserting that such a subspace is also normal.
Problem introduces normal space X and metric space Y, and discusses the implications of a continuous mapping from to on the normality of Y.
The statements in the two problems different because Problem deals with the normality of subspaces, while Problem 2 deals with the effect continuous mapping on the normality of space.
different
ANALYSIS
The NLJI check identifies the wrongly added information about Y and f and rejects the formal statement. However, note that the back translation is correct, but the analysis of statement in the NLI output is not accurate. The condition that Y is a metric space is never mentioned in the back translation.
D.2.3 A FALSE NEGATIVE EXAMPLE
Munkres exereise_32 seeeiie_______ 2b
INFORMAL STATEMENT
Show that if [[ is regular, then so Xa. Assume that each X, nonempty.
GENERATED FORMAL STATEMENT
import Mathlib
open Set Function Filter Topologe cal Space
open scoped Topology
theorem reqularSpace of product produutt_reulaaappcee Type*] IV i, TopologicalSpace (X ill
Type*) (X : [' i, Nonempty (x i)] (h RegularSpace (II i, x 1)) ; V i,
RegularSpace (X i) : sorry
BACK TRANSLATION
Let X; be regular space for each i J. Prove that the product space Π X; is regular.
In this example, the Herald translator accurately formalized the statement. The logic the informal statement and the generated formal statement is the same: the product space being regular implies each component being regular. However, the back translation is incorrect, reversing the order of the implication. This results in failed NI.I check.
21

---

Published as a conference paper at ICLR 2025
D.3 POSSIBLE INACCURACIES IN THE PROOFNET DATASET
Here, we present some of the potential inaccuracies identified in the ProofNet validation set during human expert evaluation. We only focus on inaccuracies that affect the meaning or validity of the statements, and we do not include typographical errors in this list.
Axler exercise_6_1
Suppose U subspace of V. Prove that U+ [0} if and only if -
In general, this statement does not hold. To make it valid, it suffices to add one of the following conditions:
(I) V is finie-dimenniional,
(2) U is fiiit-ddimeniional or
(3) U is closed subspace of V.
Putnaa exercise_1999.
Let f be real function the real line with continuous third derivative. Prove that there exists point a such that
This statement is truncated at inappropriate point.
Rudin eeeeriise___00
Let E be bounded set Rt Prove that there exists real function f such that f is uniformly continuous and is not bounded on E.
This statement is mathematically wrong. A uniformly continuous function defined on bounded subset always bounded.
Axler exercise_l_3
Prove that ((-v) for every V.
This statement lacks proper condition V. making it too ambiguous. Without specifying the nature of V, one could assume to be an additive group. vector space, or any other algebraic structure.
E CASE STUDY OF HERALD DATASET
In the following sections, we will first analyze examples of original statements, followed by the proofs, and conclude with the augmented statements. In sections E.] and E.2 focusing on original statements and proofs, we will conduct comparative analysis of the Open Bootstrapped Theorems (OBT) dataset in Wang et al. (2024) and our Herald dataset. By examining multiple representative examples from both datasets, alignment of natural language and formal language. Through this examination, we seek to highlight the unique contributions of Herald while also identifying areas where further improvement may be necessary. In section B.3 focusing augmented statements, will compare these augmented statements with the original ones to illustrate the effect of each augmentation technique.
aim exhibit the differences arising from how each handles the
Please note that in the Herald dataset, the stepwise natural language proof is generated first and then summarized into a natural language whole proof. contrast, in the OBT dataset, the informal statement and proof are first created, which subsequently distributed into inline comments to form the commented proof. Additionally, due to the rapid updates in Mathlib, some formal statements and proofs may differ slightly between these two datasets.
22

---

Published as a conference paper at ICLR 2025
If a translation includes MTEX formula, format it using MIEX and may make minor adjustments for formatting purposes only, without altering any content. If the translation does not contain a ЕТЕX formula, we present it in plain text.
E.I EXAMPLES OF ORIGINAL STATEMENTS
In this subsection, examine examples of original statements, each containing five components: the formal name, Herald formal statement, Herald informal statement, OBT formal statement, and OBT informal statement. Following these data, comparison analysis is presented. Please note that the OBT informal statement is cut out from the generated informal statement and proof.
E.1.1
STATEMENT EXAMPLE
FORMAL NAME
dite_eq_or_eg
HERALD FORMAL STATEMENT
V la Sort 1_ (P Prop) [inst Decidable P] (A : P + at (2
-P
a), (3 h, dite P B A h, dite P h
HERALD INFORMAL STATEMENT
Dependent If- If-Then-Else Equals One of the Branches: For any type a, any proposition P. and functions, then the dependent
any decidable instance of P. if A: P + and B -P > if-then-else construct 'dite P A B' is equal to either A(h) for some proof h of P. or B(h) for some proof of -P. In other words, the value of dite P A B' is either the value of when true, the value of B when P is false
OBT FORMAL STATEMENT
theorem dite_ee_or_eq ( h, dite A A h) V h, dite P A
OBT INFORMAL STATEMENT
For any propositions "P", "A", and "B", the value of "dite 2 A B" is either "A" "B", Prove this by cases. Show that either there exists "h" such that "dite such that 'dite P PAB h
or there exists an
ANALYSIS
dite is shorthand for 'dependent if-then-else" in Lean. unreasonable expect the LLM to accurately interpret dite without referring to its definition. In the OBT dataset, dite is treated as black box without any explanation. In contrast, the Herald dataset correctly expands the meaning of dite with the aid of dependency information. This further enables the LLM to recognize that h is proof P and translate 'h,,' into 'when P is true,' which aligns more closely with natural language.
E. STATEMENT EXAMPLE
FORMAL NAME
Comgruenceeuubrroppp Gawmaaaemaaaaaaaaaaaaaaaa otw.:easttgrroppr.mmmmaaaaaraaar
HERALD FORMAL STATEMENT
Congruencoesubgrouppp Gamma
1
23

---

Published as a conference paper at ICLR 2025
HERALD INFORMAL STATEMENT
The full level congruence subgroup of SL(2, 2), denoted by r(0), is equal to trivial subgroup, i.e., [(0) = (1).
OBT FORMAL STATEMENT
theorem Lamma__ero__aae Gamma
OBT INFORMAL STATEMENT
Given the group homomorphism Gamma Z + Mat x 2Z, where
r(k) = k:
show that r(()) = bot.
ANALYSIS
This theorem is about the definition of the congruence subgroup [(n) C SL2(Z), stating that ((0) the trivial subgroup. the OBT dataset, this theorem extracted under the formal name Gamma_ zero_ _er__eerrrbbooeeeee Using Lean-jixia, the Herald dataset extracts the theorem with its full name. Additionally, note the difference between Gamma the formal statement of the OBT dataset and CongruenceSubgrrogg Gamma in the formal statement of Herald. These distinctions aid the LLM correctly deducing that Gamma refers to the congruence subgroup. Please note that in the original OBT data, the ETEX formula is Gamma Z - Mat x 2Z instead of T Z - Mataxa (Z).
E.1.3 STATEMENT EXAMPLE
FORMAL NAME
Set www.:peeiiaeeccosstttoooo
HERALD FORMAL STATEMENT
la Type 11 linst OrdereedddaCommGroou a1l (a b a a), (fun =>
Set.Ico Set. Ico (b (c a)
HERALD INFORMAL STATEMENT
For any elements a, b, in an ordered additive commutative group a, the preimage of the left- closed right-open interval [b, under the function f(x)
is the left-closed right-open interval 66 a). Formally, this can be written as:
(f(z) = a + x) preimage (b, c) = [b - a, c a)
OBT FORMAL STATEMENT
theorem preimage const add Ico (Fun =>
x)
-1,
Ico (b Ico b
a) (c a) :=
OBT INFORMAL STATEMENT
What is the image of Ico(b, c) under the map x a + Show that it is Ico(b a, a).
24

---

Published as a conference paper at ICLR 2025
ANALYSIS
This theorem asserts that the preimage of the left-closed right-open interval [b, c) under the addition by map is preciscly the left-closed right-open interval a, - a). In the natural language statement of Herald, Ico is correctly translated as the natural language left-closed right-open interval and is represented by the commonly used LTTEX notation [b, c), emphasized in of the human-writter principles provided to the LLM.
Additionally, note the difference in the variables in the formal statements in the two datasets: [inst Ordere www.ddeoddroooooooeoeoo jixia provide the precise and broad setup of the theorem.
o:) and (a bo a) The variables extracted by Lean-
One advantage of the OBT dataset is that it occasionally translates statements into natural language questions, such as 'What is the image of ...?' This offers examples of how formalize questions natural language.
E.1.4 STATEMENT EXAMPLE
FORMAL NAME
CategoryTheary. Abell Aabelian.ee htt.:///we.........ooooooooooooo
HERALD FORMAL STATEMENT
1C : Type 1_ linst CateposyTheory.Cateeo. (u_2, 1 C] [inst_
: CategoryTheory, Abelian C]
(R1 Ra
C 3) (p Rı - Ra),
Rx.Exact
R2 Exact +
CategoryTheery.Ep (Ctrepry/heeryycoooppatlllaaorr
yp ...)
CategoryTheory Mono
Mono (Crtepry/herryyccmppbbbabbrooo.
CategoryTheory Mono
(
m) +
2 Categorylheory. Mono (eatepoyylleryyyoopoaaaaaarrrrrr
HERALD INFORMAL STATEMENT
Consider a commutative diagram with exact rows in an abelian category C:
1
A
B
C
D
E
4
3
$
F
A'
B
C²
D
E'
If the morphisms a are epimorphisms, and | and 8 are monomorphisms, then the morphism is monomorphism.
OBT FORMAL STATEMENT
theorem mono_of_ _ono_of_epl__ Mono 8) Mono :
(ha : Epi or) (h,8 : Mono () (hō :
OBT INFORMAL STATEMENT
* **Thoormm ** If we have three mappings a:A-:B, B:B-&C, and B:C-&D such that a is an epimorphism, 3 is monomorphism, and is monomorphism, then defined via 7=(808)oa, monomorphic.
25

---

Published as a conference paper at ICLR 2025
ANALYSIS
The above theorem is elementary and widely used in homological algebra and abelian categories. commonly referred the 'four lemma'. Given commutative diagram in abelian category. where both rows are exact sequences:
A
B
C
} D
E
1
0
0
7 C²
4
A'
B'
E'
If the morphism is epimorphism and the morphisms 3 and 6 are monomorphisms, then the morphism y is a monomorphism. The translation the OBT dataset misinterprets the setup, whereas the statement is correctly translated in Herald.
This is rare example of a high-quality translation of complex category theory theorem in Herald. Thanks to the detailed head statements written in the Lean file, the LLM correctly understands the complex diagram and even generates its own commutative diagram in 18T]X.
Category theory is renowned for its abstract nature, and many theorems naturally expressed using commutative diagrams. Unfortunately, most category theory theorems are not as well-documented this one. The LLM's performance in category theory, particularly in the task of informalizing category theory theorems, is far from satisfactory. Accurately auto-translating such abstract and diagram-basee based theorems remains significant challenge.
E.2 EXAMPLES PROOPS
In this section, we examine examples of proofs, each containing five components: the formal statement, Herald stepwise proof, Herald whole proof, OBT commented proof, and OBT generated informal statement and proof. Following these data, comparison analysis is presented.
E.2.1
PROOF EXAMPLE
FORMAL STATEMENT
theorem Complex. hasDerivAt_exp (x Ccomplex.exp x)
C) HasDerivvt Complex exp
HERALD STEPWISE PROOF
To show that the complex exponential function exp has the derivative exp(x) suffices to show that the function h + exp(x + h) -xx(xx) - h h exx((z) is o(h) as h approaches 0. In other words, we need to show:
exp(x h) exp(x) h exp(x) o(h)
as h tends to 0 in the neighborhood filter of O.
[hasDerivAt iff [e___ssittlee__heee zero]
We first establish the simple fact that < 2 by direct calculation.
have (1 N)
by norm_num
To show that exp(x + exp(x: h exp(x) o(h), the transitivity of big-O and little-o notation. Specifically, we need to show that:
exp(( + h) - exp(xx) - h exp(x)) S [xp(x))] 1|
26

---

Published as a conference paper at ICLR 2025
for h in neighborhood of 0. This will imply that exp(x + h) exp(x) exp(x) is O(h?),
and since 112 o(h) as h 0, it follows that exp(x h) exp(x) - h exp(x) dhi).
refine (IsBigo.of_boun I exxp xl| ?_) trras__isLittlee (istittleo_pow_ic this)
We restrict attention to the open ball B(0, 1) centered 0 with radius which is neighborhood of O. This means we only need to show the inequality for such that |/]]] < 1.
filter_upwards [Metric. 1am_m_m_mmmmmmme atttrric..allmmm_nhhhe (0
C)) zero_lt_one
Simplifying the condition h E B(0, 1), we get ||^|| < 1. also use the fact that the distance from h to 0 is equal the norm of h, and the norm of h? is the norm of h squared. Thus, the goal reduces to showing:
exp(x + h) - exp(x) h exp(x)]] S eep(2))l ||A|12
for all h such that |h|] 1.
simp only (Metric.ment mal_ dist_zero_right norm_pow]
use the known bound for the exponential function, which states that for any complex numbers and with ||=||| 1, the inequality:
exp(x + =) - exp(x) - = exp(x)] s [xx((=)] ||=|
holds. This completes the proof.
exact fun z hz => exp_bound_sq x z hz.le
HERALD WHOLE PROOF
To show that the complex exponential function exp has the derivative exp(x) at x, we need to prove that:
exp(x + h) - exp(x) - exp(x) = o(h)
h approaches 0. This is equivalent to showing that:
|xxp(x + h) exp(x) h exp(x)] <
[exp(=))l ||al||
for h in neighhorhood of O.
First, we establish the simple fact that < by direct calculation. Next, we use the transitivity of big-O and little-o notation. Specifically, we need to show that:
exp(x + +h) - exp(xx) - exp(x)) S exp(x))] |
for h in neighborhood of 0. This will imply that exp(x + h) - exp(x) - exp(x) is O(h2), and since 222 = o(h) as ht - 0, it follows that exp(x + h) exp(x) - h exp(x) oh)).
restrict our attention to the open ball (00, 1) centered at with radius which neighborhood of O. This means only need to show the inequality for h such that ||||| < 1. Simplifying the condition h E B(0, 1), we get ||b|| < 1. We also use the fact that the distance from h to is equal the norm of h, and the norm of h.2 is the norm of h squared. Thus, the goal reduces to showing:
exp(x + h)) -ex((x) - h exp(x)]l S [ex((x)]] 2
27

---

Published as a conference paper at ICLR 2025
for à such that [|b]]
We use the known bound for the exponential function, which states that for any complex numbers
and with ||=||| 1, the inequality:
exp((> + 2) - exxp(x) - 2 exp(x))l - [xx(()]] ||=||
holds. This completes the proof.
OBT COMMENTED PROOF
theoren hasDerivAt_cxp (x C) HasDerivät exp (exp x) x by Show that the exponential function, exp, is fferentiaaeee at any complex number
The expcnential function is differentiable at x if and only if it is Lipschitz continuous in a neighborhood of We will show that exp is Lipschitz continuous by showing that there is a constant such that texp (x) exp (y) <= Cix yl for all x and y in a neighborhood of x.
Let be positive constant. Then, for any and y in neighborhood of x, have
-- (xx - e !exp (x - y) - 11 <= Ix - yl Texp (2) for some between and <= Cix -l
Therefore, exp is lipschitz continuon in a neighborhood of x, and hence differentiable at x. JhasDerivat_ifffiiiittttee_. have N) refine' (IsBig0. bound ||exp x|| J ttantrrss_a. irrans_sslitteer (isLittle0_pawk pow_id this)
by norm num
filtor_upwards [Metric.ball_mmmnng
(0 C) zero_lt_one]
simp only meeriicmen_bal,, dist_zcro_right, norm_pow] exact fun 2 cxp_bound_sq x h2.le
OBT GENERATED INFORMAL STATEMENT AND PROOF
Show that the exponential function, exp, differentiabl any complex number x.
The exponential function is differentiable at if and only if it is Lipschitz continuous in neighborhood of x. We will show that exp is Lipschitz continuous by showing that there is constant such that Texp (x) - exp <= Cix yl for all x and in a neighborhood of x.
Let be a positive constant. Then, for any and y in neighborhood of
x, we have
lexp (x) 1 = |exp (x y) - 11 <= yl lexp (2) for some between and y C|x yl
Therefore, exp is lipschitz continuous in neighborhood of x, and hence differentiable at x.
ANALYSIS
28

---

Published as a conference paper at ICLR 2025
The above theorem asserts that, for every complex number the exponential function exp (denoted as Complex. exp in Lean) defined on the complex numbers is differentiable at a with derivative exp22
In the OBT dataset, the LLM initially generated a proof that was not aligned with the formal proof, employing Lipschitz continuity. Subsequently, it attempted to relocate this independent proof into inline comments. We also note that this independent proof generated by the LLM is mathematically incorrect, Lipschitz continuity does imply differentiability.
In contrast, the Herald dataset's LLM closely translated natural language proof steps aligned with the formal proof and then summarized them into complete proof. This process ensures that the natural language result accurately reflects the proof strategy used in the formal proof. Notably, even the trivial assertion simple fact in isLi welitllee _e_lee______ee pow id is not explicitly explained.
2 is preserved in the natural language proof. However, the usage of this
E.2.2 PROOF EXAMPLE
FORMAL STATEMENT
theorem padi aadiccorrm___t_oom (p N) (hp p) padicNorm p p
HERALD STEPWISE PROOF
First, use the fact that the p-adic norm of is p for p 1. This transforms goal from showing [|p|pp < to showing p-1 < 1. Next, we use the equivalence that a < 1 and only if S 0 or 1 < Therefore, our goal is show p s 0 or <.p.
rw [padicNorm_p hp, inv inv_lt_one_iff)
Since is a natural number and < p by assumption, it follows that 1 < p. Therefore, the disjunction p or is true. This completes the proof.
exact cos_ Or.inr hp
HERALD WHOLE PROOF
We start by noting that the p-adic norm of is p for > 1. This is a known property of the p-adic norm. Therefore, goal is to show that p
Next, we use the equivalence that for any element a a linear ordered semifield, a-1 < if and only if < 0 or 1 < Applying this equivalence to p, our new goal show that p S 0 or 1 < p.
Since p is natural number and are given that p. it follows that i true. Therefore, the disjunction p < 0 or 1 < is satisfied. This completes the proof that [|]p < 1.
OBT COMMENTED PROOF
theorem padicNorm_p_lt_ooe
(hp 1 p) padicNorm p P 1 by If p is a prime number greater than 1, show that p (-p)
Because p is prime, (-p) is a rational number with denominator p'p.
Therefore, if (-p-) < then p² (-p) is between and I, and hence < (-p) <.
This implics that < p (p) (p) Because p is prime, p cannot divide p (p).
- So (p) must be >= 222. So >= p (1/p) So >= p (1/p). so 1 >=
P, which is false.
So must have (-p) >= 1, which is the same as p² (-p)
29

---

Published as a conference paper at ICLR 2025
IpadicNorm P hp, inv ____o___if exact_mod_ccat Or.inr hp
OBT GENERATED INFORMAL STATEMENT AND PROOF
If p is prime number greater than 1, show that " < 1.
Because p is prime, p p- a rational number with denominator pº. Therefore, pf 1, then P2
p " is between 0 and 1, and hence p= < 1. This implies that p". Because p prime, p cannot divide p". So pe must be 2 y². So 2 p² /p, So 2 pA/ So 2 p. which is false.
So we must have p 2 1, which the same as >
ANALYSIS
This theorem asserts that the p-adic norm of the element (which is 1/p) is less than 1. In the OBT dataset, the p-adic norm incorrectly translated as p Consequently, the subsequent natural language proof unfolds under this inaccurate setup. This issue of misinterpreting notations can be significantly mitigated by directly providing the definition the p-adic norm to the LLM. This can be achieved by first translating the definition of padi cNorm and then supplying the translation result to the LLM, as done in Herald using dependency order translation.
In this example, the Herald's whole proof is considerably more detailed than typical human-written natural language proof. In human human-written written mathematical literature, deducing p < 1 from < is considered trivial. The level of detail in Herald's whole proof is closer the formal proof than human language proof.
E.2.3 PROOF EXAMPLE 3
FORMAL STATEMENT
lemma fromColumn umns httpioollms__tcoollilee teColumns (A Matrix m (n) ① n2) R) fromColumns
A.toColumnsı A. AotoColumae umns2
HERALD STEPWISE PROOF
To prove that the matrix A is equal to the concatenation of its column blocks AuColumas, and Apcoouunsyy we introduce a new variable from the row indices m and consider two cases for the column indices: n, and j 72. For each case, simplify the expression to show that the elements of the concatenated matrix match the elements of the original matrix A.
ext i () 1
5) <;> simp
HERALD WHOLE PROOF
To prove that = AvoColumns @ AlaCnlummng we need to show that the elements the concatenated and column indices
matrix match the elements of the original matrix A for all row indices j E θ n22
#*Itroduuce new variable from the row indices m: the row indices m to reason about the elements of the matrix A.
** We introduce new variable from
2. ** Consideer
for the column indices:** **Case 1: j E nyy We need show
that (AloColumns, @ Aooolummss )zz = Ai for j By the definition of matrix concatenation by columns, the element in the i-th row and j-th column of the concatenated matrix A,ooolunss S
Awcolumnsg is given by:
(AuCColumss @ Aucoluumss iij AuColumms,
Since Apooolunss, is the submatrix of A consisting of the columns indexed by n1, we have:
Apooolumns
AAj
30

---

Published as a conference paper at ICLR 2025
Therefore, (AnColumns, ① AuColumnsy )ij = Aij-
**Case 2: j E n22 We need to show that (AwColumns, AuColumss ):j = Ai for E By the definition of matrix concatenation by columns, the element in the i-th row and j-th column of the concatenated matrix AcColumnsy + AbColumas is given by:
(AuColumns @ AcColummsa)) )ij A.Colummss.
Since ApColumns, is the submatrix of A consisting of the columns indexed by n2, we have:
Aucotumnsz.ij
Aij
Therefore, (AuColumasy AcColummsg Jaj Aij-
Since both cases show that the elements of the concatenated matrix AwoColumms, ① ApColummns match the elements of the original matrix A for all row indices i E and column indices j E m4 3 n2, we conclude that:
AroColumas @ Acoolumnss =
This completes the proof.
OBT COMMENTED PROOF
Temma fromCol umns www.uuunnnototttteeteeeoooooooot tttoooonCnnnssse (A Matrix m (m @ n2) R) The function "fromColumns takes two matrices and combines them into single matrix.
The "toColumnsi and "toColumnsz" functions split matrix into two matrices.
fromColumns A.toColumnsı A. A.toColumnsz A :- by The "ext" tactic extends the proof to all elements of the matrix. -- The 'j / 3' pattern matches only the elements of the matrix that in the second column.
The '<>>" tactic separates the two subproofs.
The "simp" tactic simplifics the expression.
ext i (1 j) <;> simp
OBT GENERATED INFORMAL STATEMENT AND PROOF
The "fromColumns" functicn takes two matrices and combines then into a single matrix. The "toColumnsi" and "toColumnsz" functions split matrix into two matrices. The "simp" tactic simplifies the expression. The "ext" tactic extends the proof to all elements of the matrix. The "j | j' pattern matches only the elements of the matrix that are in the second column. The "<;>" tactic separates the two subproofs. The "simp" tactic simplifies the expression.
ANALYSIS
This theorem asserts that if is block matrix of the form (A₃ A2), then after extracting two blocks (using toCollum uunosum and toCol toColumns]) and reassembling them (using fromCol umns), the result exactly original matrix A.
In the proof, the actual function of the tactics is not accurately described in the commented proof of the OBT dataset. For instance, the ext tactic applies the extensional property, rather than 'extending the proof to all elements of the matrix.' The whether an entry belongs to block A₁ or A2. The < tactic indicates that the subsequent tactic is applied to all goals.
pattern matches two cases, corresponding to
Correctly understanding the functions of the tactics is just the first step. To generate a coherent natural language proof, it is essential not only accurately grasp what each tactic proof step does but also to connect these steps logically. In Herald, this facilitated by providing tactic explanations and proof states. Human experts annotate the function, usage, and corresponding proof logic for each tactic
31

---

Published as a conference paper at ICLR 2025
in tactic explanations. The logic of equality of each entry implying matrix equality (extensionality for matrices) and discussing the column index by cases is clearly reflected the complete proof in Herald.
Another aspect to note from this example that, despite the translation principle the prompt to the LLM emphasizing the avoidance of words similar to formal language, the language used in Herald, such as 'Introduce new variable," remains somewhat formal and not entirely natural.
E.2.4 PROOF EXAMPLE 4
FORMAL STATEMENT
theorem treesOfNunNodesEq, suce (n N)) treesofNunNodestqq (n + 1)
(Nat anticiagnall n) biiniio fun ij =>
pairwiseNede (trecsofNunNodessgg 1j.1) (treesOrrunNodessgg 1).2)
HERALD STEPWISE PROOF
Since the definition of tresOOfuumNodeeSi(( + is the union of all sets of binary trees constructed by taking pairs (i.j) from the antidiagonal of n (i.e., pairs of natural numbers (i, such that j ni,, and forming binary trees where the left subtree has internal nodes and the right subtree has j internal nodes, we can replace the goal of showing treesONNuNoodesSg( 1) with the expression:
freesOfNumNodeeSqq(r + 1) (antidiagonal())) .attach. attach.
U
(4.j) (x)
suffices to show this new goal.
rw [treesoFNumNoodesFq]]]
To prove the equality of the sets, it suffices to show that for any binary tree a, is member of the left-hand side if and only if a is member of the right-hand side. We introduce new variable reason about the membership of in these sets.
ext
Using the properties of set membership and the definition of the set product of finite sets, simplify the proposition to show that:
(antidiagonal(n)) .attach.
U
(mm))daddd)
if and only if patrvieckoe(frrsOOiiindttttttt)) ortps///oooaaaoooooooooeeeeeaaan
U
(i.) Ea.dddiniiin))))))(()
This simplification is trivial and follows directly from the definitions and properties of set membership and the set product of finite sets.
s simp
HERALD WHOLE PROOF
32

---

Published as a conference paper at ICLR 2025
We start by using the definition of tresOONumNNodesEg(ir + 1). According to the definition, treesONNuNNodesEgg( 1) is the union of all sets of binary trees constructed by taking pairs (i,j) from the antidiagonal of n (i.e., pairs of natural numbers (i such that i + = n.) and forming binary trees where the left subtree has internal nodes and the right subtree has internal nodes. Therefore, we can rewrite the goal as:
IreeSOfNumNodeeeqq paiivisekooderrrsSonuunnsssssser (henss/sssssssttteooooononnnaaa)
(antidiagonal(n)) .attach
U
(antidiiiing)))))
It suffices to show this new goal.
Next, to prove the equality of the two sets, we need show that for any binary tree a, a is member of the left-hand side if and only if a is member of the right-hand side. We introduce in these sets. Thus, our goal is to show:
new variable reason about the membership
(antidiagonal( (n)) .attach.
U
(m)))iiaano)))))))
if and only if paiviisskodedrress/uuaaaasssss/ (reassas
U
(an))iaiiinnnnnn)((()
Finally, using the properties of set membership and the definition of the set product of finite sets, we can simplify the proposition. The left-hand side,
(antidiagonal()) (n) atttach.
U
(k.J) Eandddiaaingn)))))()))
is equivalent to the hight-hand side,
U
(i.j) (x)
This simplification trivial and follows directly from definitions and properties of set membership and the set product of finite sets.
Thus, we have shown that:
treesOfNumNNodesEqqrr +)
U
(i.) (an))iiiiili
This completes the proof.
OBT GENERATED INFORMAL STATEMENT AND PROOF
33

---

Published as a conference paper at ICLR 2025
Show that the number of trees with 1 nodes is equal the bi-union of the number of trees with nodes, where the bi-umion is taken over all pairs of nodes i and such that and j are not connected the tree.
By definition, the number of trees with + nodes is equal to the number of trees with n nodes plus the number of trees with n nodes. The number of trees with nodes is equal to the bi-union of the number of trees with nodes and such that i and j are not connected in the tree. Therefore, the number of trees with 1 nodes is equal to the bi-union of the number of trees with nodes, where the bi-umion is taken over all pairs of nodes and such that and are not connected in the tree.
nodes, where the bi-union is taken over all pairs of
OBT COMMENTED PROOF
theorem tressffkunNcdesec_..u (n N)
treesOfNumNodesfgg (n +
Natt.anticiagenal n) bilnion fun ij
pairwiseNode (treesOENumVodeegg 19.1) (treesSLNunNodesEgg 11.2)
== by
Show that the number of trees with n+1 nodes is equal to the bi -union of the number of trees with nodes, where the bi-union is nodes i and such that and j are not connected in the tree.
taken over all pairs
By definition, the number of trees with nt1 nodes is equal to the number of trees with nodes plus the number of trees with n-1 nodes. The number of trees with nodes is equal to the bi-union of taken
the number of trees with n-1 nodes, where the bi-union over all pairs of nodes i and j such that 1 and J are not connected in the tree. Therefore, the number of trees with n+1 nodes is equal to the bi-union of the number of trees with nodes, where the bi-union taken over all pairs of nodes i and such that and are not connected in the tree. zw |trees0fNuuNodesEqq
ext
simp
ANALYSIS
This theorem states that the set of binary trees with n + 1 nodes equals the union of the set of binary trees whose left subtree has nodes and right subtree has j nodes, where the union taken over indexes (i,j) such that i i
Although the natural language statement and proof the OBT dataset are mathematically incorrect, they still exhibit an advantage in their natural language style. There are no formal definitions remaining in this translation. However, in Herald, words from formal definitions remain in the ыTTX formulas, such as treesOfNumNodest.. antidiagonal, and pairwiseNode. Despite the principle summarized the prompt to the I.L.M that no formal words should appear in 18TE formulas, this principle is often violated. We believe that such poor behaviour in the translation of the statement, when exhibited to the LLM during proof translation, will cause the LLM to inherit this poor behaviour in the proof. It prioritizes style consistency over adherence to principles.
E.3 EXAMPLES AUGMENTED STATEMENTS
In this section, we present examples of augmented statements.
E.3.1 INFORMAL AUGMENTATION
We select one theorem and present the results of each informal augmentation strategy applied to this theorem. This example is also illustrated in Figure
FORMAL STATEMENT
34

---

Published as a conference paper at ICLR 2025
theorem not convergent! tac Tendsto (fun E in Finset range D, 1/i) atTop atTop by sorry
ORIGINAL INFORMAL STATEMENT
Let be positive natural number. The infinite of the sequence is not convergent.
There are four informal augmentation strategies in total: logical equivalence rewriting, abstract concept substitution, omission of implicit conditions, and multi-linguiste translation.
LOGICAL EQUIVALENCE REWRITING
The infinite sum of the sequence is divergent, where is positive natural number.
The infinite sum of the sequence does not converge, where n a positive natural number.
The phrase "is not convergent" is replaced by "is divergent" and the sentence structure is refactored.
ABSTRACT CONCEPT SUBSTITUTION
Let N The harmonic series diverges.
Let n E N The series Ene 1 diverges.
The LLM generates the commonly used term "harmonic series" for Σ and incorporates more ВTEX code into the statement.
OMISSION OF IMPLICIT CONDITION
The series Σ diverges.
The sequence '1'n' does not have a convergent infinite sum.
The condition "n a positive natural number" is removed from the statement.
MULTI-LINGUISTIC TRANSLATION
Soit n un nombre naturel positif. La somme infinie de la suite J n' esst pas convergente.
X n
ド '1/n'
The statement translated into French and Chinese.
E.3.2 TACTIC AUGMENTATION
In this section, select theorem in mathlib and present all tactic- augmened statements derived from the proof. The proof state n represents the proof state after the n-th line (counting after = by). We convert each proof state into statement.
35

---

Published as a conference paper at ICLR 2025
INFORMAL STATEMENT
For any cardinal number a, show that is strictly less than 2
ORIGINAL FORMAL STATEMENT WITH PROOF
theorem cantor
Cardinal. (u)) 2 by induction' a using Cardinal, inductionOn with a rw [K- Cardinal..m_sett
refine (((singleten, fun b => Singletton_e_ssinnleeon..i. 2_) rintro ((f, ht)) cantor_injective E hf
PROOF STATE
Type Cardinal.mt. 2 Cardinal.mk mk
Generated formal statement 1
lemma cantor_aug_l Cardinal mk a 2 Cardinal.nk a : sorry
Generated informal statement
For any set a, show that the cardinality of a is strictly less than the cardinality of its power set, ie., |a| < 2|a|_
PROOF STATE
: Type u Cardinal .mk a Cardinallnnf .kk (Set a))
GENERATED FORMAL STATEMENT
1emma cantor_aug_2 Cardinal.me a Cardinal.mt (Set a) :- sorry
GENERATED INFORMAL STATEMENT 2
For any set a, show that the cardinality of a is strictly less than the cardinality of the power set of a, i.e., |o|| < |2
PROOF STATE
Type u QQuotient. liftOn2 (Cardinal.mk (Set a)) (Cardinal.nd .nk a) (fun 8 => Nonempty (a B))
GENERATED STATEMENT 3
1emma 3 -Quatient: ftOng (Cardinal mk (Set a))
(Cardinal.nd .nk a) (fur. 8 Nonempty (a B)
Sendinal.instE..pe. 1 sorry
GENERATED INFORMAL STATEMENT 3
36

---

Published as a conference paper at ICLR 2025
For any set a, show that it is not the case that the cardinality of the set of all subsets of a can be mapped injectively into itself. Formally, demonstrate that there does not exist an injection from the power set of a to a.
PROOF STATE
a : Tyрe u
: Set + a
h Injective f False
GENERATED FORMAL STATEMENT
lemma cantor cantor_aug_$ Set a) (hf Injective f) False := scrry
GENERATED INFORMAL STATEMENT
For any function f from the power set of a to a, and given that f is injective, show that the statement leads a contradiction, i.e., it false.
ANALYSIS
Each proof state after tactic is extracted using Lean-jixia. In this proof, some tactics (the first and fourth lines this case) convert formalization details without changing the mathematical meaning. Other tactics (sccond and third tacties) correspond to steps in the mathematical proof and generate new proof goals. All these cases are converted into new statements, producing both new formal statements with the same meaning and statements with mathematical meanings.
F GRADUAtE TEXTBOOK AUTO-FORMALFEATION
F.1 THE STACKS PROJECT
The Stacks Project (Stacks Project Authors 2018) is an open-source, collaborative online resource that aims to provide comprehensive and rigorous treatment of algebraic geometry and related fields. Initiated by Johan de Jong, it has grown into vast repository of mathematical knowledge, encompassing topics from commutative algebra complex algebraic geometry. As of its latest update, the Stacks Project comprises over 7,609 pages of text and 21,319 tags of lemmas, theorems, and definitions, making it one of the most extensive and detailed resources in modern mathematics. By offering freely accessible and continuously updated reference, the Stacks Project has become an invaluable tool for researchers, educators, and students, significantly advancing the accessibility and dissemination of modern mathematical ideas.
To showcase the capabilities of the Herald translator in rapidly scaling up the auto formalizzaziininn of modern mathematics, selected preliminary sections from the Stacks Project, comprehensive and widely recognized resource for advanced mathematics. As an initial demonstration, we chose to formalize the Normal Extensions section (Stacks Project Authors 2018 'aa 09HL) in the Field Theory chapter, given its foundational role in abstract algebra and its clear, structured presentation, making it an ideal starting point for evaluating the effectiveness of our approach.
F.2 FORMALIZATION OF STACKS PROJECT SECTION NORMAL EXTENSIONS
import Mathlib
open Polynomial
/-- Let $K B. F$ be tower of algebraic field extensions. If SK$ is normal S-S, then $KS is normal over $H$.-/
37

---

Published as a conference paper at ICLR 2025
theorem tower top__t_poeeeeeccccceeppopoppppp_ ofponaal (F Type*) [Field [Field E]
[Algebra
[Field K] [Algebra к] [Algebra E X] [IsScalarTower K] [a Normal
F K]
Normal E by
We use the fact that normality is equivalent being a normal
extension.
have == h.out
-- The above statement is direct consequence of the transitivity of normality. exact Normal Normal. tower_tg....._fooooa
1-
Let SF be field. Let $M / FS be an algebraic extension. Let SM E / F$, $i Vin I$ be subextensions with $E F$ normal. Then $ \bigcap i_$ is normal
SFS.-/
theorem wormal_iinf.
wwwoooollllo. coomallexttacted (E M Type*) [Field F] [Field M] [Algebra F M] (E 4 + IntermeciateFiclo F M)
[Algebra. IsAlgebraic F M] (A (i : (), Normal I i)) + Normal F In
1, E 1) :- by sorry
1-- Let SE F$ be algebraic field extension. Let 53 be normal algebraic field extension. There exists unique subextension $2 / E_{ ext (sep 11 / F$ such that $E_ ext ext (sep ))
F$
F$ is separable and $E ELi ext (sep 11$ is purely inseparable. The subextensicn $E E_í ext (sep H1 / F$ is normal. -/
theoren Normal_cxt_sep_see ttt__c______eeeettttttttaa______ _et___tc__teeeee__eeee__ee
[Field F] [Field [Algebra F R] Isllgbbaaii F 8] (h : Normal E) Normal IiseparableClosure E) E := by sorry
-- Let $E F$ be algebraic extension of fields. Let 9\bar(F) be algebraic closure of $F$. The following are equivalent (1) $E$ is normal over $Fş, and (2) for every pair $/eigma, \sigma" \in loperatornane [Mor]_F \bar(F)) we have $1sigma (s) (Xprime)) (8) -/
theorem normal_iff_forat httpaaaaaaooiaillaaaaaaaaaaaaaoa j_et___ext_ee_ (F 8 Type*) [Field r]
[Field E] lAlgebra El [Algebra. IsAlgebraic I El (overlineF Type*)
[Field overlineF]
[Algebra F overlineF] [IsAlgClosure F overlineF]
Normal E + (o a' E +.[F] overlineF), Set.range tor Set range to
: by
sorry
/-- Let $E F$ be algebraic extension of fields. If SE$ is generated by $\alpha_i Vin i Vin I$ over $F$ and if for each $i$ the minimal polynemial
$taipha is over $F$ splits completely in ES, then $2 / F$ is normal. -/ theoren of st
: ;), Isintegral ott.oooooosstttttiiieee.....eeee (minpoly (a i))) : Normal F g :- by sorry
(F Type u_l) (E
Type v_2) [Field #] [Field Kj [Algebra K] (a
8) (ha : (V (), Splits (algebramap
i)) V
1-- Let $L M K$ be tower of algebraic extensions. If $L / K$ is normal, then any $KS-algebra map $lsigma: M \rightarrow L$ extends to an automorphism of $1$. -/
theorem
[Field F] [Field ž] [Algebra F E] [Normal 8] (M Intermediaterield F E) (o : In + [F] E)
8 E [F] E, 4 M, s
:- by sorry
Let $E FS be finite extension. We have $$ t / F) [1eq[E: F] sS with equality if and only if SE8 is normal over $ F$. -/
38

---

Published as a conference paper at ICLR 2025
theorem card 1e finrank tac 1714 [Field [Field E] [Algebra F E] (h : PiniteDimensional F E) Pintype card (E 2 B) S FiniteDimensional. finrank
finrank F == by sorry
Let $L K$ be algebraio normal extension of fields. Let $E / R$ be an extension of fields. Then either there is SK$ SKS-embedding from $L8 to $2ş or there is one au: ALightarrow ES and every other one is of the form $ au \eire \sigmaş where sisigma Vin Noperatornane i Aut (L $) -/
theorem embedaings [Algebra _atgss_att___ aut_equtte of isAlgNormal tac 12245 [Field Fl [Field GI
[Field H] [Algebra HI [Normal G] (e - +a[I]] Y f +.[F] H, a = G, --eea by sorry
The Normal Extensions section is presented as a runnable Lean source file, generated theorem by theorem and concatenated into complete formalization. For opened namespaces, we manually selected a minimal feasible subset from the union of namespaces across all theorems. The generation was completed efficiently using 16-pass setting. The faithfulness was checked by humans, and only three places were modified. Specifically,
(1) The argument (this Algebra I (ssparabbeelosure F E) E) that should be de- duced by Lean rather than manually provided normal ext sep_____________________________ ext cast_tac_28600 has been removed.
normal__xt_ssp_____
(2) The conclusion of the theorem extends_to_aut_offe
tac_ 7047 was corrected
from (z : IM), a 2 E to s : E =a [F] E, 4 M, s = 2.
(3) The conclusion of embeddings_dte labgs_aut_e_e lett_____s _et_autee__ofssslggkeeaa.e [___isAlgNormal tac @tac_12244 rected from Algebra. IsAlgebraic F G f G [F] Н, 3 s G =n [F] G,
e and unnecessary condition [FiniteDi wen.iieeesiinnnn Notably, the model demonstrates a strong understanding of the content, achieving both mathematical and programming correctness.
G] removed.
For prover integration, we used DeepSeek Prover 1.5 (using SrepSeek-Prover-Vee V1.5-RL + R.MaxSS with 512 sample budget) to run inference on the generated file. Only one theorem, a two-line proof relying on an existing lemma from Mathlib 4, was successfully proved. In our broader experiments with the Stacks Project, we observed that the prover struggles with longer or more complex proofs, showing instability and reduced capability. While our translator model performs well, this highlights the need for a prover model capable of handling advanced topics modern mathematics, which will be a key focus of our future work.
G EXAMPLES FROM EXTRACT THEOREM AND COLLEGE COT DATASET
In this section, we present examples drawn from the Extract Theorem and College CoT datasets. The Extract Theorem dataset contains theorems written in Chinese; however, for the sake of clarity, only exhibit English examples.
G.1 EXTRACT THEOREM EXAMPLES
Lemma 1.7 Suppose that p 2 is prime. Then non-normal subgroups finite p -group I1pp" n-1
G are conjugate if and only if G u, v. u² 1, up 1, l
2 2
Theorem 12.2.2. Let l (12) be weak solution of Au f.f E L (0) < x0, i.e.
[ Du Dip o-=-f fup for all & E C (?!).
Then WaP (S') for any Ω CC Ω. and
u/l ull const (1 (llleroo (Illeaa)))))))))))))
39

---

Published as a conference paper at ICLR 2025
with constant depending on p, d, Dt, and Q. Also,
Au f almost everywhere in 92
Proposition 47.11. Given any n N and given any abelian group л there exists an (n + 1) -dimensional CW-complex that has no cells in dimensions I,..., 1 and that is Moore space of type M (z,n).
Assume that gambler making fair unit bets on coin flips will abandon the game when her fortune falls to 0 or rises to n Let X be gambler's fortune at time t and let be the time required be absorbed at one of n Assume that Xo- k, where I k S n. Then
Pk (X, - n) = km
(2.1)
Eg (T) = =n k))
(2.2)
The examples provided above cover various math topics, including algebra (abstract algebra), analysis (partial differential equations), geometry (homology theory), and probability theory (stochastic processes). This dataset includes a broad spectrum of advanced undergraduatt-level material.
G.2 COLLEGE COT EXAMPLES
Theorem 31 (Nash & Tognoli) Any smooth compact manifold is diffeomorphic to a smooth real algebraic submanifold of some E", i.e. to the set of solutions of a system of polynomial equations.
Theorem 9.3.1 (Hahn-Kolmoge extension theorem-uniqueness of extension of a a -finite measure) Let be an algebra of subsets of non-empty set X and m A [0, oo] -finite measure on A. There exists a unique extension of m to a measure m' defined on the o -algebra S (AA)
Proposition 10.45. Let 0 S h < l2, and put r = 12 t Then the process (B..OsIS))
independent of a (B,, s & (2)) Moreover, B, Bo 0, and B is mean zero Gaussian process with covariance function (s, E [BBb} A str In particular,
Var Be
t)
Proposition 19.18. Let A be a ring and let A be an ideal that can be generated by completely intersecting sequence f of length r Let 91..... E I be elements that generate I. Then the sequence (gi....,gr) ) completely intersecting.
40

---

Published as a conference paper at ICLR 2025
The examples presented above cover graduate-level branches of mathematies, including algebraic geometry, measure theory, Brownian motion, and commutative algebra. This dataset includes more advanced mathematical materials compared to the Extract Theorem dataset.
41

---

Published as a conference paper at ICLR 2025
H PROMPTS
Instruction:
Suppose you are an expert mathematician and an expert Lean and Mathlib. Your task to first translate the formal definition provided below into informal statement that is more accessible to mathematicians and written in LaTeX. There are six parts of information attached the definition:
Head statements, including important statements, thcorems, and definitions of the mathematical field the theorem belongs to.
2. Then create informal name. Use the provided formal name of the statement according to the naming conventions. Utilize the informal statement written in the first task. Make sure follow the principles of informal naming when creating informal names. Principles of informal statements should also be followed much as possible.
Principles of Informal Statements:
1. The informal statement should be written using human-used mathematical notations and formulas in LaTeX as much as possible, explaining the meaning the symbols therein. Explain more dctailed mathematical setup only if the definition appearing in the statement is not commonly accepted. Both the inputs and values of the definition should be expressed using mathemnatica formulas as much as possible. Example:
DO NOT ""Raallog"".
Use "Slogg" instead.
Principles of Informal Names:
1. Emphasize the core concepts in the definition. The definition name should not merely list concepts; use words that indicate logical relationships and clearly state the conclusion. Example:
Use "A equals B" "A implies B" (or simply "$A BS" and "SA to BS"). instead "theorem A and B" when the theorem states the result of A B' or 'A- B'. Both the inputs and values of the definition should be expressed using mathematical formulas as much as possible.
Demonstrations:
Input:
<Head
statements=<<eighbbb Siatellnte=<Similarr translation examples><Formal name==Formal statement>
Output:
<Informal statement==Informaal name
Figure 7: Prompt for informalizing Mathlib4 statement
42

---

Published as a conference paper at ICLR 2025
Instruction:
Suppose you are an expert mathematician and expert Lean and Mathlib.
1. Your task translate each line of the formal proof in Lean, provided below, into corresponding step of informal proof. The informal proof must express the precise logic of the formal proof, written entirely in the language of mathematicians, and must use LaTeX. You will be provided with auxiliary information improve the translation.
The formal theorem, which the goal the entire proof. is written in Lean.
2. Then, generate the complete informal proof of the theorem. Utilize the steps of informal proof written in first task and reorganize structure the proof without altering logic. Ensure that you follow the principles of whole informal proofs when generating the complete informal proof of the theorem.
Principles of informal proof steps:
1. The informal proof should be written in commonly used mathematical notations and formulas in La'leX as much as possible. Explain more detailed mathematical setups only if the definition appearing in the statement not commonly accepted. DO NOT use backticks to quote anything in the natural language translation; use LaTeX style and $ for quotations.
Example:
DO NOT "RRe"llog";;
Use "Slogg"" instcad.
Principles of Whole Informal Proofs:
1. Restate the proof in the natural order of human language, rather than in the order of the formal proof. Do not distort the logic of the proof. Example:
"To prove using theorem 1, it suffices to show B, which is exactly the result of theorem
2." should be reformulated as "From theorem 2, we get B. Using theorem and B, we get
A. The logic of "B + theorem implics A; theorem I implies B" remains intact, and the sentence more natural.
Demonstrations:
Input:
<Formal name=<Formal statement==<Iformall name>< Informal statement><Head Dtaemnenss-DDtttrrig-DDeeped Tattemens=<<Tactic explanation==<Proof state> Output:
<Informal proof steps>> informal proof
Figure 8: Prompt for informalizing Mathlib4 proof
43


Reviews:
[{"review_id": "0HnoTfJ6CR", "reviewer": "Reviewer_5xV4", "summary": "This paper proposes an informalization pipeline based on static analysis of lean, which can be used to create parallel datasets of natural language proofs and formal language proofs.\nThey used their pipeline to create a natural language version of Mathlib4, and trained a transformer that formalizes natural language statements to lean.\nThe trained model, Herald Translator, is much better than existing models on auto-formalization.", "questions": "See weaknesses.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The authors provide a clear rationale for their methods and promise to open-source the whole pipeline for data generation. This is helpful for future research in AI-assisted math.\n2. The evaluation results look impressive, and they are beyond standard benchmarks. The authors demonstrated Herald translator's effectiveness on a real-world formalization project.", "weaknesses": "1. Lack of ablation studies. It's not clear to me which parts of the data generation/augmentation are helpful. More ablation experiments would help, especially for the multilinguistic augmentation. I'm really curious if that would result in NL statements in different languages.\n2. Does DeepSeek-Prover-1.5-Instruct perform well on formalization? If so, it would be interesting to see how herald translator compares with it.\n3. Contamination: Could the data augmentation/curation process introduce contamination issues such as putting parts of miniF2F into the training set?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "AVDueaslYA", "reviewer": "Reviewer_6Lbv", "summary": "This paper describes an autoinformalization (formal->natural translation) pipeline for Lean 4 statements and proofs. The authors also contribute Herald, an LM fine-tuned for autoformalization on a dataset of formal-informal statement pairs generated by applying the proposed NL augmentation pipeline to mathlib4, the Lean 4 math library.\n\nThe authors' pipeline retrieves relevant definitions and documentation in order to ensure uninformative formal names can be translated appropriately. When translating statements as part of proof informalization, their method analyzes proof structure in order to stratify statements (i.e. sort them topologically) ensuring that natural versions of a statement's logical dependencies are available when translating it.\n\nThe authors include qualitative comparisons between their method and prior art (Open Bootstrapped Theorems/OBT) detailing both successes and failure cases.\n\nThe authors evaluate their fine-tuned autoformalization model by computing the proportion of statements in a test set for which any of a set of 128 samples drawn from the formalization model pass two checks: syntactic correctness according to the Lean REPL, and backtranslation with a fixed informalization LM followed by LM-based NLI between the original and backtranslated NL. This evaluation is conducted on three test sets: miniF2F, a custom dataset extracted from textbooks via OCR, and another one scraped and filtered from internet math resources. The authors compare their fine-tuned model to three baseline models: TheoremLlama, InternLM2-Math-Plus-7b, and Llama 3 Instruct. According to the authors' chosen metric, their model outperforms the other considered models substantially across all three sets.", "questions": "1. It seems like one of the main issues remaining in the Herald natural augmentations is the presence/copying of formal names. From the text and the prompts it sounds like you mainly attempted to combat this using instructions, but that had limited power. Did you try rejection sampling (sample multiple times and reject translations containing Lean-specific names)?\n\n2. What is the specific provenance of the web-scraped test set (College CoT)?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "- The proposed augmentation pipeline is well-designed. In particular, it's a great idea to use the results of structural analysis to order statement translation within proofs to allow informalization to condition on both formal and natural language versions of a statement's logical context. Herald definitely seems to me to be a step forward in terms of the quality of augmented examples.\n\n- While many of the comparisons this paper makes between Herald and prior work are qualitative, I found the detailed example-based analysis in the appendix to be convincing support for these claims. I greatly appreciate the authors' candor in highlighting Herald's shortcomings in addition to positive differences between their method and OBT.", "weaknesses": "- It's hard for me to get a sense of the significance of the fine-tuning results, given that both the chosen metric and two of the three datasets used for evaluation are constructed by the authors. It would be helpful to see some representative examples of the two custom test sets, in addition to samples from the model that pass and fail each validation step.\n\n- I also feel that it's essential to audit the LM NLI check and report its correlation with human expert judgements of semantic equivalence for original + back-translated statements from the test domains (it's fine if this is a reasonably small sample size). Without this information, the valid% metric seems shaky.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "mfsnN6VMrT", "reviewer": "Reviewer_BoSn", "summary": "- This paper develops a novel parallel natural language-to-formal language data synthesis method and extends it into a practical method for automatic formalization of literature.\n- The method demonstrates strong generalization ability with significant performance gains.\n- This tool will be useful for future data synthesis in the community.", "questions": "- Please include some additional baselines.\n- Ablation studies are missing; please include them.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper extends the boundaries of autoformalization using a Retrieval-Augmented Generation (RAG) based method.\n- The paper develops an innovative, practical tool that helps extend its reach to users beyond the community.\n- The paper's method is simple, and the writing is well-done.", "weaknesses": "- I believe that a contextual learning approach was used in the translation process. There should be a detailed investigation into how different retrieval methods affect it, as they directly impact the accuracy of the model's output.\n- Why not compare it with other autoformalization methods, such as [1,2].\n\n\n\n**Reference**  \n[1] FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving.  \n[2] FormalAlign: Automated Alignment Evaluation for Autoformalization.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "rOdgBhI0n3", "reviewer": "Reviewer_4Ljo", "summary": "The authors approach the problem of autoformalization, a heavily data-scarce domain, by automatically generating a dataset of natural language-formal language pairs by auto-informalizing mathlib. This is done with LLMs which are fed important context such as dependent theorems, docstrings, and similarly-named theorems (which are often highly related) together with a retrieval-augmented system to improve translation quality.\n\nFurthermore, they augment proof data to acquire similar data for NL-FL proof pairs in two ways. First they sample intermediate proofs, and second they paraphrase informal statements.\n\nAfter this data is compiled, a formalization LLM is fine-tuned on the resulting dataset, and a pretrained theorem prover is used to generate the proofs, and the authors show this data is useful for improving autoformalization performance on their chosen benchmarks.", "questions": "- See \"Weaknesses\" section above for some potential places to improve clarity of paper. \n- Is there a reason you didn't evaluate on ProofNet (there are available Lean 4 versions of the dataset)? It is a useful benchmark for more difficult undergraduate problems, which seems to be in-line with your other choices. \n- What was your selection process for the Stacks project? From the outside, it looks like a cherry picked example, which I think is ok but it should be made clear. \n- I am unclear as to what the aligned proof data from the Herald was used for in the training of the model. It seems like all the reported experiments are just for theorem statement formalization. Can you clarify?\n\nOverall, I believe this can be a solid paper but needs some clarifications. Assuming the clarifications don't significantly harm the paper and the experiments and results are sound I think my rating(s) can be improved.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "The proposed dataset has clear use to the community as a large dataset of natural language/formal language pairs for autoformalization system training. Additionally, the Herald translator is an improvement over previous methods, achieving very high performance on translating miniF2F problems, and improved performance on more difficult college-level datasets. Overall, I believe the work is well-supported.", "weaknesses": "- The authors use a pass@128 metric for successful autoformalization. This seems like a highly lenient metric, and I'm curious to know if there is prior work which uses this metric, or if the authors chose this for a particular reason (I don't recall any previous use of this in autoformalization, but I may be wrong). If high performance is contingent on so many trials, I believe the compute efficiency is a significant weakness of the approach.\n- Similarly, are the baseline approaches (Theorem Llama, Llama-3 instruct, etc.) in Table 2 also measured using Pass@128?\n- It is unclear whether Table 2 is autoformalization performance is only theorem statements, or both theorems and proofs. MiniF2F contains some formalized proofs, but isn't complete, and I am unfamiliar with the other two. If Table 2 is only theorem statements, are there results showing the proof-translation performance?\n- There are no examples of generated pairs from the Herald dataset which makes it difficult to assess the data quality. Examples from the two augmentation would be especially insightful. I see outputs from the Herald translator in the Appendix, which look high quality. \n- Also, a comparison of the Herald Translator trained on various datasets is important to judge the quality of the Herald dataset. For example, trained on MMA, LeanWorkbook, etc. and evaluated on the same benchmarks as the Herald Translator was.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)