Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning
Authors: Marcus J. Min
Yeqi Gao
Wilson Sy
Zhaoyu Li
Xujie Si
Osbert Bastani
Venue: ICLR 2026 Poster (2026)
Keywords: Autoformalization
Formal Mathematics
AI for Math
Neurosymbolic AI
LLM
Large Language Models
Formal Theorem Proving
Neural Theorem Proving
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We designed a framework that not only improves LLMs at formalizing a corpus of statements, but also learns a library of reusable abstractions, which scales to statements outside of the corpus.

Abstract: Existing approaches to autoformalization---the task of translating informal mathematics into formal machine-verifiable languages---rely heavily on pre-defined libraries and expect LLMs to directly generate complete formalizations. These approaches face three fundamental limitations: they are bottlenecked by existing abstractions, they have difficulty handling the complexity of realistic statements, and they do not transfer well across formal languages.
We propose $\textit{Divide and Abstract (DNA)}$, a zero-training framework that addresses these challenges through a two-phase approach.
First, $\textit{DNA}$  extracts common mathematical concepts from the entire corpus and formalizes them as reusable abstractions, extending the target language's capability.
Second, $\textit{DNA}$ hierarchically decomposes new statements into structured informal clauses, translates each clause using the learned abstractions, and composes them into complete formalizations.
Our evaluation on the LeanEuclidPlus and ProofNet-Hard benchmarks demonstrates consistent improvements across multiple model families, achieving up to $\textbf{8.6}\times$ performance gains over baselines.
Notably, $\textit{DNA}$  enables smaller models to match baselines using much larger models, and shows particularly strong performance on complex mathematical statements requiring nested reasoning. Furthermore, our framework requires no training on target languages, making it effective for low-resource domain-specific languages. Our code is available at https://github.com/marcusm117/DNA.

Published as a conference paper at ICLR 2026
DIVIDE AND ABSTRACT: AUTOFORMALIZATIIN VIA DECOMPOSITION AND ABSTRACTION LEARNING
Marcus J. Min'
Yeqi Gao Wilson Sy
Zhaoyu Li
Xujie Si Unniveriity of Toronto
Osbert Bastani'
Universitty of Pennsylvania Tsinnhua University (ma remin, n, obastani] @saas... upenn.edu s six0cs. toronto.edu
sixecs.toronto..ee
ABSTRACT
Existing approaches to autoformalization the task of translating informal math- ematics into formal machine-verifiable languages-rely heavily on pre-defined libraries and expect LLMS directly generate complete formalizations. These approaches face three fundamental limitations: they are bottlenecked by exist- ing abstractions, they have difficulty handling the complexity of realistic state- ments, and they do not transfer well across formal languages. We propose Di- vide and Abstract (DNA), a zero-training framework that addresses these chal- lenges through two-phase approach. First, DNA extracts common mathemati- cal concepts from the entire corpus and formalizes them as reusable abstractions, extending the target language's capability. Second, DNA hierarchically decom- poses new statements into structured informal clauses, translates each clause us- ing the learned abstractions, and composes them into complete formalizations. Our evaluation on the LeanEuclidPlus and ProofNet-Hard benchmarks demon- strates consistent improvements across multiple model families, achieving up 8.60 performance gains over baselines. Notably, DNA enables smaller mod- els to match baselines using much larger models, and shows particularly strong performance complex mathematical statements requiring nested reasoning. Furthermore, our framework requires no training on target languages, making it effective for low-resource domain-specifer languages. Our code available btttps:/gqit http://uwww...oaaaauucuo////////
INTRODUCTION
Autoformalization the task of automatically translating informal mathematics into formal lan- guages designed for theorem provers such as Lean (Moura & Ullrich 2021 and Z3 (De Moura & Bjorner, 2008), so that theorems and proofs written in natural languages can be mechanically ver- ified. The success of autoformalization will significantly reduce the amount of labor from human experts, and thus empower three transformative applications:
1. Synthesizing informal-formn parallel data for training neural theorem provers (Xin et al. 2024
Grounding and guiding reasoning processes in natural languages (Yang al.
2022
3. Accelerating verification of important mathematical theorems (Gonthier et al. 2013 Hales et al., 2015) or engineering systems (Zhao et al. 2012 Reid et al.) (016)) not only to identity potential gaps and mistakes, but also to facilitate certified extensions and future mathematical discovery.
Inspired by the breakthrough of Large Language Models (LLMs)) in machine translation between natural languages, researchers have increasingly applied LLMs autoformalization (Weng et al., 2025). Even though the ultimate vision is to automatically formalize entire theories that include axioms, definitions, notations, theorems, and proofs, current LLMs struggle even formalize individual statement (Murphy et al. 2024 Liu et al. (025a)).
Previous work in LLM-based statement autoformalization has explored in-context learning (Wul ct al. 2022), fine-tuning specialized autoformalizer models (Jiang et al.) (202aa), invoking retrieval before LLM inference (Liu al. 2025a), employing post-inference techniques such majority

---

Published as a conference paper at ICLR 2026
(a)
Phase Language Extension via Abstraction Learning
Informal Statement
Language Decumerration
Common Math Concopes
Concepts
eron Lin: 'S4
Informal Statement
deline leco rimmunt in poid?
The ciatnal dirrui lg dll poir"
sacarraae Micied on lial
ally and
Informal Statement
Concept Eerection
Concest Flawring
Tre pely lyng opper
CD0 Consinxd on
Updated Documentation
Refactored Formaa Definitions
Formal Delinitons
Conoept Dependency Graph
Pos wash 20
Call altrun CaN Parr Lin)
[
sppee very
enam 'oor
Poind
Use
Portercaee
snquar cally pe sotorn bJ capae riguo
Ubdese
diollgre tia thans
Retedtring
Formel Delic
tine spod Farul dediee
Born-Forndledd Structure
Formaiieed Stracture
Informal Siatermen
Formal Statemant
Line MY and 52 Inlenac X. TV and
wen't
Faoner Phoien 1: (M 02 T2TVX
and Colliwer and onkend The porta T,
pe tie audid
Matt seirssheeeaee aneeeeeeeeeeeeee 5,2
diaeefs nao Lie WY
V, ene other snde 52
$2.5
B BUX-
T Comples pool WTV
Gieon x
Opoorpostton
Formelazion
Compostoon
7292
IT
gia UXT
coent) and
Sande WY TV
M
CVCS
(b)
Phase II: Statement Formalization via Decomposition and Self-Refine
Figure 1: Overview of the Divide and Abstract (DNA) framework. (a) Phase I (Language Ex- tension): Given an informal corpus, we extract common mathematical concepts, filter out those already present in the target language, construct a concept dependency graph (CDG), and systemati- cally formalize concepts following topological ordering to extend the DSL. (b) Phase II (Statement Formalization): For each statement, we hierarchically decompose it into remi-formalized compo- nents, translate each component using the learned abstractions, compose them into complete formal statements, and refine using symbolic validator feedback.
voting and semantic consistency ranking by an embedding model (Li et al. 2024a). However, all these approaches suffer from limited generalizability due to three fundamental challenges:
1. Bottlenecked by Existing Abstractions: The performance of formalizing the same informal statement is limited by the richness of existing abstractions in the target formal language. For ex- ample, if the target language only contains basic formal definitions of sets and real numbers, then formalizing the relation "a topological space being a manifold" would be difficult even for human experts. In contrast, if the target language already provides formal relation "isManifold", then the translation is simply a one-to-one mapping. However, all existing methods rely heavily on pre- defined abstractions in existing libraries like Mathlib in Lean (Mathlib Community (0200) and HOL sessions in Isabelle (Nipkow et al., 2002), which fail to generalize to the cases where the target language doesn't provide an extensive coverage of high-level abstractions.
2. Difficulty Handling Complex Statements: Regardless of the availability of relevant abstrac- tions, the difficulty of formalization also grows proportionally to the complexity of statements. For example, formalizing a simple statement like "function f is continuous" is straightforward when the formal definition of continuity exists. However, formalizing a nested statement such as "the space of continuous functions from compact manifold to a Banach space forms a complete metric space under the supremum norm" requires understanding and correctly composing multiple layers of mathematical abstractions. Nonetheless, all existing approaches expect the LLMs to directly gen- erate the final formalization at inference time, which does not generalize well to complex statements that involve nested quantifiers, higher-order objects, and composite relations.
2

---

Published as a conference paper at ICLR 2026
3. Limited Transfer Across Formal Languages: Orthogonal abstraction availability and state- ment complexity, the choice of target formal language constitutes a third dimension of the gener- alizability challenge. Most fine-tuned autoformalizer models (Gao et al. 2025 Wang et al. 2025 Xuejun et al. 2025) are heavily trained on Lean Mathlib and formal statements that directly use Mathlib abstractions. However, shown in Table these models perform poorly when the target is a domain-specite language (DSL) that is not in the training data, or even when Mathlib evolves newer versions with updated syntax and library structures.
To address these limitations in generalizability, we propose an end-to-end framework Divide and Abstract (DNA) with three key designs that directly correspond to each challenge:
1. Abstraction Learning: While previous methods treat the formalization of each statement in- dependently, we leverage the insight that statements within the same corpus often share common mathematical concepts like definitions of objects and relations. As shown in Figure a given the current language documentation and target informal corpus, DNA first extracts these shared con- cepts from the entire corpus and formalizes them as collection of reusable formal abstractions. This phase essentially extends the target language by enriching the library of available abstractions, thereby facilitating the statement formalization both within and beyond the corpus.
Hierarchical Decomposition: Unlike existing approaches that let LLMs directly generate the formal statement, we take advantage of the fact that mathematical statements data-each statement consists quantifiers and a body, and the body is broken down into a list of premises and list of conclusions; further, quantified statements nested in the premises conclusion can be recursively decomposed in the same manner. As shown in Figure I DNA hierarchically decomposes a statement into a structure of informal clauses, translates each clause into its formal correspondents, and composes the formal clauses back into a complete formalization. Since we have learned rich library of reusable abstractions, the formalization of each individual clause becomes significantly more tractable than formalizing the entire complex statement at once.
semi-structured
3. Zero- rroo-Triinng Framework: DNA is designed be zero-training, plug-and-play framework. This is achieved by simply providing the target language's 's documentation in the context of the LLM. After the abstraction learning phase, the documentation updated with the newly learned formal definitions, and then passed as context to the statement formalization phase, conditioning the LLM on both the original language specifications and a library of directly usable high-level definitions. The entire framework requires no training on the target formal language, and is thus particularly effective for low-resource DSLs.
We evaluate DNA on LeanEuclidPlus and ProofNet-Hard against fine-tuned autoformalizers and general-purpose LLMs including GPT-4. 1/5, Claude-4-Sonnet, and Qwen3 variants. DNA consis- tently outperforms baselines across all model families, with the most dramatic improvement being Qwen3-1 14B advancing from 1.0 to 9.6 success rate (9.6x gain), while PPT--411mmn improves from 4.8 near GPT-4.1 levels. On ProofNet-Hard, all baselines achieve zero success, whereas DNA en- ables successful formalization, demonstrating its effectiveness for domain-specific languages lack- ing extensive training data. To summarize, our contributions are as follows:
(1) identifying three generalizability challenges in autoformalization, (2) proposing a zero-training framework combining abstraction learning and hierarchical decomposition, (3) demonstrating 1.17x to 9.6x improvements across diverse models and benchmarks, and (4) enabling effective transfer to challenging domain- domain-specifie languages where specialized models fail entirely.
2
THE Divide and Abstract FRAMEWORK
2.1 PHASE LANGUAGE EXTENSION
As illustrated in Figure D a)) the language extension process unfolds through six coordinated steps.
Step 1: Concept Extraction. The first step of our abstraction learning pipeline aims to extract math- ematical concepts that are non-an non-ambiguous, well-defined, and abstract, as specified in the prompt guidelines detailed in Appendix D.I.I These extracted concepts encompass three categories: math- ematical objects, relations between objects, and functions mapping objects to objects. Our extraction process enforces precision by specifying argument types and counts, dell-definedness by ensuring
3

---

Published as a conference paper at ICLR 2026
Step 1: Concept Extraction
Step 2: Concept Filtering
Run
Recall
Correctness
Run
Correctness
Average
94.44%
100.00%
Average
100.00%
Step 3: CDG Construction
Step 4: Concept Formalization
Run
Correctness
Run
Correctness
Average
100.00%
Average
97.87%
Step 5: Refactoring
Step 6: Documentation
Run
Correctness
Compression
Correctness
Qwen3-235B
GPT-5 mini
Average
99.155%
1.59
100.00%
97.4%
99.8%
Table 1: Performance Analysis of each step in Phase Abstraction Learning, averaged across runs on LeanEuclidPlus. Please refer to Appendix C.I for detailed analysis of qualitative examples on both LeanFucliddPlus and ProofNet-Hard.
conventional mathematical validity, and abstractness by avoiding particular variable names or spe- cific instances.
We evaluate the quality of this extraction step using two metrics reported in Table I both averaged across 5 runs. The correctness metric measures what percentage of the extracted concepts are indeed non-ambiguous, well-defined, and abstract out of all extracted concepts. The recall metric quanti- tatively analyzes how many concepts from the oracle abstractions written by human experts successfully identified and extracted by our system. Both metrics are evaluated manually because the output of this step consists of freeform natural language descriptions, and no reliable automated evaluation alternative exists for assessing the semantic correctness.
Step 2: Concept Filtering. The second step of our abstraction learning pipeline performs concept filtering to remove duplicates and concepts already formalized in the target language, as specified by the guidelines in Appendix D.1.2 The filtering process leverages LLM understanding of both the extracted concepts and existing DSL capabilities to identify gaps in abstraction coverage.
We evaluate this filtering step using the correctness (precision) metric reported Table for the filtering step, which measures what percentage of filtered-out concepts are indeed duplicates or formaize-d out of all filtered-out concepts, averaged across runs. We deliberately focus on precision rather than recall for two important reasons. First, in the abstraction learning phase, our priority is to formalize reusable abstractions without missing potentially useful concepts, making filtering precision naturally more important than recall. Second, borderline cases exist where natu- ral language concept does not directly correspond to exactly one formal definition but can easily formalized by slightly adapting existing definition. For instance, the concept of two triangles sharing a common vertex in Euclidean space has no direct corresponding formal definition, but be straightforwardly expressed by specifying the three vertices of each triangle. We design the filtering step to remove only those cases that are absolutely obvious duplicates or concepts, erring on the side of caution to preserve potentially useful abstractions. The correctness metric is evaluated manually for the same reason as Step 1.
The third step of our abstraction learning pipeline constructs concept dependency graphs that analyze how each extracted concept can be formalized using existing formal definitions and other concepts, following the guidelines in Appendix D.1.3] The depth and complexity of these dependency graphs vary across benchmarks and concepts. For each concept, we analyze direct expressibility using existing DSL elements, pre- requisite concept dependencies, and formalization feasibility. The CDG contains two node types: leaf nodes that are either directly formalizable or impossible to formalize within the target language scope, and parent nodes that depend on other concepts. Formalization follows topological ordering by starting with leaf nodes, then proceeding layer by layer up the dependency hierarchy. Algo- rithm [ details the construction process. Notably, CDG construction inherently performs concept decomposition, demonstrating that abstraction and decomposition are complementary, with neither achieving optimal performance in isolation (Table 3
Step 3: Concept Dependency Graph (CDG) Construction.
4

---

Published as a conference paper at ICLR 2026
Algorithm 1 Concept Dependency Graph (CDG) Construction Algorithm.
Input: Filtered Concepts C, Current Language Documentation D, LLM M
Output: Concept Dependency Graph containing all concepts C' and their dependencies
1: Initialize the analysis result dict A < 0
2: Initialize the to-be-analyzed queue Q + C
3: Initialize the have-analyzed set S <-
4: while 2 * 0 do
5:
fetch the next lo-be-analyzed concept 6: Analyze concept using LLM M given context (D, determine the dependency status of
Q.dequeue)
c, which can is one of: _xtpeetiy_eepeessbbleee, "needs_ "eeeddddeeendenciess" or "impossible" D save analysis result
7:
Alc] <- analysis result
8:
S S
b add c to the analy-a set
9:
if c has status "needs dependencies" then for each dependency d in the dependency list of do if d & S and d & Q then @ + QU {d}
11:
12:
> add d to the to-be-analyzed queue
13:
return A
We evaluate this CDG construction step using the correctness metric reported in Table D which measures the percentage of the dependency analyses for each concept that are correctly constructed out of all dependency analyses, averaged across runs. The correctness metric is evaluated manually for the same reason as Steps and 2.
Step 4: Concept Formalization. The fourth step of our abstraction learning pipeline translates the concepts identified in the CDG into actual formal definitions in the target language, following the guidelines Appendix This step involves generating both the main target definitions and any necessary helper definitions to support them. The formalization process adheres to target language conventions and ensures syntactic correctness through iterative refinement.
We evaluate this formalization step using the correctness metric reported in Table I which measures what percentage of formal definitions are correct out of all formal definitions, with helper definitions counted separately (essentially counting the number of function definitions), averaged across runs. Importantly, concepts not need to be formalized by strictly following the previously analyzed concept dependency graph; formalization is considered correct as long as it can be interpreted as faithful to the original natural language concept. The correctness metric is evaluated manually despite the output being in formal language because the same natural language concept can be formalized in multiple ways that are all acceptable to human experts. As discussed in Section 3 no symbolic equivalence checker is complete, and some not even sound, necessitating manual evaluation by human experts to assess faithfulness.
Step 5: Formalization Refactoring. The fifth step of abstraction learning pipeline performs formalization refactoring to eliminate redundant definitions and extract common helper definitions, thereby creating a more concise and general library of learned abstractions that downstream users, whether human or language models, can better understand and employ. This refactoring process follows the guidelines specified in Appendix D.1.5
We evaluate this refactoring step using two metrics reported in Table D The correctness metric measures what percentage of refactored formal definitions are correct out of all definitions that were refactored, with helper definitions counted separately (essentially counting the number of function definitions), averaged across 5 runs. Additionally, we quantitatively analyze the compression ratio, which is the ratio of the number of formal definitions before refactoring to the number after refac- toring, averaged across 5 runs. This compression ratio metric important because it indicates how effectively common helper functions are reused and how many unnecessary formal definitions are eliminated. A high compression ratio facilitates better understanding and utilization of the learned abstractions by both humans and language models, it reduces cognitive load and clarifies the sential conceptual structure. The correctness metric evaluated manually for the same reason as Step 4, since multiple semantically equivalent refactorings may be acceptable human experts.
5

---

Published as a conference paper at ICLR 2026
Error Type
Qwen3-235B
GPT-5
Unfaithful Variable Name
1
1
Validation Error
8
2
Stronger/Weaker Translation
10
17
Incorrect Translation
11
8
Table 2: Error analysis of 200 failed formalization attempts. where 100 are from Qwen3-235B and another 100 from GP5-5, The numbers shown are the count for each error type. Four main error categories were identified.
Step 6: Documentation Update. The sixth and final step of our abstraction learning pipeline generates clear and concise natural language documentation for the learned abstractions, abstracted away from low-level implementation details such as internal helper definitions, to serve both human and language model users. This step is critical because excessive definitions in the documentation would inevitably confuse both language models as the context grows and human users attempting to understand and use the learned abstractions. The documentation generation process follows the guidelines specified in Appendix D.I.6
We evaluate the documentation update step using quantitative metrics reported in Table | The cor- rectness metric measures what percentage of documented formal definitions correctly convey the meaning of the definition without missing any essential details or introducing ambiguity, out of all documented definitions, averaged across 5 runs. We also evaluate downstream task performance on LeanEuclidPlus using two strong models, Qwen3-235B and GPT-5, with our four-stage hicrarchi- cal decomposition pipeline. Under the hypothesis that good documentation should enable strong models to generate syntactically correct formalizations with high reliability, we report the compila- tion rate of the two models averaged across 5 runs. For Qwen3-235B, the maximum compilation rate is 98.2%, minimum 96.8%, mean 97.4%, and standard deviation 0.47%; for GPT-5, the maximum is 100.0%. minimum is 99.0%, mean is 99.8%, and standard deviation is 0.45%. These consistently high compilation rates with low variance validate the quality and stability of the gener- ated documentation.
for concept extraction, filtering, and dependency graph construction LeanEuclidPlus. while using GPT-5 with high reasoning effort for ProofNet-Hard, For the more complex tasks of concept formalization, refactoring, and documentation generation, we utilize GPT-5 with high reasoning effort across both benchmarks to ensure high-quality formal definitions and coherent abstraction libraries. In Table [ we show how error language extension decomposes across steps.
For Phase language extension, we employ D-we3-233B-IIme
2.2 PHASE II: STATEMENT FORMALIZATION
Building upon the extended DSL from Phase I, Phase II employs hierarchical decomposition to formalize individual statements. Unlike existing approaches that expect LLMs to directly gener- complete formalizations, our framework systematically breaks down complex statements into manageable components that can be formalized using the learned abstractions.
Motivation and Error Analysis. To motivate our decomposition approach, conducted an error analysis on 200 failed formalization attempts (100 each from Qwen3-235B and GPT-5) using base- line methods without our pipeline. As shown in Table 2 we identified four primary error categories. Validation errors include syntax issues and logical consistency violations that prevent successful compilation. Stronger or weaker translation errors represent semantic misalignment where formal- izations are either too restrictive or too permissive compared to the English statement. Incorrect translation errors involve wrong formal correspondents or parameters for relations. Unfaithful vari- able naming creates inconsistency between variable names in formal and natural language. This analysis reveals distinct error patterns across models, motivating our dccomposition approach that systematically addresses each error type.
Solution for Each Error Type. Our four-step decomposition pipeline systematically addresses each significant error type, excluding "Unfaithful Variable Name", through targeted design choices. Step decomposes complex informal statements into semi-formalized structures with explicit quan- tifications, premises, and conclusions, ensuring logical scope precisely matches the informal state-

---

Published as a conference paper at ICLR 2026
ment and addressing stronger/weaker translation errors. Step translates each component using learned abstractions from Phase I, enabling focused attention on correct formal correspondents and parameter assignments for individual clauses rather than managing entire statement complex- ity, thereby addressing incorrect translation errors. For instance, in LeanFuclidPlus, the relation fo rorTri angl requires specific parameter ordering where points a, b must lie on line 4 points b, c on line /2, and points a, on line (3-our clause-by-clause approach helps prevent logical con- tradictions from incorrect parameter ordering.
Step 3 systematically composes formalized components back into complete formal statements while ensuring proper quantifier scoping and logical consistency, reducing validation errois through struc- tured composition that maintains clear relationships between components. Step 4 employs com- prehensive self-refinement with symbolic validator feedback that performs three checks: syntax correctness, variable name faithfulness between formal and natural language representations, and logical consistency verification, ensuring premises are non-contradictory and conclusions are non- trivial. Unlike existing approaches that rely solely compiler feedback, our validator provides targeted semantic feedback to guide iterative LLM refinement, directly addressing validation errors and unfaithful variable naming until the formalization meets all quality criteria.
EXPERIMENTS
Benchmarks. We evaluate DNA two benchmarks: LeanFuclidPlus and ProofNet-Hard. Lea- nBuclidPlus adapts LeanFuclid (Murphy et all 2024), implementing a formal Euclidean geometry system (Avigad al., (2099) as a domain-specifie language (DSL). The scarcity of training data for LeanEuclid-styy statements makes it ideal for evaluating autoformalization generalizability across DSLs. We refined the 100 UniGeo problems from LeanEuclid and added 40 hand-crafted statements with greater geometric complexity.
Our main evaluation uses the 100 core problems for end-to-end pipeline assessment, while the ad- ditional 40 problems test generalizability of learned abstractions and decomposition-ddiieen formal- ization. ProofNet-Hard comprises 19 challenging ProofNet (Azerbayev al., 2023 Vishwakarma et al. 2024) statements requiring auxiliary helper definitions beyond standard Mathlib imports. As Table shows, when helper definitions are withheld, both specialized autoformalizers desppp
ProofNet training data (Wang et al., 2025 Xuejun et al. 2025) and tftt-offthhe-rt models like
GPT-5 and Claude-4-Sonan achieve zero success rates.
Evaluation. Previous work uses LLM backtranslation and semantic equivalence judgment (Ying ctt al., [0255 Gao et al., [025]] Wang et al.) 22055) Xuejun et al.) 2025 Liu et al.) (025b),, which lacks soundness (Liu et al.] 2025a). We selected benchmarks with symbolic equivalence checkers for rigorous evaluation. For ProofNet-Hard, we use the BEq+ checker (Poiroux et al., 2025), which provides semantic equivalence verification through bidirectional entailment checking for complex logical structures. For LeanEuclidPlus, we enhanced the original E3 symbolic checker with com- prehensive three-stage pre-checks to eliminate false positives and separate bidirectional verification of premises and conclusions to minimize false negatives. We report pass@) 1 accuracy based on successful symbolic verification.
Models. We evaluate across fine-tuned autoformalizers (Kimina (Wang et al. (025), Mathesis (Xue- jun et al. 2025)) and three major model families: GPT (OpenAl 2024) 2 Claude (Anthropic 2024 and Qwen (Yang et al., 2025 B each with standard and reasoning variants. We sample 5 runs per problem with temperature 0.2 for non-reasoning models/modes and 1.0 for reasoning models/modes. Specialized autoformalizers use 1024 tokens, other models use 6144 tokens, and reasoning models have 12,288 token budgets. All models receive standardized 1-shot examples demonstrating the complete pipeline (see Appendix B for ablation).
Baselines. Since DNA consists of two phases that can be executed individually, we design a system- atic ablation study evaluate each component's contribution. Our baseline represents the standard autoformalization approach used in prior work, where models receive no corpus-specific abstractions
'GPT models: 1pt-4.1-mini-2225-00
gp=-5-min--2025-00800 000.::400000000044.4..m0mm000000 gpt-5-2025-08-07
appt-4,12225-04--
"Claude models: Soaude-4-onnet-2225500
'Qwen models: Qwen3-14B, Qwen3-32B,
Qwen33-33BB-A22P 20
Thinking-2507
7

---

Published as a conference paper at ICLR 2026
LeanEaciidPlss
Pros
Model
Bascline
Devide
Abstract
DNA
OraciaN
DNOrackA
Buscine
Diiie
Abstract
DNA
OcacicA
DNOrackA
Fire sued Model
Kaniza Aunoormalier 7B
0.0
0.0
0.0
1.1
7.4
Mathesia Astofoemallerr
0.0
0.0
0.0
5.3
5.3
Noc Reisoning Modals
GPT-4.1 misi
4.8
25.4
62
42.4
17.63x
3.0
46.8
19.05
08
0.0
53
744
10.5
13.3
GPT-41
35.2
28.5
00
10.5
23.2
Clunde 4 Sonaet
34.2
46.6
36.2
58.2
170025
36.6
60.2
00
147
12.6
26.3
Owan 148
L0
5.0
4.8
9.6
1K.00N
3.0
13.4
112.404
0.0
0.0
3.2
0.0
0.0
Qwes3
4.0
20,6
13.48x
0.0
4.2
4.2
Qwen3 2358 Irainact
43.6
45.4
64A
157.8%
775.0%
0.0
1.1
9.5
2.1
16.8
Avarags
18.7
28.9
20,9
61.6
11.17x
25.6
46.9
11.51x
0.00
0.0
3.9
7.9
7.6
13.9
Reasoting Mudals
37.0
51.2
58.8
157.W5
-90.258
0.0
12.6
28.4
Chade Sousei (Tinking))
32,5
43.4
43.5
57.4
175.0%2
30.8
64.4
196.36
0.0
0.0
11.6
12.6
18.5
30.5
(Thinkingt
30.8
91.6
192.0%
11.00x
9.5
Owen (Thinking)
31.6
39.4
40.8
137.8%
46.8
582
196.69
0.0
2.1
84
14.7
Qwee3 2158 Thinking 250
00.2
45.4
41.6
55.
136.35 99
16.4
70.4
725.11
0.0
0.0
53
533
9.5
19.0
36,5
47.9
51.1
162.29
42.9
11 103
0.0
7.9
207
Table 3: Performance comparison across model families and experimental conditions on LuanEu- clidPlus and ProofNet-Hard benchmarks. Results show pass@ I accuracy with improvements baseline highlighted in red. DNA consistently outperforms individual components (Divide, Ab- stract) and often surpasses oracle conditions (OracleA).
and directly generate formal statements without decomposition. While all models are prompted to provide step-by-step reasoning, the critical distinction lies in whether we explicitly prompt the LLM to decompose statements into our semi comi-formalized hierarchical structure.
To isolate the contribution of each phase, we systematically reintroduce individual components. The "Divide" condition activates only Phase of our framework, providing models with our 4-step statement autoformalization pipeline that includes hierarchical decomposition and self-refinement,, while operating with the original DSL. documentation without any corpus-specific abstractions. Con- versely, the "Abstract" condition activates only Phase enriching the DSL with reusable definitions learned from the corpus, but requires models to generate formal statements directly without the ben- efit of our decomposition pipeline. Our complete "DNA" method combines both phases, providing models with both the corpus- -specficcc abstractions from Phase and the hierarchical decomposition capabilities from Phase II.
To establish theoretical upper bounds and validate our approach, we include oracle conditions using human expert- wrritee corpus-specific definitions for both benchmarks. The "OracleA" condition provides these oracle abstractions to downstream models without activating our 4-step statement autoformalization pipeline, effectively testing the potential ceiling of perfect abstraction learning. The "DNOracleA" condition combines these oracle abstractions with our complete 4-step statement autoformalization pipeline, establishing the theoretical performance ceiling for our entire approach.
4 RESULTS
4.1
EFFECTIVENESS OF DNA
Our analysis of Table 3 reveals several key insights about the effectiveness and generalizability of our framework across different model types and benchmark complexities.
The DNA framework demonstrates substantial performance improvements across all model cate- gories and benchmarks. On LeanFuclidPlus, the most dramatic improvement is Qwen3-14B ad- vancing from 1.0 to 9.6 (9.6x gain), while 1P9--.1-mimn improves from 4.8 to performance levels approaching G.T-4. On ProofNet-Hard, baseline performance across all models is zero, making DNA's ability to enable successful formalization particularly striking, especially considering that GPT-5 with high reasoning effort-thh same model used for Phase language extension- ffils completely in baseline scenarios without corpus-spectins abstractions.
The framework proves especially beneficial for smaller non-reasoning models, demonstrating markable scalability advantages. The most notable improvement occurs with Qwen3- 14B, which ad- vances from merely 1.0 success rate at baseline to 9.6 with DNA augmentation, representing nearly
8

---

Published as a conference paper at ICLR 2026
Model
Divide
Abstract
DNA
Qwen2-235B-A22B-mmmmuu gpi-5-mini-2025-08-07
13.5
25.0
47.0
9.5
47.5
57.5
Table 4: Ablation on 40 complex LeanEuclidPlus problems.
10x performance gain. Similarly, GPT-4.1 improves from 8 at baseline to performance levels approaching GPT-4.1, constituting transformative enhancement for resource-constrained applica- tions. Reasoning models exhibit smaller relative improvements compared to non-reasoning models, which aligns with their inherent training for generating extended reasoning traces and decomposing complex problems autonomously. However, comparing baseline and "Divide" columns reveals that decomposition still provides substantial benefits even for reasoning-capabll models, as detailed in the ablation analysis presented in Appendix A
Fine-tume specialized autoformalizer models demonstrate complete failure to generalize across domain-specific languages, achieving zero success rates on LeanFuclidPPus due to their inability to follow instructions for generating correct LeanFuclid syntax and performing decomposition op- erations, failing even basic compilation syntax checks. On ProofNet-Hard, despite Mathesis Auto- formalizer [Xuejun al. 2025) being initialized from Kimina Autoformalizer (Wang et 2025) and Kimina being trained on ProofNet data, both models still achieve zero baseline performance. Notably, for specialized models, the "Abstract" condition outperforms "DNA" because these mod- els cannot follow decomposition instructions effectively. and the decomposition prompts actually impede their performance. These findings conclusively demonstrate that fine-tuning specialized autoformalizer models lack generalizability, and effective generalization requires DNA framework integration with models possessing strong cntructtionfollowiing capabilities.
4.2 GENERALIZABILIT OF DNA
To assess the generalizability of both our learned abstractions and decompositional statement auto- formalization approach, we evaluate Qwen3-2351 215---33--nntttrcc and GPT-5-mini, representing the best- performing non-reasoning and reasoning models respectively the 100 core LeanEuclidPlus prob- lems as presented in Table 4 to determine whether our main results extend to the 40 additional problems with greater diagrammatic complexity. The generalizability results demonstrate consistent performance patterns across varying complexity levels, with DNA (Leamed+4--stae)) maintaining substantial advantages
both Abstract (Learned+1 -ttage) and Divide (Barebone+4-stage) ap- proaches even on more challenging geometric problems, confirming the robustness and scalability of our integrated framework design.
4.3 SYNERGY BETWEEN DECOMPOSITION AND ABSTRACTION
Analysis of Table reveals a consistent synergistic relationship between our two framework phases across all evaluated models and benchmarks. The complete DNA framework almost invariably outperforms both Divide (D) and Abstract (A) components when applied in isolation, demonstrat- ing that the combination of abstraction learning and hierarchical decomposition yields performance gains that exceed the sum of their individual contributions. Remarkably, DNA frequently surpasses even the OracleA condition, which provides human expert- abstractions, indicating that our learned abstractions coupled with systematic decomposition can match or exceed the effectiveness of carefully crafted human-designed abstraction libraries.
These empirical findings validate our theoretical framework presented in Section 2 confirming that decomposition and abstraction represent complementary facets of the autoformalization challenge rather than independent optimization targets. The synergistic effect emerges because abstraction learning enriches the target language with high-level mathematical concepts that facilitate more accurate clause-level translations during decomposition, while hierarchical decomposition exposes the precise semantic structure needed to effectively utilize these learned abstractions, creating a mutually reinforcing system that achieves optimal formalization performance.

---

Published as a conference paper at ICLR 2026
5 RELATED WORK
The field of autoformalization has advanced from early rule-based systems to modern LLM-based paradigms (Weng et al.] 2025). While proof autoformalization has been employed in neural theorem proving (Jiang et al., 2023b) and LLM reasoning verification (Zhou ett al., 2024), the lack of faithful automated evaluation metrics has led most research to focus on statement autoformalization. Recent LLM-based approaches include in-context learning (Wu al. Azerbayey et al., 2023), supervised iin-ttning (Jiang et al.] 2023al Ying et al. [0255] Gao
Autoformalization.
2022
ct al. 2025), reinforcement learning (Huang et al. 2025 Xuejuun et al.) [025| Wang et al. 2025),
retrieval-augmented generation (Zhang et al. [2024] Liu et al.) 2025a). and post-inference sampling
techniques like majority voting (Li et al. 2024a) and compiler feedback (Poiroux al., 2025). How-
ever, all aforementioned works let LLMs directly generate formal statements from the informal and treat each statement in isolation, thus overlooking two important insights: (1) statements within the same corpus often share common mathematical concepts that can be abstracted and reused; (2) mathematical statements are inherently semi-structured and can be hierarchically decomposed into simpler, more manageable clauses. Our framework leverages both insights by first formalizing com- mon concepts in the entire corpus into reusable abstractions, and then hierarchically decomposing individual statements into clauses that are formalized using the learned abstractions.
Decomposition. Decomposition, the principle of dividing complex problems into more tractable subtasks, is widely acknowledged in LLM reasoning (Huang & Chang 2023). Theoretical works show that problems are more efficiently learned when decomposed (Wies et al. 2023). and generat- ing step-by-step solutions enables LLMs to tackle increasingly complex tasks (Li et al. 2024b). This principle is empirically validated across various diverse domains (Shwartz et al.) 2020: et al.
2021 Wei al.
2023) from commonsense reasoning code generation. 2023 Zelikman et al.
In neural theorem proving, decomposition has heen successfully adopted to break proof goals into simpler lemmas (Wang et al. 2023 Zhao et al. 2023 Wang et al. 2024a). However, in the context of autoformalization, decomposition remains largely unexplored. Only one recent work (Xuejun ct al. 2025) uses decomposition for evaluation purposes: an LLM judge decomposes the informal statement into premises and conclusions, and then assesses the semantic equivalence between the decomposed informal statement and the predicted formalization. In contrast, our framework the first to apply decomposition directly to the formalization process itself.
Abstraction Learning. Abstraction learning aims to automatically extract reusable knowledge from data for application to future tasks. In program synthesis, library learning focuses on extracting reusable subroutines from program corpora (Ellis et al.] [022] Wang et al.) 2024b). In theorem proving, systems learn libraries of reusable lemmas to simplify future proofs (Zhou et al., 2022 Johansson et al.) 2014: Kurashige et al. 2024, Singher & Itzhaky 2021). In LLM reasoning, tool learning enables models create reusable tools for commiin-ppciife tasks (Yuan et al.) 2024 Qui jet al. 2025). Our work introduces abstraction learning to autoformalization, where the goal is curate libraries of reusable mathematical definitions and relations. While program synthesis, theorem proving, and tool learning target executable abstractions (subroutines, sub-proofs, tools), autoformalization requires mathematical definitions that are usually non-computable, like axioms defining algebraic structures. Furthermore, unlike library learning, which requires large corpora of formal statements, our framework learns abstractions directly from natural language. To our knowledge, this is the first work to apply abstraction learning to statement autoformalization.
CONCLUSION
We have presented DNA, a novel framework that addresses the three fundamental challenges lim- iting autoformalization generalizability through corpus-driven abstraction learning and hierarchical statement decomposition. Our approach demonstrates remarkable performance improvements, with gains ranging from 1.17x to 8.60x over baseline methods across diverse model architectures and domain-specific languages. Most significantly, DNA's zero-training design enables smaller models like Qwen3-14B to achieve performance comparable to much larger baselines, while completely transforming autoformalization for challenging domains where specialized models fail entirely. The framework's ' success suggests fundamental shift toward more generalizable autoformalization ap- proaches that can adapt to new mathematical domains without extensive retraining, opening path- ways for automated mathematical reasoning across previously intractable formal language targets.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGEMENT
This work was supported in part by an AWS ASSET Ph. D. Fellowship. NSF Award CCF-2338777, Amazon Research Award Fall 2023, Amazon/ASSET Gift for Research Trustworthy AI, Indi- vidual Discovery Grants from the Natural Sciences and Engineering Research Council of Canada, and the Microsoft Accelerate Foundation Models Research (AFMR) grant program. Any opinions, findings, conclusions, or recommendations expressed herein are those of the authors and do not necessarily reflect the views of funding entities.
REFERENCES
Authropic. Claude URL
Jeremy Avigad, Edward Dean, and John Mumma. A formal system for Euclid's Elements. The Review of Symbolic Logic. 2(4):700-768, December 2009. ISSN 1755-0211. doi: 10.1017/ $17550203099900988 /0t0:///.../.......o.//////////0
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and formally proving undergraduate-levv math- ematies, 2023. IRtts:
org/ abs 2302 12433
Leonardo De Moura and Nikolaj Bjørner Z3: an efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008. Springer- Verlag. ISBN 3540787992.
08, pp. 337-340, Berlin, Heidelberg.
Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, and Joshua B. Tenenbaum. DreamCoder: bootstrapping in- ductive program synthesis with wake-sleep library learning. In Proceedings the 42nd ACM SIG-
PLAN International Conference on Programming Language Design and Implemenattion, PLDI 2021, pp. 350- New York, NY, USA. 2021. Association for Computing Machinery. ISBN 97814 9781450383912. doi: 10.1 05411444//43348334554000000
Guoxiong Gao, Yutong Wang. Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated Lean 4 dataset. In The Thirteenth International Confer- ence on Learning Representations, 2025. URL https: httpss://pppreveeeee net. forum? did=
Se6MgCtRhz
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garil- lot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Proceedings of the 4th International Conference on In- teractive Theorem Proving, ITP' pp. 163-179, Berlin, Heidelberg, 2013. Veringg ISBN 9783642396335. doi: 10. 1007/9977 0-77778---42--0- 642--36634---- 2_11_11444 httl::/t:: /ttp:////oo..oo/....
Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal proof of the Kepler conjecture, 2015. URL
02155
Jie Huang and Kevin Chen-Chuan Chang. Towards reasoning in large language models: A sur- vey. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Findings of the As- sociation for Computational Linguistics: ACL 2023, pp. 1049-1065, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10. 1/653//w/2023..iddinggs https://acl antho ogy org. 2023. nd mordiigg-ac.. 67/
URL
Yanxing Huang, Xinling Jin, Sijie Liang, Fuwen Luo, Peng Li, and Yang Liu. FormaRL: Enhancing autoformalization with no labeled data. In Second Conference on Language Modeling, 2025.
URL htttptttt///tpeeet ew.

---

Published as a conference paper at ICLR 2026
Albert Q. Jian, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization, 2023a. URL httpt::t/aaaatttt.. org/ abs/2311.0377 03755
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, 2023b. URLttts::://axx:
org/ has///b///// abss/210.... 12283
Moa Johansson, Dan Rosén, Nicholas Smallbone, and Koen Claessen. Hipster: Integrating theory exploration in a proof assistant. In Intelligent Computer Mathematics, pp. 108-122. Springer International Publishing, 2014. ISBN 978-3-319-08434-3, doi: 10. 10.1007/978-3-319-0444444
Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, and Nadia Polikarpova. CCLemma: E-graph guided lemma discovery for inductive equa- tional proofs. Proc. ACM Program. Lang., 8(CCFP), August 2024. doi: 10. 10.1145/3674653.
Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Fan Yang. Xian Zhang, and Xiaoxing Ma. Autofor- malize mathematical statements by symbolic equivalence and semantic consistency. In A. Glober- son, I.. Mackey, D. Belgrave, Fan, U. Paquet, J. Tomezak, and C. Zhang (eds.), Advances in Neural Information Processing Systems, volume 37, pp. 33598-53623 Curran Associates, Inc., 2024a. URL https::/prooceeiins..eurrrrssrre wapppp fites/papee/e///////////// File /tte://6666111111122222222222222 Con.epeeerrrooeeenecee..comee pdf
Zhiyuan Li, Hong Liu, Denny Zhou, and Tengyu Ma. Chain of thought empowers transformers to solve inherently serial problems, 2024b. URL MRRL::::s///aiiiii wttp://wwwwgg//////222.2.2 221./222222128 12875
Qi Liu, Xinhao Zheng. Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: Towards faithful metric and dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025a. URL https:
//openzeview. www. wow.:e/oooommmaa--00
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. ATLAS: Autoformalizing theorems through lifting, augmentation, and synthesis of data, 2025b. URL httth:///azxiii org/
wwwp/rgggg.......//e...eeeeeee/e abs/ 2202.. 05567
Mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20), pp. 367-381 ACM, 2020.
doi: 10.1 00.1145//37288533338844
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction - CADE 28, pp. 625-635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5.
Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Auto- formalizing Euclidean geometry. In Ruslan Salakhutdinov, Zico Kolter, Katherine Heller, Adrian Weller, Nuria Oliver, Jonathan Scarlett, and Felix Berkenkamp (eds.), Proceedings of the 41st In- ternational Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research. pp. 36847 36893. PMLR, 21-27 Jul 2024. URL https: /tttps://proceedinggs .ml.............mm.............. press/v235/ mu mprphy22 html
Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer- Verlag, Berlin, Heidelberg, 2002. ISBN 3540433767
Maxwell Nye, Anders Johan Andreassen, Guy Gur-Ari, Henryk Michalewski, Jacob Austin, David Bieber, David Dohan, Aitor Lewkowycz, Maarten Bosma, David Luan, Charles Sutton, and Au- gustus Odena. Show your work: Scratchpads for intermediate computation with language models,
2021. URL [tttttttt wwwp:vvv.ogg/o.oooooooooo wtw.////...00.0 00114
OpenAl.
Introducing gpt-5, 2024.
URL https:// .tm.aiccccmm//oo wwt...com./..o..o...... nddxx
introducing-opt--
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving autoformalization using type checking, 2025. htllhtttps::/axxiv.orrr wwwpaawwwwwww..a////a/aaaa/ 07222
12

---

Published as a conference paper at ICLR 2026
Changle Qu, Sunhao Dai, Xiaochi Wei, Hengyi Cai, Shuaiqiang Wang, Dawei Yin, Jun Xu, and Ji- rong Wen. Tool learning with large language models: a survey. Front. Comput. Sci., 19(198343), 2025. ISSN 2095-2228, 2095-2236. doi: 10.10007711100---440000
Alastair David Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Mustafa Zaidi. End-to-end verification of ARM @ processors with ISA-Formal. 2016. URL http:////pp..smmmtiicccchooooooo
Drg/CorpusID:ee 45478988
Vered Shwartz, Peter West, Ronan Le Bras, Chandra Bhagavatula, and Yejin Choi. Unsupervised commonsense question answering with self-talk, 2020. URL.
Eytan Singher and Shachar Itzhaky. Theory exploration powered by deductive synthesis. In Alexan- dra Silva and K. Rustan M. Leino (eds.), Computer Aided Verification, pp. 125-148, Cham, 2021. Springer International Publishing. ISBN 10--3-030-11888--
Rahul Vishwakarma, Kazumi Kasaura, Pietro Abbiiitne OndaNaoto, and Ziyu Zhou. lean
ProofNet-lean4, 2024. URL. http:s/s//ggtttb....cc/c////a//a GitHub repository. accessed 2025-09-24.
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. LEGO-Prover Neural theorem proving with growing libraries, 2023. [tt.:ttss://aat
aalaabs22111 00656
Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang. Jian Yin, Zhenguo Li, and Xiaodan Liang. Proving theorems recursively, 2024a. URL https: //atps wttg/bs.////ooooooeo...ooe..aere /adds//4000 2405.14414
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying. Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo
Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang. Zhengying Liu, and Jia Li. Kimina-Prover preview: Towards large formal reasoning models with reinforce- ment learning, 2025. URL httph:tttt///ttetst
org/ abs/ 2504 11354
Zora Zhiruo Wang, Graham Neubig, and Daniel Fried. TROVE:
inducing verifiable and efficient toolboxes for solving programmatic tasks. In Proceedings of the 41st International Conference on Machine Learning, ICML.'24. JMLR. org, 2024b.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models, 2023. URL https: // org. httpg//aa////.....//// 11903
Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. Aut- oformalization in the era of large language models: A survey, 2025. URL URRlhttps://axxii
org/abs/2500 25cbb./2205... 23486
Noam Wies, Yoav Levine, and Amnon Shashua. Sub-task decomposition enables learning in quence to sequence tasks. In The Eleventh International Conference on Learning Representationss 2023. /tL/tttps:
net http://ee..e.rrroaaoee/ee//////.
Yuhuai Wu, Albert Q Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022. URL https:
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prowe Prover: Advancing theorem proving in LLMs through large-scale synthetic data, 2024. htll.https://rree wttp://.rggga////e/eeooo
13

---

Published as a conference paper at ICLR 2026
Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haox- iong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao. Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin, and Zhenguo Li. Mathesis: Towards formal theorem proving from natural languages, 2025. URL
07047
An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, Jian Yang. Jianhong Tu, Jianwei Zhang, Jianxin Yang. Jiaxi Yang, Jing Zhou, Jingren Zhou, Junyang Lin, Kai Dang, Keqin Bao, Kexin Yang, Le Yu, Lianghao Deng. Mei Li, Mingfeng Xue, Mingze Li, Pei Zhang, Peng Wang. Qin Zhu, Rui Men, Ruize Gao, Shixuan Liu, Shuang Luo, Tianhao Li, Tianyi Tang, Wenbiao Yin, Xingzhang Ren, Xinyu Wang, Xinyu Zhang. Xuancheng Ren, Yang Fan, Yang Su, Yichang Zhang, Yinger Zhang, Yu Wan, Yugiong Liu, Zekun Wang. Zeyu Cui, Zhenru Zhang, Zhipeng Zhou, and Zihan Qiu. Qwen3 technical report, 2025. URL https: /tteps://atee /atpii/aaaivvv.. org/ abs 09388
Kaiyu Yang, Jia Deng, and Danqi Chen. Generating natural language proofs with verifier-guided search, 2022. URL
12443
Huaiyuan Ying, Zijian Wu, Yihan Geng, Zheng Yuan, Dahua Lin, and Kai Chen. Lean Workbook: A lcage-scale Lean problem set formalized from natural language math problems, 2025. URL
https: /wwpvvaivviv...///vv//aaaaaa.ava org/ abs 2406. 03847
Lifan Yuan, Yangyi Chen, Xingyao Wang. Yi Fung. Hao Peng, and Heng Ji. CRAFT: Customizing LLMs by creating and retrieving from specialized toolsets. In The Twelfth International Confer- ence on Learning Representations, 2024. URL httph:ttt//// httpss////ppeeeeeieeeeee net formm?id
GOveDSt 9XM
Eric Zelikman, Qian Huang, Gabriel Poesia, Noah D. Goodman, and Nick Haber. Parsel: Algo-
rithmic reasoning with language models by composing decompositions, 2023. URL https:
7/arxiv. wtaxiiv.or//bbs/22122 wwtporgg/abbaaaaaee 10551
Lan Zhang, Xin Quan, and Andre Freitas. Consistent autoformalization for constructing math- ematical libraries. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp. 4023.4 Association for Computational Linguistics, 2024. doi: 10. 11/1665//1111224emmnmm-ooo emn
URI. http: //dp://xxx.o doi wtt.....g/......551111///// 1...0.8663/1120000
p-ma in. 233
Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve 7dancewic. Formalizing the LLVM intermediate representation for verified program transformations. Proceedings of the 39th Annual ACM SIGPLAN-SIGACE Symposiun on Principles of Programming Languages, POPL '12, pp. 427-440, New York, NY, USA, 2012. Association for Computing Machinery. doi: 10. 10.1145/103666.2103799
ISBN 9781450310833.
URL
T145/2103656.2103777
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demon- stration learning for formal theorem proving, 2023. URL https::/arxiv.co wwtp:iiioorr/aa...o...aaa.s 2305. 16366
Jin Peng Zhou, Yuhuai Wu, Qiyang Li, and Roger Baker Grosse. to extract theorems from proofs, 2022. URL https:://pperew/// net www.neeettf/reeeee 82 627jGa G3
REFACTOR: Learning
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. Don't trust: Verify grounding LLM quantitative reasoning with autoformalization. 2024. URL
https: :tbps:///rxiie org/ atgg/bb///ee 2403. 18120
14

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus 3-Stage Decomoposition
Model
I-Stage Direct
2-Stage Self-Refine
4-Stage Decomposition
Non. Reasoning Models
3pt-4,1-mini-222555
3,0
33.2
gpt-4.1 2025 04 14
34.2
46.6
59.0
61.2
Claude 4-Somet--22205555555
36.6
47.8
57.0
60.4
Qwen3-14B
3.0
6.8
10.2
13.4
Qwen3-32B
9.2
10.2
17.0
26.4
55.4
59.2
63.6
71.4
Average
23.6
29.9
40.3
46.9
Reasoning Models
20--minn-0025-8-0777
58.0
60.4
70.0
71.2
gpt-5-2025-08-07
60.2
68.4
Claude 4 Sonnet 20250514 (Thinking)
50.8
54.2
60.4
64.4
Qwen3 14B (Thinking)
33.0
37.8
50.0
$1.6
Qwen3-32B (Thinking)
46.8
55.6
57.0
58.2
Qwen3 ASBB-22BBB - 2507
58.4
59.2
67.2
70.4
Average
62.2
Table 5: Ablation study on the four-step statement formalization pipeline showing cumulative per- formance improvements. Each stage adds measurable benefits: 1-Stage (direct generation). 2-Stage (+ self-refinement), 3-Stage (+ decomposition). 4-Stage (+ translation). Results demonstrate the value of systematic decomposition over direct formalization.
A ABLATION ON THE STATEMENT FORMALIZATION PHASE
Table presents a comprehensive ablation study examining the individual contributions of each component within our four-step statement formalization pipeline across multiple model architec- tures and both evaluation benchmarks. The results demonstrate that each step provides measurable and cumulative performance i improvements, with decomposition into semi-formalized structure con- sistently yielding the most substantial gains across all model families, typically improving baseline performance by 15-25 percentage points for non-reasoning models and 8-15 15 percentage points for reasoning models.
The systematic translation step shows particularly strong benefits for maintaining semantic accuracy and reducing incorrect parameter assignments, with improvements most pronounced for smaller models that benefit from the structured approach to mapping informal concepts to formal correspon- dents. The composition step provides consistent improvements in maintaining proper quantifier scoping and logical relationships between premises and conclusions, addressing significant source of validation errors in direct end-to-end approaches. The self-refinement step with symbolic valida- feedback contributes incremental but meaningful improvements of 3-8 percentage points across all model types, demonstrating the value of iterative correction guided by comprehensive semantic feedback rather than simple compiler error messages.
These findings validate our design choice to implement multi-stage pipeline rather than attempting direct end-to-end formalization, as each component addresses distinct and complementary aspects of the autoformalization challenge. The ablation results also reveal that the performance gains are not merely additive but exhibit synergistic effects, particularly between decomposition and translation steps, where the structured intermediate representation enables more effective utilization of learned abstractions and reduces the cognitive load on language models during the formalization process.
B ABLATION ON THE ONE-SHOT EXAMPLE
Table 6 demonstrates the critical importance of providing structured examples for consistent task performance across different model architectures, revealing substantial performance degradation when models operate without guided examples. The results show that models without 1-shot ex- amples exhibit significantly degraded performance, typically declining by 20-40 percentage points across both benchmarks, with increased variance in output formatting and frequent failures to adhere particularly to domain-sparn -specifcc language syntactic requirements. This performance degradation pronounced for specialized autoformalizrr models, which show complete task failure without proper formatting guidance, and for smaller general-puroos. purpose models that struggle to infer the expected de- composition structure from task descriptions alone.
15

---

Published as a conference paper at ICLR 2026
LuanEuclidPlus
Model
Examples
Baseline
DNA
DNOracleA
Non-Rcasoning Models
0-Shot
3.8
21.6
26.6
gpt-4.1-mini-2025-000
1-Shot
4.8
42.4
48.8
0-Shot
14.4
29.8
48.6
8pt-4.1-2025-04-14
1-Shot
26.8
48.4
61.2
0-Shot
10.0
30.0
37.8
Claude-4-onmne-2025500
1-Shot
34.2
58.2
60.4
0-Shot
1.0
0,0
4.0
Qwen3-14B
1-Shot
1.0
9.6
13,4
0-Shot
1.8
5.4
17.4
Qwen3-32B
1-Shot
4.6
20.6
26.4
O-Shot
16.8
29.2
44.4
Qwem3-233B-A22---ntttttt--
1-Shot
40.8
64.4
71,4
O-Shot
8.0
19.3
29.8
Average
1-Shot
18.7
40.6
46.9
Reasoning Models
0-Shot
12.8
31.8
33,4
gpt-5-mini-2025-00-00
1-Shot
25.8
58.2
71.2
0-Shot
18.2
22.8
32.6
gpt-5-2025-08-07
I-Shot
35.4
55.8
68.4
O-Shot
14.0
30.0
40.0
Claude-4SSomet-225553 20 (Thinking)
1-Shot
32.8
57.4
64.4
0-Shot
12.0
15.8
26.8
Qwen3-14B (Thinking)
1-Shot
25.4
38.6
51.6
O-Shot
18.0
25.2
34.0
Qwen3-32B (Thinking)
1-Shot
29.6
40.8
58.2
0-Shot 27.0
30.4
56.0
Qwen3-235B-A22B-Thiee
1-Shot
40.2
55.6
70.4
O-Shot
17.0
26.0
37.1
Average
1-Shot
31.5
51.1
64.0
Table 6: Ablation study on 1-shot example provision showing the critical importance of structured examples for task performance. Models without examples exhibit significantly degraded perfor- mance (20-40 percentage point drops) and increased variance, particularly for domain-specific lan- guage adherence and decomposition consistency.
The provision of comprehensive chain-of- examples serves multiple crucial functions beyond performance improvement. First, it establishes consistent formatting expectations that enable mod- els generate outputs compatible with our symbolic validation pipeline, reducing parsing errors and ensuring meaningful evaluation. Second, the detailed reasoning traces in the 1-shot examples demonstrate the expected progression from informal statement analysis through semi-formalized de- composition to final formal translation, providing concrete template that models can adapt to new problem instances. Third, the examples help calibrate the level of detail required at each decompo- sition stage, preventing both over-simplificatin that loses semantic content and over-complication that introduces unnecessary complexity.
The ablation results also reveal interesting model-specific dependencies example provision. Rea- soning models show more graceful degradation without examples compared to standard models, likely due to their training on step-by-step problem solving, but still benefit substantially from structured guidance for domain-specifee requirements. Conversely, fine-tuned autoformalizer mod- els show catastrophic performance collapse without examples, highlighting their brittle nature and limited eetrructionfollowwiin capabilities outside their narrow training distribution. These findings validate decision to include detailed exemplars in all experimental configurations and suggest
16

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus: Extracted Concepts
two distinct lines intersecting at a point in 2-dimensional Euclidean space three more distinct points being sequentially aligned on line in Euclidean plane two sets of points lying on opposing sides of a line in Euclidean plane two angles in Euclidean plane being supplementary two lines being parallel in 2-dimensional Euclidean space two angles Euclidean plane being congruent
a point lying between two other points on line segment in Euclidean plane a triangle in 2-dimensional Euclidean space defined by three non-collinear points two triangles sharing common vertex in Euclidean plane two points lying on the same side of a line in Euclidean plane two points lying on opposite sides of a line in Euclidean plane
ProofNet-Hard: Extracted Concepts
square root function mapping nonnegative real numbers to nonnegative real numbers sequence of real numbers being convergent
limit function mapping convergent sequence of real numbers to a real number
topology on a set X
family of topologies on a fixed set X
intersection family of topologies on X being a topology on X union of family of topologies one topology on X being finer than another topology on X (inclusion of collections) two topologies the same set being comparable under inclusion two topologies on the same set being not comparable under inclusion basis for a topology on set
X not necessarily being topology on X
topology on generated by the basis of intervals with rational endpoints
Figure Example result from Step Concept Extraction.
that example provision represents crucial component of any practical autoformalization system deployment.
C QUALITATIVE ANALYSIS
C.I ABSTRACTION LEARNING
Step 1: Concept Extraction. To illustrate the types of concepts extracted, we examine representa- tive examples from both benchmarks shown in Figure For LeanEuclidPlus, the extracted concepts include objects such as non-degenerate triangles in 2-dimensional Fuclidean space, relations such as two distinct points being on line, and various geometric functions. For ProofNetHard, which addresses more advanced mathematical domains, the extracted concepts span a broader range: ob- set X. families of topologies a set X, and bases for topologies
jects include topologies a set X; relations include predicates such as sequence of real numbers being convergent and the intersection of family of topologies
X being topology on X; functions include the square root function mapping nonnegative real numbers to nonnegative real numbers and the limit function mapping convergent sequence of real numbers real number.
17

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus: Filtered Out Concepts
a point lying between two other points on a line segment in Euclidean plane two points lying on the same side of a line in Euclidean plane
two points lying on opposite sides of a line in Euclidean plane
the measure of an angle Euclidean plane mapping an angle
real number in degrees convex quadrilateral in 2-dimensional Euclidean space being parallelogram
LeanEuclidPlus: Kept Concepts
two distinct lines intersecting at a point in 2-dimensional Euclidean space three more distinct points being sequentially aligned on line in Euclidean plane two sets points lying on opposing sides of line in Euclidean plane two angles in Euclidean plane being supplementary two lines being parallel in 2-dimensional Euclidean space two angles Euclidean plane being congruent two triangles sharing a common vertex in Euclidean plane an angle at vertex of triangle in Euclidean plane
ProofNet-Hard. Filtered Out Concpets
square root function mapping nonnegative real numbers to nonnegative real numbers sequence real numbers being convergent
limit function mapping a convergent sequence of real numbers a real number family of topologies on fixed set X intersection of family of topologies union of a family topologies on not necessarily being a topology on X
X being topology X
basis for a topology on a set X
connected topological space (no separation into two disjoint nonempty open sets)
Stone-Cese compactification BX of completely regular space
ProofNet-Hard: Kept Concepts
sequence of real numbers defined by a_ sqrt(i
sqrt(i for in the natural numbers
subbasis for topology on set X
lower limit topology R on the real line (topology with basis half-open intervals [a.b))
K-topology 3 K_K on the real line topology on R generated by the basis of intervals with rational endpoints
sequence of functions f_: [0,1] - K defined by f_n(x)= = x"n
pointwise limit function [0,1] - R with g(x) = for 0 < and g(1) = limit point compactness (every infinite subset of X has limit point in X)
uniform topology on [0, 1 induced by the supremum metric
Figure 3: Example result from Step Concept Filtering.
18

---

Published as a conference paper at ICLR 2026
Step 2: Concept Filtering. The filtering behavior and results vary significantly between two benchmarks due to differences in the richness of their underlying formal libraries.
For LeanEuclidPlus, shown in Figure 3, the minimal nature of the target results in relatively few concepts being filtered out. Representative examples include the concept of a point lying between two other points on line segment in Euclidean space, which is filtered because it corresponds to the primitive relation between axiomatized in the target DSL. Similarly, the concept of two points lying on the same side of a line is filtered because corresponds the primitive relation Point. simeSi de. The relation describing two points being on opposite sides of a line is also filtered because it already exists in the target DSL as an abbreviation expressed as a. onLine 1 A b. onLine 1 A - sameSide a b 1.
In contrast, ProofNetHard exhibits substantially more filtering activity due to the exten- sive coverage of Lean Mathlib, as illustrated in Figure 3 Concepts such as a sequence of real numbers being convergent are filtered because they have direct formal correspon- dents in Mathlib, specifically the filter limit Filter. Tendsto f atTop (nhds 1) de- fined Mathlib Sohnii/TTopology" Instances/Real. The concept of a family of topologies on a set X is filtered because it is already represented as Set (Topologi capacce X) or as an indexed family & -> Topologicalspat Mathl bottlibbTie wtt.ii/eooy///aaaaeeeeeeeeeeeeee BBasiiiigg. Even sophisticated mathematical concepts such as the Stone- Cech compactification of a completely regular space X are filtered because Mathlib provides com- prehensive support through StoneCech along with the unit map stoneCechUnit and exten- sion operation st stoneCechExtend in Mathlib/ WathlibbTopology. / SSenehh...
X with complete lattice operations in
Step 3: Concept Dependency Graph (CDG) Construction. For LeanEuclidPlus, Figure presents an example of a depth-3 CDG where the target concept to be formalized depends on both already-availlale formal definitions in the target language, such as Driangle.offoint: offoints and Line. erstetssetts.... LLine, as well as other concepts that do not yet have single direct formal correspondents and must themselves be formalized first. An illustrative example of the nuanced dependency analysis performed in this step involves the concept of a point lying on a line segment including endpoints in the Euclidean plane. This concept is superficially similar to the previously fil- tered concept of point lying between two other points line segment in Euclidean space, which was removed because it has a direct formal correspondent in the primitive relation between, How- ever, these concepts are semantically distinct: the former permits the point to be endpoint of the line segment, while the latter does not. Consequently, the former concept is retained and can be formalized using between, logical disjunction, and equality. The dependency analysis also correctly identifies that the concept of the line through two distinet points in Fuclidean plane is di- rectly expressible using Point. onIi ne, inequality, and existential quantification. The concept dependency for a line intersecting two sides of triangle in Euclidean plane is similarly constructed correctly with appropriate dependencies identified.
For Hrard, Figure a simpler depth-2 CDG. The example concept of the lower limit topology on the real line, which is the topology with a basis of half-open intervals [a, b), demon- strates correct dependency construction. The analysis correctly identifies that this concept is di- rectly expressible using the following formal correspondents: Set (Set R), Ico caggicalppacce GenerateFror Set (Set R) -> Topologicall Space IR, existential quantification, conjunction, and equality to describe the generating family. This concept dependency is correctly constructed and precisely matches the oracle definition of the lower limit topology written by human experts, vali- dating the accuracy of our dependency analysis.
R -> Set. RR representing half-open intervals [a, b),
Step 4: Concept Formalization. For LeanEuclidPlus, Figure 5 iillssraates the formalization of the concept of three more distinct points being sequentially aligned on a line in Euclidean plane, along with several helper definitions. The natural language description of this concept encompasses multiple sub-concepts: mutually distinct points, collinear points, and points aligned in sequential order. The language model correctly decomposes the formalization task by first formalizing each of these sub-concepts as helper definitions, then composing them to formalize the target concept. While this approach is correct and faithful to the original natural language concept, it introduces some redundancy that will be addressed in the subsequent refactoring phase.
19

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus: Concept Dependency Graph (CDG)
Concept [Needs Dependencies]
line intersecting two sides of triangle in Euclidean plane
Concept [Directly Expressible]
Concept [Directly Expressible]
point lying line segment (including endpoints) Euclidean
the line through two distinct points in Euclidean plane
plane
Formal Correspondent
Formal Correspondent
Formal Correspondent
Triangle.ofPoints
between
Point.onLine
Formal Correspondent
Formal Correspondent
Formal Correspondent
Line. intersereseeenne
Formal Correspondent
Formal Correspondent
ProofNet-Hard: Concept Dependency Graph (CDG)
Concept [Directly Expressible]
lower limit topology R_ on the real line (topology with basis of half-open intervals [a,b))
Formal Correspondent
Formal Correspondent
Set (Set R.)
TopologicalSpace. Gerireeeeeerrtterroome Set (Set R) TopologicalSpace
Formal Correspondent
Formal Correspondent
Exists (3), conjunction (A), and equality (=) to describe the generating family
Ico R Set (half- open interval [a.b))
Figure 4: Example result from Step 3 CDG Construction.
20

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus: Formalized Concepts
@ @[smmp]
def distinctFromList (x Point) (ys List Point): Prop match with
D => True
y ys x # y distinctFromList ys
@ [Simp]]
def pairwiseDistinct (pts List Point) Prop match pts with
[ => True
X xS => distinctFromList xs pairwiseDistinct xs
[simp]]
def allOn (pts List Point) (L Line): Prop
match pts with
0
True
X xS x.onLine allOnLine xs
simp] def betweennessChain (pts List Point): Prop := match pts with
a :
rest => between c betweennessChain (b :: c :: rest)
True
@ [simp] def sequentiallAAlignedOnniin (pts List Point) (L Line): Prop ==
ainOnLine pts pairwiseDistinct pts A betweennessChain pts
ProofNet-Hard: Formalized Concepts
@[simp]
def ToploogicaSSpcce.comaaaaeee {a Type*) (t TopologicalSpace a) Prop :=
tsuvust
@[simp]
def TopplogicaSpace..noCCmpaaaalll (a Type*) ut TopologicalSpace a) Prop ==
TopologicaSSpece.ccmppaaaae
@ [[simp]
def IsSubbasisFor (X: Type*) (S: Set (Set X)) (t: TopologicalSpace X) Prop :=
Type" == TopplogicalSpccc.geeeetfeeer S
@ [[mmp]]
def loverLimilGeeneralnggesss Set (Set R) =
(U 3 a b: R, < = Set. a b)
@ [Simpp]
def LealLooor Tpploe =
Figure 5: Example result from Step 4 Concept Formalization.
21

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus: Refactored Formalization
@ [iimpp] def betweennessChain (pts List Point): Prop match pts with
a c::: rest between b с betweennessChain (b C rest)
True
@[simp]
def sequentiallyAlignee (pts List Point): Prop := betweennessChain pts
ProofNet-Hard: Refactored Formalization
[[impp]
def TopopagieSComparable (a: Type*) u TopologicalSpace a) Prop u v
@ [imp]
def sSubbasisFor (X: Type") (S Set (Set X)) (t: TopologicalSpace X): Prop :=
t = ToppoogicaSpaccegeeeeaataeee generateFrom S
@ simp]
def Lower LowerLiiittubbarrttecc Set (Set R. =
{U b R, a Set. b)
@ @[simp]
def TepeerryyTTpologo TopoloiccalSpcee R gewerateFrormrmmmmmmmmmm Lobbibss
Figure 6: Example result from Step 5 Formalization Refactoring.
For Proo/NetHard, Figure demonstrates the formalization of concepts with their helper def- inition dependencies. The formalization of TopologicalSpacee notComparable de- pends on and utilizes TopologicalSpace. Comparable as a helper definition. Similarly, www.iiiepoolloooooooo.....e real rLimi Tepology depends and uses
as helper definition. Both the main concepts and their helper definitions are correctly formalized, demonstrating the system's ability manage dependencies during formalization.
Step 5: Formalization Refactoring. For LeanFuclidPlus, Figure O demonstrates significant refac- toring opportunities. As shown in the initial formalization in Figure the concept was implemented using multiple helper definitions for mutually distinct points, collinear points, and sequential align- ment. However, careful analysis reveals that the chain of betweenness relations already guarantees that the list of points must lie on the same line and must be mutually distinct by virtue of the between relation's semanties. Consequently, the two separate helper definitions for collinearity and mutual distinctness can be eliminated as redundant. The refactored version shown in Figure 6 consolidates these concepts by retaining only the essential betweennesse eschhash definition, with sequentiallyAligee
serving more intuitive alias for the same concept.
For ProddNedHard, Figure 6 shows more conservative refactoring activity. The definition Topologi ca 1pacee. not Comparabee is removed because it is simply the logical negation concatenated with copplooiccalSpacee.....oo... Comparable making a separate API unnecessary and potentially confusing. The refactoring also includes renamings that improve domain speci- ingSes is renamed to LowerLimitSubler
ficity and clarity: better reflect its mathematical role, and real wiw.wee.iitttteeeeee....
is renamed to
22

---

Published as a conference paper at ICLR 2026
LeanEuclidPlus: Updated Documentation
def
(L : Line) (i Point)
two distinct lines and M intersect at point i, i.e. L M,
lies on both L and M, and LLinntersectsLine M"
The syntax is TwoDistictLinessneeeecccPPP
L M
def sequentiallyAAiggned (pts List Point)
a list of points sequentially aligned (ordered collinear chain) iff every consecutive triple (pi, pin,, pa) satisfies "between pi p pi:
No extra line or global distinctness is required beyond betweenness.
The syntax is sequentiallyAligned [pe, p., Pa, ...]'.
def sequentalllyAignneeTTTeeOOOOM (pts : List Point) -
like sequentiallyAlignedd, additionally requiring the list to contain at least three points.
The syntax is sequeentallyAligeeeTtrreeOOOO [po, pi, p.....]
def twoSetsOpooinggddeeSnniii (xs ys: List Point) (L Line)
two lists of points lie opposite sides of line L: (1) no point from either list is on L; (2) every cross-pair (x E xs, y E ys) on opposing sides of L. The syntax is twoSetsOpposinSSideSOnni.. [x., X;, [y,, y:, ...]L..
def supplementaryAngles (a d e Point)
angles L atbic and z dre:f are supplementary iff (4 a:b:c) + (4 d:e:f) L.
The syntax is "supplementaryAngles a fdef
Figure 7: Example result from Step 6 Documentation Update.
sorgenfreyTopology using the conventional mathematical terminology. While these refac- torings are strictly necessary for correctness, they enhance readability and align with domain conventions, and we therefore consider them correct refactorings.
Step 6: Documentation Update. For LeanEuclidPlus, Figure 7 illustrates the selective docu- mentation approach employed by this step. The internal helper definition betweennessChat not directly exposed the documentation; instead, its more intuitively-named alias sequent aenuentiallnn aetiilllllllll gned is presented to users. The natural language description correctly cap- tures the formal semantics of sequentiall innggiggned, attending to subtle but important details such as the fact that the points are mutually distinct. This demonstrates the system's ability to abstract away implementation details while preserving semantic precision in user-facing documen- tation.
For ProofNetHard, we adopt a different approach due to the scale the original Lean Mathlib documentation, which exceeds far beyond the context limit of any current L.MMs. Instead, skip the documentation update step and directly use the compact refactored code (comprising just formal definitions) documentation for downstream tasks in the decomposition phase.
C.2 COMPARISION BETWEEN LEARNED AND ORACLE ABSTRACTIONS
We present qualitative comparison between the abstractions Iearned by system and the ora- cle abstractions hand-crafted by human experts. Figure g illustrates representative examples from LeanEuclidPlus, and Figure 9 presents corresponding examples from ProofNet-Hard. Our analysis reveals three distinct categories of learned abstractions.
Correct Overlapping Abstractions. The first category comprises abstractions where both the learned and oracle definitions capture semantically equivalent concepts, albeit with different naming conventions or slightly different formulations.
23

---

Published as a conference paper at ICLR 2026
LeanEuctidPlus: Correct Overlapping Abstractions
Learned Abstractions
Abstractions
@(oimp) dal belweernesshhhh (pts Las Point): Prop
@[eimo]
sequardalyiignedd (point List Point) Prop match goint with
: rest =a belween b betweernesChhh :rees) True
=0 True
-> True
@leimpl
a 6: o reel secuentillyAAgnne A.
def scquentallyAignec (pts List Point) Prop.= betwoemeesschhin 205
anquentilllAiignadll ist (b rest)
[[simg]
[[simp]
abtrev InseintereecA//ot (11122 Line)
Line) Point): Linnline LintersectslLiee
Point) interrsectsuiee LonLine
Sttimpl
parallel Linel:
paralla (L M: Line): Prop
-I intersectsLine
M.M. A Intersectstine
@[eimp)
aborev perpendiculer (L1 L2:12:: LinLine)
del perpend culanA M. Lina) a o: Point): Prop
(p1 p2 Point) Prop
LittersectsLine me tomKeztinankoggaa a L.M A arod)
twounesrtosses//Po 1 pl.onLine x Apt A #i p1xp2=
@(sirp)
manglesSiimiarr
Prop
[]amm [Triangle
edit)
Triange
BII/ (D DD-Ej=Re
(la-bil [d--ei) (Iib-Cl)/ 01o-0 [[e-[]) (Io--)) (((-0))
KB-CII KE [C-M] KF-O
[C-AI]/ WF-DY (A-B) (D-E)
ZABCC DEF A.ACB BAAAABADDEEKBBAGSSBBBAA
LeanEuclidPlus: Correct Non-Overlapping Abstractions
Learned Abstractions
Abstractions
@ttsmpl del noneOnLine (pts List Point) (L: (LnLine) Prop match pla with
@lsimm)
portieeincFFomm (a Point) [point_lit Point) Prop metco point jist with
xx:: LinoLinne L noneOnLine xs
[]]
=> True
[
poinDhisinsFrommiis
@tsimo)
@Staimp)
Miluus: [ List Point):
del SilOpreingSddesPPPoiiii (x: Point) (ys Point) (L: Line:: Prop.-
metch point list with
match ys
8: rost pointDetnniirommit nest
-> True
ly xoppeinggSees y elll@pposingiideeeeeeoooo
@Usimo)
@xssmp
(point_list: Point)
parvisskorosspppeen
Point) (L: Line):
metic point list
malch with
[
Thue
xx: alOoggoingSSdee Soreeeinggitseettnntttttt
[] => True
peinesenccceesppgooooooo Oppciing xs yo
6. => a.samaSide
2: 2:B.:..: ::::::::ee res: aisameSide b sameSiceList Ib p. rest)
@isimo]
Sisimpl
Sterey sameS deDitinnDttt in (paint list List Point)
del wwsSettopppsnngiideeeeo
(xe ye Liet Point)
(L: Line): Prop
sameSideList point list muuuuatyDistnnaPoinss ist paint
naneOnLine noneOnLine
peiiwiseecroessOppee Oppoeing
extsmp!
del IneCutsTrinngeed TrngtannnnnneeennnCCCC
Point) (AB BC CA Line) Prop
eaangieei c BC GA batwoon pb betwoon p.onLine L. q.oniine L
Figure 8: Comparision between Learned and Oracle Abstractions for LeanEuclidPlus.
24

---

Published as a conference paper at ICLR 2026
For LeanEuclidPlus. the learned abstraction @eetwenneesshaain and its alias sequentiallyAlic gmed correspond directly to the oracle's sequential.LAAiigmeelll. both encoding the property that consecutive points in list satisfy the betweenness lation. Similarly, Innoiinnnnntesectttttt..
mirrrs the oracle's and the learned parallel and perpendicull artt. definitions align precisely with their oracle counterparts. The learned trianglesSim lar captures the same geometric concept as the oracle's similar abbreviation, encompassing both angle equality and proportional side lengths.
For ProofNet-Hard the learned SuctDff exactly matches the oracle's fune- tion g, both computing the difference between consecutive square roots. The learned LowerLimi t.Subaaiis sorgen fryTTool ogy, KNatRecip, KTopologySubbar and kTopo logy correspond semantically to the oracle's citer__mmit_tttt ogy, K, and k_topology.
These examples demonstrate that our abstraction learning phase is able to recover most of the com- mon mathematical concepts identified by human experts, validating the effectiveness of our auto- mated approach for discovering domain-specific abstractions without manual intervention.
Correct Non-Overlapping Abstractions. The second category consists abstractions that are correct formalizations of the natural language concepts but do not overlap with the oracle.
For LeanEuclidPlus, the learned abstractions include noneOnLine, which recursively veri- fies that point in list lies checks whether all points in a list are on opposite sides a line relative to a reference point. The learned pair www.wwsserrrssspppoo provide compositional predicates for reasoning about point configurations across lines, while l LineCutsTrl ang eOnABamdACAt encapsulates the specific geometric configuration where a line intersects two sides of triangle. In contrast, the oracle for LeanEuclidPlus contains dif- ferent abstractions such as pointDistinctt romList, mutuallyDisssomm www.llyDssitttooiiiio sList, sameS distist, and sameSideDistinees predicates over point lists.
given line, and m.Lopposingiidessooooiio
which
and
which focus on distinctness and same-side
For ProofNet-Hard, the learned abstractions include StrictlyyoonddeAAoveee generic predicate for sequences bounded by a constant, Topologiescomparaa for comparing topologies, NestedCl caeeelleppeN Intemmeemptyy for reasoning about nested sequences of closed sets. The oracle involves different abstractions such as is topology, a first-principess definition of topological structure, and countably_comm countable compactness.
and NestedC1 NestedCClosd:Noreeee osedNonempty along with
which directly encodes the definition of
These non-overlapping abstractions illustrate that concept extraction by humans and LLMs from the same natural language corpus be complementary: each identifies valid abstractions that the other may overlook, suggesting that combining both approaches could yield richer and more comprehensive libraries of reusable abstractions.
Correct Learned Abstractions, Wrong Oracle. The third category, observed exclusively in ProdfNet-Hard, consists of cases where the learnd abstractions correct while the oracle ab- stractions contain semantic errors. The learned IsLimi tooint correctly defines a limit point (accumulation point) of set A point for which every neighborhood intersects A (x). and PwwtttPonnttpppccccccc correctly states that every infinite subset has such a limit point. However, the oracle's limit __otttt_________ cettt__coppcttttett incorrectly uses ClusterPt (P U), conflating the notions of cluster point and accumulation point.
In Mathlib, ClusterPt X defined as NeBot (N x n F), which for a principal filter reduces to checking whether z E U. Crucially, since any point E U trivially satisfies ClusterFt x (P U) (every neighborhood of x contains x itself and hence meets U), the oracle's definition degenerates merely asserting that U nonempty-4 property that holds vacuously for any infinite set. This renders the oracle definition trivially true every topological space, including infinite discrete spaces where the correct limit-point compactness property provably fails.
25

---

@[simp] Published as a conference paper at ICLR 2026
ProofNet-Hard: Correct Overlapping Abstractions
Learned Abstractions
Oracle Abstractions
(/simol
[[simp]
def sertSwodDiff (n: N):R R.=..=
g (n:: : sqri -
Real.sort ((n: R)+ 1) Real.sgrt (n: R)
@teimp]
[g/aim]]
daf lower limit topology (X Type! (Preorder X]
def LowerrLilllSubbsss (Set a a R, a A Set.cco a
TopologicalSpace generateFrom (S Set
3 a a a S Sel a
@/simol
@[simp)
sorgenfrey Topology : TopologicalSpace
cot K: Sel ( (r]an::N.r=
SppologicalSpace
Spw.cpeeeeeeeeeeroooggoo generateFrom LowerLimitSbbasis
@laimp] eppology
@isimol
(S Sew.giaaSSaegggeereeeeooo
KNaiRedip:
aab.a<ba
[x] n PNat, x (1: R)/((n ()) K))
Set <b Set
@Baammo] KTopologySubballl Set (Set
[U]3 a R. (U loo
v U Set.loo b KNatieccip)
Isimol
KTopology TopologicalSpace
TopologicalSpaace generattFrree KTopologySubbasii
ProofNet-Hard: Correct Non-Overlapping Abstractions
Learned Abstractions
Oracle Abstractions
@[temm]] Bynddyy (o: Type")
@[simpp
del is lapology (X: Type") Set (Set Set.univ
(8 :NNN a) (o:00 a): Prop
s. -ITTTT--ttTT)
V n
s. (v LET) SelsUnion T)
@dsimpp
Copooagies (a: Type")
def countably compact (X [TopologicalSpcca
u: TopologicaaSppace a): Prop
Set
tsuvusi
(V IsOpen (U (J) ((Satuniv: Set X) U Uii))) UI) t: Finset (Seluniv: Set X) UiE U
@[simp]
def Neeeeeeeeehsss (X: Tyge")
TTopologicalSpace X] (C NN Set X): Prop
Antionne A N.N, laClosed n))
A Nonempyyyy
@[simp] def NeweeeeeDSsseeeeeennneeeeeeeeeee
(X: Type")
[Togologica/Spacce X] Prop (C:
X),
Antitone
[V myn:NN IsClosed (C n))
[V N.N. (C Nonempty
n, Nonemptyyy
ProofNet-Hard: Correct Learned Abstractions, Wrong Oracle
Learned Abstractions
Oracle Abstractions
PaLimpPoint (X: Type") [TopologicalSpace (A: (x: X): Piop
@[simp]
(Bsiimp) del limit point compact (X: Type") Topoloogcalpopeeeeeee X] Set X, Infinita ClusterPix
(U.n Nonemlyy
@(simp]
LimitPint (X: Type*) [ToolooicalSpace Prop VA: Set Infinite
Figure 9: Comparision between Learned and Oracle Abstractions for FroofNet-Hard...
26

---

Published as a conference paper at ICLR 2026
This example demonstrates that automated abstraction learning by LLMs can sometimes produce more reliable results than manually constructed oracles, particularly in domains where the formal- izations contain subtle semantic distinctions that may escape human review.
C.3 HIERARCHICAL DECOMPOSITION
We present a qualitative analysis demonstrating the effectiveness of our hierarchical decomposi- tion approach (Section 2.2 for autoformalization. Using learned abstractions on LeanEuclidPlus, we compare direct formalization (Abstract column in Ta- ble against our four-stage decomposition pipeline (DNA column in Table 3 on a representative problem.
Instruct-2507 with
Informal Statement. The English statement describes two triangles TUW and VSW sharing vertex W, with lines SU and TV intersecting at W. Given that W lies between S and U, and between T and V, along with the premises angle TUW angle UTW and SV | TU, the goal is to prove angle V angle S.
W
T
V
S
Figure 10: Diagram for Parallel-17 in LeanEuclidPlus.
The following is the complete reasoning trace produced by Qwen3-235B when formalizing directly without hierarchical decomposition:
No ase given an Bnglish atatement invelving two triancles, rUN and VEN, shazing point H. The lines au and TV also and given Wancle TUK
intorsect H, Mangle DIM (L.e.y Lao angles Leiangle ase congroent),, and Chat parallel arw Lo prove that Margie V. Vaanol s.
1ics
Iel's break Chis step by atep.
1: Identify pointa, lines, geanstric entities
Pointa montioond:
T. U. -- cozm triangle TUW
Suom telangle
point
Lines: SU and 7V intersect at X
liwe beixeen S and U. >. beikewn S
lies betseen
beiveen
Linws Lo defines
Foz cziangle IUN; sidea IU, ON, WT
triangle
Linw 80c containa ina
Line TW: containa and V
Wangle 7U% Vangle UIW
Veanle TOW la the angle at in triangle TUM: Mangle TelleW
Vaangl JTW ls the angle at. in Lxiangle TUW: Vhangle 0:7:90
(Vanngle
WVangge UETEN:
39
SV in the lioe Chrough and
7T is the line through and
parallel (1ine 8V) [lire
Ne asw proves Mangle
Mangle
Vangle V. likely neans the ang le an V. in tmiargle vewe Vangle BeMeet on Vangle WcM:8? Vaangle Iw likely neans the angle
triangle vews Wangle ViSril Vangle W:
Not notes triangle VSK has vertices V, 5, N. Soz
27

---

Published as a conference paper at ICLR 2026
Vannll trianole VEW la Mangia B:V:M Vannle 5 in triancle VEW is Vinngs V:S:M
IMancle 8:VeN) iMannle V:3:M)
aut xait -- is tast necoscartly true? Lot's sec.
Aiternatively, could Wancle and Viagll refar angles different trianglas? are TOM and VaN.
triangles
Giver that BV II TE, and lines EU and TV intersect at H, this looks 1ike conficuration shere two lines cross pussibly forning ainilar Lriangles
of pacallel Lines
usind propertioa of parallel linea and transvozsals.
aut the conclusion is Vlanll V Mangie S -- L.M., two angles at V. and 8, likely in Lriangle VSA.
Mais if II TV, and and 80 are Cransveraals intersecting at M, then we night use alcernate interior angles or cocrespenting angles.
But Vlnnll V Mangle triangle VaN as Lsosceles at
both Lriangle vew Mangle 5:V:M Mangle VeStK, that sould
3ut lasls cwexanine.
Alternativaly, could Wancle maan Vaanll NVB and Wangle moan Vingla WBV? Yoa that"s the name as above.
conclusion isz in triangle VON, Mangle at equala Vangle briangle VSM is isosoe les with 5X (MM1?
Not the uxiion is just Vangle Vangle 8, Fiery angle equa" equa
vo aze to proves Mancll B:VeN) IMaanll V:B:N)
BuL given:
Vangle T:U:N Vlangle Mangle at ds Vaangle T:lla triangle
isssceele let's see:
Mangle at 7: Vlangle U:T:R
If these equel, then in triangle le TUG, angles at T and 3. equal sides opposite eguil +>
leaxceles
Also givent BV 11 TO
intersect at N, with V. between and U, and between V.
do the con contiguration lat tau lines (BU and TV) insecaeos at H, forming an *X", and two segnents; : TU and 8V are parallel, wish 7.0
side, S.V the other.
This classic setup for sinilar txiangles or asing parallel 1ine angle propect
New, since av It th, and TV is cransversal (Fron T. to paxsingg through W), thens
Vangle UTN Vangie might alternate interior anglos? let's sec.
Maie - transversal 1. TV croases parallel lines TO and SV.
the patallel lines.
Traneversal TV: intersects TU at Ty and BV at V.
at point angle ketwezn
Wangla UITIN (since is TV beyond Wait batweon and
V, s0 tron to Vi T-N-V.
Hine TV: I
Simi larly, 80:
TV tron to SV tron to
Giver BY 11 FJ.
transversel
TU and BV
So the angle at between TU and TV Hiee. Vtangle between TU and IMI is Vangle UTT:
the angle between
(i.c., betweer VKI but direction mattore.
Sincr SY II rJ, and TV is a transversal, thon:
- Vlangle UTM lat II and Vinggl SVM (at Vi are correeponding angles? de alternate?
Lot's dafine disections.
Assuma standard contiquration: lines and sv are parallel, cransversal TV qoea from I co. V, crossing both.
Then Viangle between TU and at T, and Vangie between EV and TV it aze on the came side, they are corresponding.
But need zelate the angles.
Alternativoly, trensversal SU: from 8 to U, crosses SV at 5 and TJ at U.
at anglo between and +> Wangle T:31l (since W is SU beyond No.
and
feom to
28

---

Published as a conference paper at ICLR 2026
3o at U: Line 20 and line s0 mest at I anole Vangle 1:0:M
9: Line and 1ine
angle Mangle V:8iW
Since By II IJ, and SU is transvereal, then: Mancle T:U:M and Mangle Via:W are cozrespondiag anglea -> they are equal.
Boz Vangle
Mangle ViB:W
act xe are diven: Vizngi I:U:K Mangie 0:2:W
Boz Mangla
Mangle Via:W
Now, look at transversal TV: from Co crosses TU at F and V.
5: angle between and TV Mangle
AE V: angla batwoen SV and TV -- new, deponding on diraction.
II TJ, csrrespendina?
tranaversat, then Mangle
Vangle B:V:l are alceznate interior anglea?
below, TV going Then 2t angle between TU (left-xighti and IV (dowa) -- say, lower right angle.
Let's suppose lines oriensed that and By horizontal,
V: angle between (left eaght) and TV (up) upper right angle.
These alternate Interior angles -x eiuel.
Vannlo U:IEN Vangle
ThereCusw: Mangle BrVeN
Mangle U=T:H Vlangle TeDeM Vannle VrS:M
Mangle SeVeR Mangle VeBeM
Thas, triangle VSN, anglis and
Vaangle V. Wangle
conclusion luz (Mangla B:VsM) (Mnngla V:S:M)
Now Sarmalia Lise.
#+ 2: Declare all variables
Pointa: 7, 0, N, V, Linee:
For triangle TUM; rU, UM, Nr
tstangle VEM: vs,
Line SU: contains and
Fire TV: onntwina and V
Line through
(uM line through g and m
line through N
through
SW: Line through 3 and
WV: Line through 1| and V
through
through
3ut rote: 30 and TV are alzeady menticned.
express:
formTriangle I0 WT
toumTciangle V vs SM WY
Noo0itLietLinssseeeeeeeeee between
intersect K, distines
setween T v
Vianle I:U:M Vianli UITIM -> (Mangg T:U:0) OManngi 0:710) sy parsilel (1ine throuph (1ine shrough and Conciusion: IVaangee
M'nange
3ut No most oetine the lines.
assign: (T x 5 Pointi
(TU UM WI : line) for triangle TUW
WV 1inc) trianzic
Line) ter interseczing
aut note: S0 most be the line through 3 and 0 -- but NO aiso have SKi and NUB Not necoscarily.
SU, 3ct given that SD and TV intersect, at and la between and U, and between F and V.
to ensure 5,
collinear on
can dotine:
29

---

Published as a conference paper at ICLR 2026
through
and
IV: Line thzough I and V and 25 on it
the txiangle decinitiona: cesangie IUM:
14nes UN,
But is part or SU2 Not nocessarily -- unices 0, N, 5 are collinesr, which they are -- since in on SU and between and U.
points 5, aew collinear
similarly, 7, N, V aze collinsor on Line TV.
ve can define:
Line IU: through I and U
Line UK: but and are on aU -> UN La pazt of S02 But need 1ine foz side ON of Ceiangle TOW.
But "foonfeiangle', on need three distinct lines AB, BC, CA.
3o for triançle TUK:
side line 70
aide
ase on so 1ine muat same line Only U, ccllinear -- which they aze.
cannot
that line is the
anlesa define it.
But in Surnelisat isation, we can l
line UM be the same as line BU? But 30 contaira M, 1. line Chrough O and H in the sane as 1ine
But in Lean, lines aze axtensional -- if two lirea have two points in cormon, they are the sane.
Cosmal system,
assigning labela.
So co avaid fociani we should de def
Imt Line 30 be Lhe line comtaining 8 and U. and aince M is beLween: and D, M SE.
triangle TUM, needs
Line
"Formtriangle
T and I on TU
and it UM
5o UW must be Tiee containing if and M -- which SS0 does.
Larly, tor triangle and on again, S and 8 acm on 8U? No
5 and M on SM
S and W aew on SU, but and S are on SU.
different line.
Wai: triangle VSW:
-V and 1ine
an and on 1ine
but ase on.
part SU
Buz it sllowes Not fornel system, we can have pple rames for the zame Tine, "Forntriangle" we need to assign specific Lines.
line SW
co sate, xe
Line S0: contains 5, N,
Line TV: containg T, N, v
Line contains
Line containg
but and T are on TV eo is part of Line WV: contains V also on TV
tine NT: contains
tngleg
IU: line 70
(uM Line SU isince and W on 50)
isince
Similorly, tor triangle VSW:
VS: Line vs
line 18 and SU)
So ve can couse linee SU and IV in both triangles.
must ensuxe that linas axe
triangle.
For triangle TUW: lines IU, SU, IV most he distinct
For triangle lines
distinct
We are not told they are distinct, but in typical confiquration they are.
But the "Ianntriangle" predicate zequizes the thaee lines distinct.
So vo must assune that.
similarly, Exotietiiecciinsttteeessss
requizes ie TV.
30

---

Published as a conference paper at ICLR 2026
letta wxice the statenenc.
Step 31 promises
Ke need:
WT
But 3M 10 90, WI la TV so:
-> fornIrianglc 7 U su
20, su,
Hoaning:
-T and 0 70
TV
And TO, S0, TV distinct.
FornTriangle
90,
=> formIriangle V su
Argunemtis: V, 8, 98, 80, Heaning:
and H on 80
6 and V on TV
distinct.
discinctPoint aOnLine 8 SU to ensure 8 and D aze distinst and on BU But "forntrll angle already requi dist Foct badnlddn for each side? amquises distinut points di Poi sOnt ine b.c. RC
backs "IonnSriangl distinet Poriinneeooaaonntiie
distinel innt CA
So Formtriangle
distimeLPuian auiat 70
di et not Poi soaiitatnti
Simi larly for V. 5 W. VS S0 TV:
dist mot innt V. VS
-dsstintt Pot.nnoooon
di Porl sdnd fine
distinctness pointe Lines.
also need Chat belveen
between
between
5. betveen X
givex: SU 1- TV
intersects at
But "Forntciangee" al rlred requi ree it on 50 and W on TV?
dictinceeointeonlinn su and IV, gives they are
"twaDietincttines teeetttt reed.
at
resundant? Possibly,
I- which might implied othervise.
So include it.
Wangie 7:JEN Vaarle IVlangie T:U:N) (Mangi U:I:N)
87 11 TU
VS 1ine), is 1ine
paraliel
Conclusion: Vingie S:VIK Mangie VISIM
(Vaanal S:V:N) (Mangla
Note: Vangie SIVER is the angle at V. in triangle VSM: points 5, V. W so vertox V. with and on the sides.
Similarly, Wanglo ViS:N anglo points
vartox
30 vo need to output:
Wiforall
Point)
[prenises] (Mangle S:Veltt (Vaangle
Viaski
But xait -- triangle VSW, xe used lincs VS, SU, IN.
But 50 is used for 3H, IV for WV.
angle at Wangle this requites peints 3, M.
31

---

Published as a conference paper at ICLR 2026
aimilarly, anglo at S: Mangla ViaiW - points V, Sy M.
have
aut in the prenises, we have tormiriangis V s VS SU TV -- this ensures that: and on vs
and
3o the triangle is well-foxmed..
the formalisation.
Pinal Farma Beatement
Variahles:
Poinuss
Linea: TU 15oz TU), 8D (for UM and EW), TV [foz W2 and WV), [foz VB3
We usms
CosnDsiangle
Counteianglo
TV
bellwen W
between R.3
(Vangle T:0:M) (Mangle U:7:W1
pasallei VS 20
Conclusion: Manngl B:VeNt Maangll V:S:N)
Note: The Line VS. is the wome as 8V, TO is the zame on UT direction doean matter For 1inex or parallel,
eec W.forall IT V.V.S. Point) (TO so 29 VS : Line), Tosalla iangle D TU su TV Viland CounZsiangl V. VS 80 TV Wiland. between D Waland betueen T T.W. Wiland twant inntiecintliiin mesteenntttetteeee (0 Waan IVtangle TellsM) IMaanle U:TaM) Waand parallel
(Mnngl
ORangle
The following is the complete reasoning trace produced by Qwen3-235B when using four-stage hierarchical decomposition pipeline:
seni Tormal ize English Statenent into acructure premises conclus Lona. exanine the Enzlish Statement sentance by sentence, and lareak down each sentenze into a natural language slause that as atemic passible.
"pranisess ses":
sentence "Twe Lriangles TUW shace point W." declarea two Leiangles.
*/
"The distinct points I, and forn triançic Vitriangle 7 D. 87)
"The distinct pointa
Leiangle Virriangle V.
/+
The sentence "The linea 80 and TV Intersect point R.* declazes two linea and Chels Intersection.
"s and distinct points line sU*,
"r and aze distinct points on line rV1,
"hee distinct lines su and TV intersect az point W*,
The sentence "The point X lies between and U, and also lies between and V."
distinct 5, the Among disciact points 7, V, the poins between
between and
"Biven Wargie
Mangle
./
"The neasure of angle 7 J. equals the messure of angle U.D. 2.97,
santence "B
*/
*S and ase distinet points liwe SV1, the angle
distinct points parallel to lane TO*
1.
"conal uxions":
The angle
To convert the Geri-Formal:zer Scructure into Tornsll lixe Structure, we now iiee each clause.
32

---

Published as a conference paper at ICLR 2026
sesnisss":
*oonnrianggc
*forntriongic V
XV*,
"dlacinctPeinttballaa" 8 8U", rddeinctPeinntooiine
"Laubist w.a.baaeiiiiiiieeeaeeeeeeeeeee
*batwaen S W"
*botwcen 7 V"
"VSaaggle
MVaagll d=T:W)",
"dlacincteeintecniin
vat,
"dLscAnctPeinntpoaan 7 13",
*paraliel VS 10"
"[Vaanll 2:VeN) Mangle VedeWy
Varisblwa: (7 U Pointt CCV OR WT
8M WV 50 Linel
eec W.oorall IT
Point) (TO
ON MT
58 WV 50 TV Line),
Cosnteiangle O UM WD AYland
fornf-iangle
Wlann
distinctPoinnt
Valand
distinetPointsontiiin T Wlann
twolti it ni At 80 TV Waadd belween
Wladd
R.V Wiaan
(Sannge T:0::01 = 0Gangle Detee Waadd
distinel PuintePPinnsiiiii sOuLiow S V. Alland
distinot Pointanninne
patallal TU
->
(Mannle S:V:Mi
(Mangge
V:S:MI 305
Direct Formalization Without Decomposition. When prompted to formalize directly, Qwen3- 235B produces the following output:
Wiforall
Feint) SU vs Line),
Counteiangle between 5. W. Wlaadd belween I V.V. Viland
TV Wiland CoznIeiancie
twoDiatinet wooooeLnnee Intessttttssssteeeo (Mangie
30 7V Wiland
(Mangie U:TINI Ailand parallel Mlangge V:8:MI
(llange 8:V:M
This formalization is missing two critical premises: dist
S U SU and disti Po ntstnLin T v TV. Without these, the statement weaker than intended be- cause it does not enforce that S and U are distinct points on line SU, nor that T and V are distinct points on line TV. This error type corresponds to the "Stronger/Weaker Translation" category in our error analysis (Table
Notably, the model's reasoning trace explicitly identifies these requirements. Step of its chain- of of-thhugh,, the model states: "distinctPoint siinttinntnnnnneeeeie
SU to ensure S and U are distinct and on SU" and initially considers adding this premise. However, the model then in- correctly reasons: "But formTriange
already requires distinetPointsOnlLine for each side?" U W TU SU TV provides di st. Potooinnttttooooo soninnnsnnnnnn ne w SU. This reasoning flawed: in the formal language. SU is simply variable name for line-it could equivalently be called 4 or any other and has no inherent semantic connection to the points S and U. The only way establish that S and U actually distinct points this line is by explicitly stating strain and W lie on the line named SU, says nothing about whether S lies on this line. This illustrates common failure mode in direct formalization: the extended free-form reasoning process can lead to flawed logical conclusions where the model misled by suggestive variable naming into believing semantic relationships are already captured when they not.
and lists that formTr formTriangle
S U SU. While form TrmTr' angle does con-
Formalization With Hierarchical Decomposition. In contrast, our four-stage decomposition pipeline guides the model through structured process that prevents such errors. When processing the sentence "The lines SU and TV intersect at point W" in Stage (Semi-Formalized Structure), the model is required to break it down into atomic clauses. This forces explicit representation of implicit assumptions: the model produces three separate clauses- "S and are distinct points on line SU", "T and V distinct points line TV",, and "The distinct lines SU and TV intersect
33

---

Published as a conference paper at ICLR 2026
at point W" In Stage 3 (Formalized Structure), each atomic clause is independently translated to its formal correspondent. The clause "S and U are distinct points on line SU" simply becomes & U SU, regardless of what other predicates might or might not im- ply. This one-to-one translation prevents information loss and eliminates the flawed dependency reasoning that caused the direct formalization to fail, yielding:
MMoorall (7 J.W V. Peint) (TU EW WI vs aM WV au TV Line), Wland
formfiinngl
WT Waand forntriangle 90 VVland distinetPoiat Line T.V Wland
distinctPuint DO tvoDlatinet Eineaiineennnnstaraeaeee Innssesttaaaeetttooooo 50 TV Wiard
between R D Wland between T.W V.V. Walan
(Mangle T:0:00 (Mangge D:2:01 Maaand
Pot ntsontine V. Wiand di dootiinttoon 0 70 Wlad parallel VS 70
-> Olangge B:V:Wi
(Mangge
V:S:KI
The decomposed output correctly includes all necessary premises. The hierarchical structure ensures that each semantic unit from the English statement is explicitly represented as an atomic clause, preventing information loss during the translation process.
Token Efficiency. Beyond correctness, our decomposition approach also demonstrates improved token efficiency. Using OpenAl's BPE tokenizer, the direct formalization consumed 4,661 output tokens for the free-form reasoning trace, whereas the decomposed approach used only 1,892 output tokens, which is 59.4% significant reduction. The structured intermediate representations serve as a more compact and organized "working memory" compared to verbose natural language reasoning, reducing the cost, inference time, and most importantly the long-context challange for the model.
D PROMPT TEMPLATES
D.1 ABSTRACTION LEARNING
D.1.1 STEP 1: CONCEPT EXTRACTION
You are an expest in mathenatics and logic with deep knoxledgs of all fields of mathanatics. You are giver. English nathenatical statements list previcusly extracted mothenaticel concepts. Your task to extrast AlL nathematical concepts nontd in the cursent statemencs. iondliioal__ppcs)
# Nathematical Concepts
types nathenatical concepts
*Dezinitiina Machenatisal objects*:: Point, Line, Integar, Real Numbar, Beries, Group, Bing, eic.
2, +*Rcictions between Nothemsticol Objestsee; 'a point boing on line', "an intager being even", 'a group being subęroup of another group", etc. veFunctions mapping Nathenatisal Objests Marhanstical Objectov:; 'the Buclidean distance function. napping Lau puinca in Eacl idear. space Lo a real muthee', "the Delmaninant. function napping a squace natrix to a real nanber', etc.
Guidelines
< When extracting dafinitions, relationa and functicas, you NUST as precise and detailed as possible. For example 'coagrient' is not a precisc nathematicol relation! You MUST specity how nany arqurents and what of azgunenta the relation ez Iunction takes like "Lao integers being congruen: nedulo "Evo criangles beine congruent', 'a 1ist line segnants being congruent each other",
2. velell--2ffi Doinn--oiin Flease HARE SURE. that each nachonatinal ob rolation, and function you well defined, oe has conventional? well aucepled defination, exanple, "Lvo lines being en appossing sides of point! is not sell-dafined because point can't partition a plane into sidea.
sAbbet rack neaaves i The definat lons, relat ions and funet ions you exiract HBS? be abe L.M. not invelving atatementa.
any particular jects, variahles, to line 2D is not abstract becacse it involves the nanes and 'CD'.
example, "Line being paraliel
vtlaminn Consisteneyees whan naning concapts, you MUST align with the previcusly extracted concapta 1C they thing.
exengle if previ eus concegts contait "two lines being paralle) in wuel idclidean apace' and the parsent stalements nent exactly the nama teve linea being pasallel in qualidean space! for this concept extracted fron the murrent statements. Only add new concept names if they truly new and not covered previously concegia.
refer the
"patallel limes in wuel idban space's , you should use
Aleaason ingstt Please carefully analyse the all English statmments sentence by sencence, ident all polantial defani celations and funolions, and deuble cleck the they well defined, Provide your detailed step-by-step ressoning sEREFORET intpeting your final excraction answer,
43 Output Fosinal
You AUSSTA drovide your final extraction anaver i.e. list of extracted concepts within triple angle phrase containing any recessary
brackets and aegerated by colons. Each concept chasacters exceps swni swni-colen colon!!!
665 bancept concept2;
200
Task Context:
34

---

Published as a conference paper at ICLR 2026
Freviously Extracted Concapts:
arerious__oonoppee
ET Curcent English Stateneats:
D.1.2 STEP 2: CONCEPT FILTERING
You are an expest in mathenatict, logio, progromming lanaguages, and ternal veritication with deep knowledge of all fields of nathenatios and forms izaatin mathenatios, You given list of mathematics ccacepts Eaglish, and the documattation of a Domain-Speciric Language (DSL) for tomal mathonatics. 1 soditional_epecs:
want include and fornslize
these concepts the current fernal DSL, Your task to filter concepts that neet the criteria toz inclusion.
# Filtering Criteriz
You MUST tilter concepts that ratisty ANY at the tolloving criteria:
*Duplisatioo other conseptaee: The concept
duplication of another concept. For exampee, the ccncepts "a point being the midpoint of a line segment and 'a point cividing a 1ine segment into two equal parta" aze duplications because they describe the exact same nathenatioal leal zelationship using different wording. Please please keep the ecneept "a point being the nidpeint ot Hine segmens' and cilter out the other one.
clearer
conventional verdine. this
2. ellleady Defined in Current Datev: The concept has a direct corresponding forma relation/tunctico// reing line with the description: daf la b Foinz) G : Line) -- peints and b are distinct and on line L. The syntex la Mist aciiin b L. Then the sumaupt 'Lee distinet puin.s liwa on line' akould be already definad in the
sirsady derines
DSL, example, ", and tha DS1 there is cosnal selation "discinttooiatonniie distinctPountsomil
concapt "ewo distinct
filtered out because
Dal.
43 Guidelinws
Conservative Filteringee: When in doubt, KKEE the concept. Only filter ouz concepts that cleasly violats of the criteria.
2. DSt Comparisones: Carefully compare each concept against the current DSL to idencify redundancy or easy ibill Don't filter out compepts mistake! Note that concepts night be very aimilar to DEL,
foural
in the the concept 'tve points boing or a line" is vazy similar tha fornal relation "def
different in aubile aspecia. For example
dist innt aonline la b Paint) G i Line)", ", but the forner allows the tau points to be the same point, while the laster zequizes the Lvo pointa to be diatinct. For another example, the concept la set of points being Pointl a faret", , but the latler only fosnelizes the concept that 'Lvu points being on the same side of a line', while the forner allows the aut of points to be nore than two.
sids
Hine is very similar
foral relatien 'dež sansside
eleessniigss Please carefully analyse cuncepi by cuncept, cupare then with other cuncepis and the cursent DSL to idencity redundancy, decernine which concapta should be PILTERED our (NC7 KEEPING), and provide your led step by ressoning +*ARPORTT outputing your final filtering ansver.
Octput Format
You M.USTA provide your final filtering sionsion sion as List of concepts to FILTEE oUr (NOT KRPPTNG) within Lziple angle bisackesa and supasated by suni volons. The new of the comcepls you provide should be M EXACTLY THE SAME as the nane of the concapts in provided concept list!!!
6ce conceptly comvept2; ... 350
If chare is concept. to filter out (KEEPTNG AL. CONCEPTS), please outgut eapty lists coc 300
Task Context:
$4 GCarrent DEL tormenntations
doc)
#F CCConcepts for filtering:t
[cancspt_] [ist]
D.1.3 STEP 3: CDG CONSTRUCTION
You expert
ics, logie, programing languages, fornel veri Firet with deep knouledge all fields of nethenat los and fosnelise isstion of nethenaticn. You are given list of machenali concapta in English, a 1ist of previously analyzed concepts, and the documentation of a Bemain-Spaciflc Sanguege (ne1) for fornel nat natheeattion ies. [addit ions". s_peeal
Your task analyzo the dapendancy atructuro each concect and determine how they can be cormalized the nil..
Degendency Asilysis Por each concept in the list, you need to deternine:
eatl rect Expressibi lityar Can this concept be directly expressed using exiating formll types, relations, current 3517 yes, list the speciiic DE1 elemett that can express this concegs.
lons
2. ecCongept Tependenciasse
nos di direetlly ly expressible, what other natheratios) corcepts (with no direct vorsespondentt in the cursent DSL) dows this cuncept depend on? last all the presequisite concegt needed to detire this concept. Taese depensensies should be abstract nechensticel concepts, not epecitic Instances.
35

---

Published as a conference paper at ICLR 2026
2. Fommalizatioon Statusve: Basad on the anslysis, classity the concept as:
aurestay_cxptessiioe Can be directly expressed uring cxisting DS2 cioments
paedi__@peedenciee" Requizes other coneapts be definad cirst, altimately foxmalizable "Iapossiale": Cannot be expressed in the current DaL and would requizo fundmeertal DEL extensions
44 Hathanatical Concepts
There types mathenatical concepts you add additiensl dependsacies:
**leCiniiiona Nachamatioal db jejecla*:; Point, Lire, Intages, Real Nurbee, Bec.es, Group, Ring, wiu.
2. **Relations between Mathematioal 0b (bstttar:: "a point being on lina", tan latager baing even", ta szoup being cubçzoup of another group", etc.
exPunel napping Mathemation
jesja Mallamalioal jecttaee "Che Buclidean distance Sunation napping two poinca in Buclidear. space to real number", "the Determnant function napping a aquaze natrix to a real number', etc.
Gridelines
"Conservativve Claxsi iante: Hhan in doubt beckeen "needxx dependecees and 'impoxsible', choose dewdaa_eeendeencie '. Only mask as 'igoosaible' 1f the concept Cundanentally tly cannot be expressed in the nathonatical franswork of the DEL. when in doubt between "directly strrecty_oxpreesibbl sime the
and "raeda_dapaadancee designed be expressive enougin for these coscept
" thoose 'diressly eappeyee and you should 1-1R YOUR BEST bo find direstly expressible fornal corsespondents for these concepta.
2. zaul Corsespondents Analysinass Be precise about what DS1 elanenta (lypes, relat luns, funet ional can express each concept, Quote the
DSL definitions
explain hov they selate to the concept.
3. Cunceep Dependencies Andlysiau First of all, ARRY YOUR BEST NOT Doxs introduow nes consepls unleas absolutely pacessary!!! If you mast incroducs nea concepts, note thas the 1ist of concepta you are other. "t's great hns, but be caseful about circular dependencivs! TMO CONCEPTS CAN DEPBNO ON EACH OTBER!!!
analysing night have degendencies
define concept
of
Conceep Tepandencies Criterieus When adding rew henat ical conceptx degendersless ex, you MUST follow
these criteria:
4. Prracissiaaess then adding new nachenatioal concapta as depandancies, you HIST be precise and detailed as possible, For exampl= 'congruent' is not precise nechenation relation! You Mist argunenta and what lype of argumenia the selation or Cunot ion Lakea like "Lw integers being congruent modulo 31, tewp triangles being congruent', congruent to each other', etc.
spenify how
15st
segrents seing
b. a Helll De indiiniisssres Please HARE SUREA that wash nat nethmnation ubject, relation, and funetiea you add depencency is wel deefined,, or has conventionallyy well-sooegred definition. for example, 'exo being appossing sides point plans into sides.
well defired because point can's partition
C. Abbbtt ract neesses The defin relations and funct ions you add as a dependency MUST be abstrect fie. part icular objects, variables, nanes in the curtent statsments. For exanple, '1ne aostract because it iavolves the names 'AB' and 'CD',
not incolving
being parallel line
Allessoningss Please carefully esanine concept by concept, recell the definit ion of each connegt, analyse which other concepts are neceseaty detine the current concept, which those aave direct correspondents
DS1, provide your deteiled step-by-ster ressoning esPEPRE.. generating the 390N output surroanded by tsiple angle brackets.
4 Output Formet
You HHUST provide your tinal analycis in 380N rornat within triple angle brackste. The JSON should have the tollowing structure:
tson
croncept_name 1a
"analysie"; "detailed step-by-stop reasoning for dependency anslycis'
"fornal corresgondents": i*l of DEL elemente that can express this concegt"), "soncest_doronnenssee ("list of preroquisite consepts"), "scatus": "directly_oxprees expressiiie mreeds_epeedeenciee laposssiae""
"conespt_name_"":
<ec OOT_OOOTTTEEERRS >>5
Task Context: ++Current Iocumentationn+.
[dsl_doc)
#+ Ppeeiioosly Analyzed consepts:
..Concopts for Analysis:e.
[concapt_[ist]
D.1.4 STEP 4: CONCEPT FORMALIZATION
You are an expeet nathenat ies, logie, programming languages, and Cornal vericication with deep knowledge of all de of methemation ios, proof ass assistants like Tean, and bonsin- Sinn---p-ff-- fig Tanguage (n51) design. You given cuncept. dependency graph (CDG) of nathenat inal concepit, previnus extenaioo file(a)
containing concepts you have siready implenented, and the decumentacion ot a Donain-Specstiic Sanguege (nerd for formal met remetetts.....
36

---

Published as a conference paper at ICLR 2026
Your task 1s to extend the current DEL by impiemaating / tozmallzing the provided concepts in the CDG based on the current DEL.
[additimal__ooccs
11 Gcidelines
+CDD Intespretation=:: In the COG,
concept, the field 'states' indiestes if fermalia this cuncept as relacion, function, albrewiation, alias, sic. in the ouszent BSt. IC is dissetiy_ oxxpe_ssseessebeee then the field "formdl wow.oooorreeeeee cosrespeadeent"" 1isss the specific DSt elenanta that can express this concept. You +*UUSI+* cirst tzy your test to implement the concepts usiag these Gemal_oozegoombenaa" Boweves, if they rediets any specificat iuns given above, You abould carefully use your oan knoxledre and judqenent deternina the most appzopziate way implomant / fermalize each concept based or the current DSL, if the fisld 'status' is deperddcaeer then the field "esncept "essneet__lependeeii pdegendenncies liats the prerequisite concepts that need to Commaliee first before we formalis this concapt.
directly
Faithh Criginal Concegite: please bry your best to faithfully implement / fornalize the original concept, nothing nore and notliag leas. Por example, if the original concept is a la quads fatera" in 2-dimenaional Euclidian space', then you should only invevle the four points and Zour linas that corm slements
as the diagonel linesvs!!! Please AAAA EXTRA A thiat!! Buch subtlety will result in entisely different fornalization ions.
quadrilatera',
3. Code Beuseess Please Lry best Lo caose the halper funct luns Iosnal ised curouplx fron the previous extension file(a) implenent fomalisa
concepts. Please don't reinvent the sheel!!!
4. ACCusi stunsis with Curreal DÉL.:: Please wnaute your extensiun nalthes the parcent DS1 in spieit and atyle. For example, caming, API convention, fornallzation choices, eic..
Affocument ionass Please carefully y docurent every new type, re re'ation, Funct ion, axion, abbrevition, alies notation, sle, in your anglensniation Please make sure that the style and level of deceil are consistent with the cuszent Dal dosamentation
ABBersonings: Please carefully waanine cuncepi by cuncept, analyas the dependency struelurs of wach concept, dotarnine the best way to inplament foraliie each concept based on the casrent DSL, and provide your detailed step by step reasoning A.RROORE outputing your final inplementation.
Output Format
You don't need to re generate the previnus exteraion filets), AON output your impil enentationn of the new comsepta, which will be appunded to the previous uxtension filwist. You MMBB provide your Linal Inglenentstion within triple angle brackets.
your antiow implerentat goes here
# Task Context:
4d Current DSL Romment-atio0ss
(dal dos)
Ht P-Pevious Extension (s)
(peevioux exteeniiintttiiinn (i__eiiiinn___a
4+ Concegt Degendency Graph FAA
lodg_liste
D.1.5 STEP 5: FORMALIZATION REFACTORING
You MADMEL nathenal ies, logie, programing languages, Cosnal veritioat fon with deep knowledge of all flelds of nathenacics, proot assistants l.ke Lean, and Damain-9peeific Lanquaoa (DaL) dasign. You are given the cocumentation of the current Densin-Speciric Language (DSL) for cornel machonstics and file (a) containing extensions jaew definitions, selations, funetiona, axions, theorens, nocations, etc.) this
Your Lask is to refactor the extension file to Improve its quality, misstainabllity, and consistency with the DEL desien principles.
[additional_sgees;
44 Guidelines
vxAggressive asfactoringes: You should bold refactoring extension file:
*>Elmmintte Badundancyee: maltiple definitions express the exact same nachemstical concept wizh
different leoels of generality, keep only the nest general and well abst rected version. reConsolidate Sinilar Patzernars: then you find mittipe sinilar definitions that can be unified, renove the individual ones
single, paranetarined abstracs ion
riuullity Goes Quantatyus Is's beiles to have feaes, will desigred abstract iuns than nany spacific,
poorly abstracted onas. You are not sequired to preserve every single decinition from the original file. Pocus great
sxiick One Colyes: If clear, meintaineo's
and nathenatica inally sound extenaion.
nany formal calasions that sinilar each other, substituta each other, you should either carafully cheose one than, oz nerge then lnco singls, nore general and canonical def definition, Malt pll sinilar APTs can be confuxing to the user, A.R CONCISE, B2 coNerse, BE CINCIE
YA Prrrssevv
The Ne Eoen though you are red to refactor aggressivelyy you should preservw the formal concepus ase not trawly not in the cuscent bas, IL's ok if they night be easy te inplsmeat using the current 155, prinit but this will enhance the readsbility and forther extendabi of the DSI.
Docunent at loners Please carefully update the documentation of every colation, function, axion, abbrevition oo,, ias, notation, etc. you refactored. please make sure that the style and concent are vons inte wish the current eSl, documental ion, son the comment in the extension filejsl. If there comments extension silels: tast are not consictent with the DSL decumentation, please retazter then as well.
37

---

Published as a conference paper at ICLR 2026
Reaaoniingee: Pleass carefully analyze the extension file, idantify areas for inprovement accordiac 2o the rofactoring criteria, and provide your detailed atep-by-stap reasening **BEFORE** catpatting your refactored implanencation.
Output Formet
You + grevide your zefactored Lean file vichia triple angle brackets. The output should be complete, be appeaded the DSL. include any ixpost statements they will landled supacalely.
valid Sean filc
<<< your refaztered implemmtariio gocs here b55
Context:
Ff +*Current DEL tocunsatation:**
[dsi_dos)
626 xxExtension File to Refactoriex
lexcension_
D.1.6 STEP 6: DOCUMENTATION UPDATE
logic, programing languages, fornal verifioat with deep knowledge fielda of mathenatios ics, proot assiatants
wegwet
Lean, Danain Spscia---peiiii Language (BBL) design. are qiven the cocumentation of the currant Densin-Specific Language (DS1) for cozmal machanatics and definit Lions, renst fons, axiuns, theurems, not lans, eic. is generate DEL docunentation incorporate
extennion filw cuntaining that have added this DSL, the new elenents from the extersion filets), whi preserving the previous dommentatt fon intact.
[addi
Guidelines
exPresevve Existing Contentre: Keep all existing documantat fon content unchançed, This in +*MIST
scCumisseecyy with For example, if the current documentation explains the syntax or gives usege examplet, then you shou.e de the same.
Keep the style
the DSL docuren
Reasonningss
csrefully analyze extension filetst, identify decurented, deternine the best way to integrate then into the exist ing docuenntat ion strcture, and provide your detailed step stystep reasoning e.BEPRR cutputiing the new updated Dal documetal lun.
elements
Output
You H provide the new DSL decumentation vithia tripis angle brackets. The sutput should be complete, new version of the DSt. documentation that incluces everything: bach elenence from the current his. docurentationn and documentation for the extension file(s). (x).
<cc your entire new DSL. domment goes here
Task Context:
(cc)_doc)
Filelsi Documentive
(excension, 1el))
D.2 HIERARCHICAL DECOMPOSITION
D.2.1 LEANEUCLIDPLUS INSTRUCTIONS WITH LEARNED ABSTRACTION
You gi vie Lng Stat of thearen from Eael idean Geanelry. Not that all puints and limes unless othersise implied
ioned the
prenises.
Your Lask is to flest wedi fornalize the Bnglist: Btasement into a Json style stzupisee (sew Guidlines 421, then fornalizo each clause in the Muni-Fornslise Structure reacl:ing in a Fornalized Scructure, and Formll following focmal definitions and guidelines. inws.
finelly
fornsl
strint by adhering
Baxic Gennetric Sorts
Point Pyge
axion Type
axion Sirll Type
Inductive ou Typea for Seumel cue Batities Ieduct fon Angle right ofPoints n Point! induct Segnent inductive Triangle effeints
Point)
Point)
Notat lons and Macros for Geanecria Rnt
38

---

Published as a conference paper at ICLR 2026
(a-b1] 1" means the length of the 1ine segnent Itype (R)thab(R), not type Segnent) between point and point b.
"anggl asbre" neana the degrea of the angle Itypa (R), type Ancle) Corned points and whare is the vertox of the aaçle and and c are points respactively on the two sides the angle. Add parentaeser azound the englo notation like " "(aaangle sibre)" to avoid anbiguity.
"Aperp means the degree of the right angle (eype Wiathbo/RR,
typo Angis).
"Veeiannla atbie" neans the triangle itypa relancle) forned from points a, b and c. "Triancle. arca Vitrizngle aibie" means the azez of the triangle formed by points and c. Add perentacses the Lesangle notation like "BNisiangle ashsu) Lo avoid anbiguity.
Relations and Axions for Gaonatric Sorts sarespace Paint def caline la Point) II : Line) -- point a is on lire i. The syntax is "a.entine 27.
def sameBide (a Point) Cle Lanel point and Line by but can the sane point. The syntax is "a.sanedide 1".
the side of line L. They both
def sepoxingSidee (a b Points (L Linel distinot point and b ase opposile widea of Line h. They both not Line The syntax "spooppiing b.l".
def satircle (et Pelot) (C: Circle) point a is on uircle c, The syntes is "a.onCiecle CT.
def Insideci lws Point) 10s Oirole) - point is inside cirele Te can't be the rile... The systax is "a. iniddeellele C".
def out rede (as Pointy (Gs Circlet- point is autxide slirale C. Tt cantt be on the circle, The syntax Ls "dooessdeeieele C"..
def re (et Point] (C: Circle) -- point a is on the unique center of role C. The symtax is "acirtrrtre C
isMidpointo
Point) point
micpoinn segnent iif becveen and thence all The synbax is "m. in..iMidppiinnt la"..
three are dissinct and col Finerl, and [AM]
def spiidoo of Endpol Enggent nte in b Polinti ISP Segnent) expl ieit segnect wisnexs. Reguiies SP".
an "mr iidipoorrtt bt with Segnent indpoints by, The syntex 'm.
def callxtenxionnee Beyyndd between b p", The syntex in "p. "p.ooxxtensi onBeyend b',
Pains) point I lims the extenaion ion of segnent AB beyond indpoint B iff
def inlaetennionneyeee (F a b : Paint) point p Lims on the ext Iun of segnent AB beyond undpoint À iff between b p", The syntex pr.onnxtensi b'.
Point
camesaace line det incerseoteidae (L Dansl two Lines and incersect at some point. They can the cone line. The syntax is "hrantersectatinee W".
det incerooctecirolee (L Ginel (C Circie) line and cirole intersect. The eyntax is "b. intersectaCi Ct. and Nine
namespazo Cirzic det soce (C) 02: Carole) -- circle 01 and 02 intersect. The syntox is "C1, "cI.inceroeescciccee c2'. and Circle
namesaace Triangle des sid:AB la b Poinc) LL Painti : Segment -- the side AB of trianglc ABC as a segment, ilc. "Sogneat. triangle.sisent
endpoints b², The
def sid:30 La Pcint] (b c Pointi : endpoints b e", The syntem in "Triangle.sssees a b ot
Segment -- the side a0 of trianglc aad as a segment, i.c. "Segnent.
def sidsCA 2oint) Lbb Poinz) Point: Segnent the side et trianglc ABC as segnent, i.c. drgpenttenddoirte. a", The syntax ie "Teianglo, a d". and Triangle
Geonstric Relstions det cistinatPointecnllns la Foint) (L: Line) -- points and are distinct and or Line L. The syntax in L".
"dssiincteoinscoaiaa
def between (a a Point) -- motually distinct points 3, b and are collinear and ordered, Point b is batseon point and c. The syntax is "batwaen a c".
det tomrriangue
CA 1 Line: matually distinct points a, and toum triangle, where point and b are on line AB, point b and a are on line 20, point a and a are on line ca. The Hines 12, 20, and Ch must be distinct. Noto that the crder and carsespondence or argunents b, a, AB, and
Point)
atrictly required and they mast ba passed in the exact order! The syntax is "tommTecangle
be
and ac CX".
CA,
def CembBettilinasAAne (a Pointi (AB BC Line) - points a, b and e form reccillnwar angle, where vertex
and points saspectivaly sides and BC. The sides
39

---

Published as a conference paper at ICLR 2026
and BC can ba the sane line, the points and e can be the aane point, but the vertex b suat ba distinct Zeom and C. The syatax 10 SernRectiInncriinn a h e AB BCt.
def fomfasalletocra b clocstto//oonearroooee
Point) (AB AC Line) mutually distinet points by and (in disgcnal) soam a paralleiogran, where points a and la are
order 1.c. ad on Line AB, poincs c and a are on line CD, points a and are on Line AC, and points b and d are on line BD. The linea AB, cb, AC, and BD must be distinat. Note that the order and cotrespeadence of argunence Cr AB, Cb, e must on Ac. and nuat be en BD, and they must be passed an dhe exast arder The aynlax is ternParalleloge
BD stristly required 1.s.
and
be
and
a b e d AB CD AC 3D".
def Lsodiatin Liventi sesect
Line) Point) i, 1.s. 1- N, lies on beth. and H, and iLttrrrrcttttin M". The ayncax 2 R 1",
diat lines and intersect point
def sequentialiviiggnd (pto List Point) 1ist of points pequantially alignad (ordered collinear chein] iff every consecutivn triple le P PLD))) satisfies "betveen pia I plin pl 2222 No wxtra line or gichal distinctrass is sequited beyond beiveerness, The ayatax is "sequantalllycc halllyyy [DY_O, Plat, Pi_2, ..-I"-
def suquentia Sagunnaayy.iooooiheeooooo the list to contain at least three points. The syntex is 2 ...l".
(pta List Foint! like gequentiallyAlllne additionally requieing Ipl_o, Plu,, pl
def twosocssppodiinneeesccaa
(xs ya i List Poinz) (2 Line) swo lists of points 1ic on opposite sides of Line it ()) no point from wither list is on L, (2) eowsy grosa pair is Win sh, Win ys) is on oppoaing sidea of L. The syntax is sesdarsspppssnngsdeeeeee
[XL_,, x1_2, .... IYL yLa, .... ur.
def sugllemntasyynnge
a d C. C. Point] angles Mangle asbre and Vangle dreef are supplemntaary lff (Mangge asbret + (Mangll die:f) = 1sparp Mppepp The aynzax is "auplonentarylogles a b & P..
def parallel (L R : Line) syntax is "parallel 1. M".
LvO linea and are parallel ift they are distinct and do not intersect. The
ranCol Liperroinnts () 1- G. The syneax is "nonCall inearllinsarriittt
Poinc) -- points a, b, are non-coll ief Triargleveres (Vstriangle asb: et,
def segrent Proveertexoooogos teside al #2 p.:. Point) (SP Segrenti -- segrent SP connects vertex to point the appoxite side vls2, The ayntax is PegnentPrunneeee Pwuneee
by "between al p 42", Bequizes '52 Segnent endpoints v.p.
al a2 p. BP".
def congruent Segrenta [4 b d.d.d. Point) segnents AB and CD are congruent iff [AB] I6D), The syntax is congruent b d'd
def pe pergendieulartl IE 9 Line) ii a e Point) lines I. and i are perpendizalar with right angle at vitness point using points on L and a itts III "Iiintersectatinn H'; (2) inmertti H" a. Him on and 5, syntax is "perpend L
H, with e".
vertex); Mangge asisel Vperp
def equa Sengttanthheet ion (6 b / (GH1). This real-nunber equstions no nen-sore-length guard is entoraed, The eystax 15 equn a b o d t 3',
f h Point) ity of two segrent length ratioss ((AI) / (0D]) (1F
det trianglokngicsum (a interior angle sun Apperp Vpperp i (llangge brasel + (Maangle asbret + (Mangle aseibl + W perp Aperpp . The syntax is Arriarglenng eSon b e".
Point)
nen-derenerate triangle ABC 1i.e, "noncol
b o'1, the
def trianglestimilan (a are equal: Wargis BAC Wançle E0E, Wangle ABC Vanggs DEF, Wangic ACB VMangic DEB) 12)
Pointi triargles ABC and DEP are sinilar iff: (1) corsesponding angles
ccrresponding rides are propertioral: [ABI/ DS - 1301/1EF1 and 13C1/18F1 ICA//IEDI, The oo correspandence i8 AC-DD, BC-23, ce-or, No non-degeneracy is assuted, The syntax is "sriarglesSimiler e
def tri Cocorrrnnnttt la b c dedeeff f : Point: triangles ABC and nEz are congrsent iff: (1 correspending angles are equal; (2) correspondirg eides are equal: IABI-IDEI, 18C1-18F1, ICM1-12D), The carraspaneence is A4-30, BC->E, C6-FF, The syntex is triang_estengruen
abc
dcf tommonnesouuddiiaaasss la b c d : Pcint) (A8 BC Co DA : Line) -- erdered pointe a, b, c, d with side- lines AB, ac, Co, DA torn corvex quadiilttrral :tt: (1) consecusive vertices lie on their side lines with distiact endpoints: "distinetPoinnsooninn distinctPoirts0mli
AE", "diecinctPointsoniine
BC',
a CD", "dietinctFounteehiinn a DA'; (2) tor each side line, the two nonincident vertices Lie on the same side ot tast line: SudameSide AB, d. sameSide a BC, semeSidd b CD, b. sameside e DA. No further distinctness, intersectica, or noa-colliraarity is inposed. The ordez and cervesponiennce
strict: AB is the side ab, is the side be, is the side ed, is the ac D8
and they moet be passed in exact order. The syntax is "tocncorvesQuadri lateral
def disooiiaorquarriaattta
é Point) (aF Segment) SP the diagonal AC the ordared quadropic 1a, b, c, db, 1.c. "SP sognant.endpcinns a c". The syatax is "daanalkorruarritteen a d SP'.
dof disponnieorruaariiteee.
Point) (3F Sementt SP the disgonal B0 the ordered quadropic 18, D, c, sh, 1.c. "SP eegnent.endpcinne b d', The syntax is "ddsppniiBoottaarriitttt a d SP".
dal swgnentBisectssnneeaa
BP Line) segmen bisscta angle ABC at vartax b. with: 2,5 A3) byc on BCJ b en B2) intorior kitnaszed by sane-side constrainta a. samsSise p B2 and c.sans5ide 7 Λзю sub-angles equel 1V Mangce aib:p) IMaani pib:e); and "SP Segnent, endpointa la p". The order in acsiot: AB is the side ab, BC is the aide be, B2 is the carrier and thay
(a
Point)
Segment)
line of the Rissctor acomattllocctoongaaeeeee.
passed in
exact order. The syatax is
a F SP a2 BC BP"
40

---

Published as a conference paper at ICLR 2026
def trianclesShareeidhe (sell_2 Foint -> Point -> Point -> segnent)
(2ell_2 Foint Point Point Seqnent)
(a dede : Peint) triangies aac and DEP stare a side witneased by secnent selecters "sel\_3" and "cal
12" itt "sel'_1 a b c cell_2 d e.r". Typical solecters are "ssiangiecciddta" , "Iriongis Stiaeg The syntax is "triangieshharesdddyy Triangle. aideAA Triancle. aideac b d a E"
CF
del Teuiaatuaateeiangl
a Point) Leiangle ABC equilateral [AB]
(BC) and [BC]
[CAI. The
syatax is "epuiattrattiianlee b.b e".
del IsuscelusALA b Paint) Lsiangle ABC isoacelea vertex ifc [AS] ACC The synlax is laoscoleshth a b c*.
del LsoscelusALB la b Paint) - Criangle ABC is isoaceles vertex ifC [aX] BC) The ayntax is 1soscelesAtB et.
(B), . The syntax ia def isoscelusAte la b.e. Paint) -- criangle ABC is iscacelea at vertex D LEC [CA] LaozcelesatC a c".
def Liasuttatciannleedeeaaaae
(a c p.g i Poinc) (AB CA L Line) -- Line intersecta sides and of triancle ABC at points p and q respectively, with: "fermtriinaae a.b. a AB BC CN') betweenness between p b" and "belween la the aide
and both and L. The order and cus respondeenee aew atsiets AB is the side and
la the aide this exact order. The syntax is "Laccurssannonaaaddd
line; they P BC CA L".
passed in.
def Lineutsstiinggiennaaadeee
Point) (AB BC CA L Line) -- line 1 intersects sides AB and BC CX"s betweemess "beeseen F b' betwwen i q e'z and both p and q on 2. The urdez and cozzespondence aie striet as abuve. The synlax is SamelttatsanggeeuuBaaii
(a
at points p and q resgectively with: 'formfriang'"
a b b.c.p. P AB BC CA Lr.
del baaaaaaaeiannnnnnnaaaaa
(a 4. Paint) (AB CA Line) -- Line intersecta sides at points p and q respectivolv, with: "Forntriangia a b AB BC CATs becxeenness "backeen e P a" and between b q etz and both and on h. The order and corcesgondence are strict as above. The aystax is LineCutafe wwg.aaaaaaannnnnanaaaa
a be AB BC CA LT,
def ShmenuttARendAACaa lelRc
C.P.P. : Point) JAB BC CA Line) line cuts sides AB and AC at p and and is parallel to side 30; suquires "lineCutwTeinn wew.eaiiinngllaaaaaaaaaa All BC CX ti,,
a la a p AB ac CA 1. and "pasellel
agt, The eyntax is inneCtt sARardAcPaaal T lelnn
def Lineetaa
a P q Doint) [AB BC CA a Line] line cuis aides AB and ac at and and is paralle Ie to side CA requires "1 "Hineuuteee Triingg lengllenndiccce a l. c. An an CA 12" and le ABl BC CA Lt,
cat, The syntax is "lineCut stBer AScrrea lellca
def HineCut secettaeane
P : Point) JAN no CA Mine] line cute sides ac and mn at p and and is parallei to side AB; requizes " "lineCuta werullarinnggne Werringglnndaaddeeee a b. o 4 AB ac ca 1." and "parellel ABl BC CA L",
AB', The eyntax is Stteraastaara LelAB
Guidel inws
1. lize Statement Fornat: Your tormalized statement nust be of the tor eee Wtorsll Goob P_1 Wland P_2 Walan P_n -> 0.1 Wland 0.2 ... W Wan 0 255 where shere each P_l and D.1 ix built fron the above builcing blocks using conjunction (WAlnd disjuaction WWlo } and negstion MWng 1. Mi variable seclaracions must be placed in pacentheses after the univerosl quanticler, You chouldn't declare varishles or use fient in any other places! For di differert types of verisbles, you should them ditferent pareatheses. For exeplee, the Englich statement contains *Iae points A, on line AB", shen you should declate (A Pointl (AB Line) in the tormalized stazement.
2. Semi-Fo:malised Structure: For the Semd-Formalized Structure, you must output 5 isors-style structure tyou interleave comments in betweer data) with fields "prenisee" and "conclusions", and the each riled is List clauses.
"pramises": Enguish clause 1, English sh alasee 2,
Roonal on
English clause 1,
English clause 2,
Sach clause Englich sentence representing proposition. The relaticnship betwsor prenises and conciusions is inplication. The prenises are the antecedent and the conciusions are the consequent. relaticash.p between each clause is confunction. You should try to make each clause as atonic as pessible i.c, within a clause, taere shoulin't be any logical operators. It there has to ie some, you fav loqical operators wichin stause pessible, and multigle clacses instead express the same meaning.
should
3. Formallzed Structure:
The structure is exactly the same as the Sun--Pormalzed Structure, but you will expressicas, to get the Fornilizod
termalize English clauses 4a premises conclusions Structure.
"psenisus":
Foznalized clause
Fornslized clause 2,
"conclusione":
41

---

Published as a conference paper at ICLR 2026
Foodallzed clause 1, Poznalized clause 2,
For the formalization of each clause, you should fleat tay to find it there is disect corraspending fornal example, the English sentence "distiact points
relation providad. potsncial diseutly correspondigg farnal relation iun "belawed" You should then doable cleck the detailed description of the fornal rolatior. to see if the details natch the actual English clacse, and pass the arguments in the correct order specified in the description: "between b a c". If no direct tormelizaticn natch,, you should Eosnalize equivalenily using
between and ot has
relation deserigtion ian does available oparatozs, constants, and other forall relations, Por axample, "che sointa A, B, S form inseribed trianalc in circle Viaipha docen't have any direct formiization but it's equivoicat to the points à B, C forn triangle, and they are all en cirele Valpha ", which can be fornalized AB CA Wiland A.oncizela Valoha Wland B.onCircle Malpha Wiand c.saCircle
available,
farniriangle Malgha
4. Emplication: Thare can be only single implication. in the Commllas either sida of the implication must be conjunction farmllas.
5. Variable Kaniao: You should always use the EXACT SAN varialsle nane in the fermllized statemant as the ens
In the English saatmment. For exangee, if the Rng statement cuntainx *Point A, B is on Line AB" then you should
the variable canea not add any prafix er surcix to the variable names like "poins_A" or "AB_ !ive sontimas the Engl ish statemen: night fiest sufer to a Line as *AS", but. later use "ax" for the sane Haw, in which case you should use the fiest occcering name "AB" for that same line consistently in your fornalized statement.
Point] (AB Line) the fornllized atatement. traau
5. Bunezic Values Restrictions: Denoce 90-dacree angle by Vipepp 130-deqree ancle by Viperp + Vipapp etc. Also, when referring segrents, always mean itx length (i.e. 14s II.
quantified Variables: Your quantified variables must linited to prinitive caometric typea: points, lines and pircles. AMd, hound variahles that you declared must be nertioned in zone clauses later,
Internediate Variebles:
should never decine intermediate variable inside preposition, For example, thet Vellhh sn (nomething);" not alloved.
9. Homenic Operators: You should only uses addition [41, subtraction (-1, miltipltercion (e), and division 1/1, Avoid using other nathenat loal operatora
ex exponentiationn
1C. Fiuality Rolation: You can use the equality relation (e) and con-egulitty relation (!=) to compare points,
lines, circles, angles, and line segnentx, Booever, please cavosder uxing the equality relation compare exprescions and numeric values as it's not supported by the current tornal language
englementationn ion, For example, you shoo ld write (e I - (0o-)) 1" insteed of *[]a-b)] I / / ((od)) "*,
11. Angle Notations When you see short-hand angle notation like "Vannge Xt, this neans that is the of angle. You should alweys expand to the full sngle notation "Viengle Mangle AsX:B) where A and B ase points respect ively on the two sides of the angle.
[formely ly,
12. Syntax tip 1s You should only use the provided relactons and axions. Please exanine the provided axions and relations caretully to rind the best way to express your proposizion. Don't create or use new ones that are not provides above! When you see an error nessage that cortaine *unknown idertitie=", it neane that you might have used some relations that are not provided in the guidel blease double-check this, or your tormalized statement won't complie!
13. syntex fip 2: You must declare all Points, lines, and Gircles that you will use in the formwl statenent. You shouldn't coclare any extre, Points, Lines, or circles that are not used in the tormllized statement. When
message that contains "unknown identifier" tergettan to deciare some Points, Linos, Circles that aze used the formalized statement. Ploase druble-check chis, or your tormllized statement won't compile!
means that you night have
14. Syntax Tip 3: You shouldn's declare any
Foints, Mines, or Circies that not used tornolizes zed statenent, Mhen you see ar esroz neseage that contains "Unexpected expression", means that you night have deal declared ared some extra variables that are not used in the formalized statement, Please deublc-chook this, or your formalized statsment won't complle!
15. Syntax Tip 4: fornalises angle Mangle
always expects three point iffer separated by colons I. sven though you will see the Eaglich expressiens like "Vaanii y", but "Mangie y is not a valid tornalization. You should commllie it into "Vannge X:Yig" where X, Y, and 8 are tae three points that message like *unexpeeted token 'P') expected ';",,
form the anzie. men you you have not provided, the correct nimber identitices for the angle, or you need to susround the angle with perentheres like (Mlaggle XiYiEi to avaia ensiguity, Please double-check tais, or your tormllized statement won't compile!
that
16. Reasoning: Please think caretully step-by-step and state your intermediste reasonirg steps betore you -tomalizz each: clause whea corverting the Engiish Statement to Seni-Formslized Structure, formalize each clause when converting the Semi-Fommalize Seructure into Formalized Structure, and write domn the final Fornalized Statonant, **This cracial!!! Please do aot provided by the user, you must strictly follex the tornat and reasoning the exampleat!!ee
chis!!! if there examples
17. Rasponse Format: Present your formalized Lean expression within triple ancle bracketa [see Lean expression here 525), Do not add any imnotations//xpiassiinne markdow: syntax.
D.2.2 LEANEUCLIDPLLUS ONF-SHOT EXAMPLE
Heree is an exapple:
Bnglish Statement:
42

---

Published as a conference paper at ICLR 2026
Thare aze tvo triangles VMrriangle GBJ Viceianlle IPJ with shared vertex J. the 1ines intorseat at point J. the poiat 1ics between G and I, and a1so Lios between a and 2.
Given B Complete the proof that Weriangla G. Vitriancle F
Semi Sand-Foznalzed Scructure:
To seni formalize the Enelish Statenent into a acructura of prenises and conclusions, we will exanine the English Statement sentence by sentence, and larcak down each sentence into a natural lanquage clauss that
possible.
"pranises":
f+
The sentence "Thaze ace Lwo cxiangles Wiriingle GBI and Wiriangle IPJ with shazed vertex J." fisst declares 2 triangles Weriangla G.B. B J.J. and Veriangle I F.F.A.
Pron the instructions,
know that all points and Lines distinct, ao also declares distinct points: B, J, G that zozn triangle Vitriangle B.B. J, and I, E, J that rorn triongla Wariangie I.P. J.
No can break down senzencs into the following pranises:
4/
"The distinct pointa G, and J. forn triancle Vitriangle G.8 J triangle Verriagle
*hhe distinct points T,
Poz now, the pranises above only partially expresa the fast that points G, E, J, I, are all distinst and some Lines (xides of the triangles) distinct.
Bexevar, we night
to incorporate and express this distinctneas relation later prenises, we don't create addit tonal prenises for then right now.
Instead, will first examine sentences in Bngli statement eventuelly create prenizes for rensining unexpreased dist inctness relat lons if necessary.
+/
sentence "The linea and intersect at point J." Cleat declares linwa: GI, BF,
Pron the instirutt ions, knox that all points and Linex are dist inct, so also declares 4 dissinct line GE,
points and distinct lines: on HE,
It then states an intersedt fon relations the Lines GT and HP Intersect at point d.
IF explicitlyy
the inttness of the points and lines, night interprated same paint, and P can be the wame puint, or and SP aow zame Line, which is not what ve vant.
wither G and I can
Theretore, can bresk down the seatence into the zollowing 3 premises: ./
"Il and are distinct points on line 197,
*S and distinct points line
distinct lines GT and
point J*,
Since ve had explicitly expresses. tast the poince G, B, J are matually distinct, and that the points al expressed all discinetness relatiors between the
are nutually distiret, points B, 2, except the distinctness rolation beckeon and and I.
If G were the same as F, shen Gt (FT) would intersects HP at point F as well as point J, which means which contradicts must dissinct points.
either and are distinct lines. Theretoze,
and are distinct points GI
If B were the same as i, rellewing the exact canc reasoning, will get a contraciction. Therotore, distinct points.
Tharefore, we chocked that ail distinctrase relations anong the peints G, H, i, F are expressed. There is only one note distinctness relation lett to check: the lines GB and FI are distinct.
vero
as FI, would the incerssetion of which contradicts the tact that 6, H, and (b, F, and 31 form a eriangle. Theretore, GB and FI must be distinct lines.
HE, paint a1so lying (EI),
Theretore, checked ./
distinctnese relations among the points
expressed.
contonce "The poins lios betweon and I, and also lies betxezn and states order rolations : the point J is between G and I, and ciso between H and F.
dea't explicitly state the distinctaess the points, night be interpected be the cana oz or J can which is net what we want.
Tharetore, ve have the folloving premises:
Among the disciact points a, 1, the poins between and
"mong the distinct pointo H. J, E, the point is between H and F",
43

---

Published as a conference paper at ICLR 2026
sentence "diven J seqnants: J 3.
atacea nunezic equation between the ratioa of line
ThareCore, have following prenise:
"The retio of segnent GJ zo segnent 1J equtls the ratio ot segment EJ to serment FJ, denoted ad J E
The sontence "Completa the pxcor that Wirriançle G. J Wirriangi I.P 3. states the gocl of the pooof: show that the isiangis Wirzingge
Vileiangle 1.3 sinilar.
Tharefore, we have the following conctucion:
*/
"The triangles Weriangla B and Vitriangla sinilar, denotad Vitriangle G J troangle F.F.
Formalized Structure:
convert Boni-Formalizdd Beructuze into a. Zormalized Structure, vo will exanine naturel laaquage clauses in the Seni Pornali Struckure une by cns, and formalize each into fornal planse Lhas. is formed and well-defined according to the quidelinea.
"greni swa":
clause "the distinct pointa G, 3, Coen triangle Vitriangle has potential dizect Forms i ixet ion in the guidel inest "fom"riannge""
check the desoription of the "fomitriaggl"" relation: "motually discinct points a, form triangle, ly shere point and are on Line AB, pains b and a are Line 8G, paint a and are on line CA. The lines AB, BC, and CA must be distines",
nutual dist nnst poine
pounta as and of, definition, target
deseription "mutually distinet
3 pointa that foom a criangle mast be cea-colllmass, which nacches the description "The line AB, RC, and CA must be distinct", Therefore, this relation is indeed equivelent to target clause.
"forntriangle" takes (e b Point) (AN CA Tire) es engurents in arder, so we can formali the clause ast "fomft "oomnriangle G B Gil HJ J6".
fol lowing classe "the dist points F, form triangle Mersangle Tormalixed in the exact same way.
"herefore, formal iie the first clauses fol lows:
*torntriangle GH EJ Je", forsstriangle Y.J.J TP JI*,
The cleuse "il and are dist not points on lire HP* has potentlal direct in the quicelines: "gistinottotaesoniinee""
double check the dascrupticn of the "diitinccFoinssontii"" relation: "poince a exe distinct and on line D". It is indeed equivaient to our target clause.
takes Point) Line) arcumente ordes, distinetPeineeonniee
formalize she clause
The tolloving clause "G and I are distinct pointe on line GI" can be rormilized in the exact same way.
"herefore, formalise
clacses follows:
./
"dlstinctPcinntonniie R F RF*, distinncteeinttoolnne GI",
/+
The clause "The distinct lines aI and HF intersect at point J has potenzial dizect fornalization in the guidelines:
Me deuble check the dascriptica of the wwwbrrtreetaeetttsseeeeee
relation: "twe distinc: lines & and M intersest at point 1.0, 1 1- H, liss on both b and H, and "Liincareactsiine N clause since it quasantees
*r It indeed equivalent
lines distinct
It takes IL H Line) (1 Point) as arcuments in ordez, so can fornalize the clause as follows:
/+
clause *Arong the dissinct points formallzation the gcidolines: "botxoen".
the
and has potential direct
Ne double check the descraption of the "between" rolation: "autually diatinct points and are collinear ordered. Point between
and is indsed eguivalent target clause since quaraatses shat the paints axe nutually distinet.
44

---

Published as a conference paper at ICLR 2026
It takes la b a : Point) as arqunents in order, with Point b being the ona that As. batween Peint a. and Foint 5o vo can toralizz the clause es: "betwoen G I",
following clause "Naong the distinct points B, J, E, peint J is berasor, can formalizes in the exact same way.
Tharefore, formalize the next clacses followe:
"batwoen G I", *botwoen B F*)
The clouse "The rotio of scancat GJ to sogncnt 1J equals the ratic of secment EJ to semeett EJ, H. J. J" has potential dizect Fosnalization in the guidelinea:
denoted J.
equllennthRatiess
He double cleck the deaceaption of the "aqualangthilat ios" relation: fequality of tvo segnent- leagth rariaa: (JAB] / (22 = (122) (QE)). This is real-nunber equation) nea-zere-length quard enforced*, is indeed equivalent
Larget clause.
It takes la a q Peint] as arguments in ordar. Cherafore, the paranetezs a, a corresponds cuncrele argunent and J, the parameters corresponés and J, the parametees pasanatera 9, cozresponda co
correapanda and
formalize
clause follons:
"euuaaanttiacccce G IIJHJPO
Rounel usions":
The clause *The triangles Weriangle G & and Weriangle F.F. are sinilar, denoted Wtriangle has polential dizent Tornal isation guidelines:
a J Wiriingle
trianglasBniiaar.
Me double cleck the deacrsption of the "similar" relation fons "Lrianglea ABC and DEP sinilas ifC: (1)
Mangle BDF, Wangle angle ACB Vaanll DF3; (2) corowegonding sides are proport ionall: [AB1/1BR] 18C1/18PI BC /12F) = /CA//1F3)- The ouzeesgondence is A8-22, Be-sE, De-28. No non degeneeaty is assuned". is indeed eguivales
correeponding angles equal: Mangie
Margle DRF,
target clause.
check that point corsesponds to the paint I, the point cocresponds Lo the point P, the point J corresponds to the point J.
"triangiesStriier relation takes (a. c
Pointl argunents orcer. Theretore, perameters o, b, c correspends our concrate argurents G, H, d, the paraneters d, e, corresponds to 1, 3, J, d0 we can furnllis isse the clause as follows:
*erianglesSimila
Pornslized Statement:
3etore converting the Fornslized Structure into Fornalized stateneat, geonetric objects that nentiored in the clauses Tormalized Seructure as variables.
ceciare
According to the guidelines, sinse all our declared variables will be bounded by s universal quantitier W clauses of Formalized
fersll.. shoulen't declare extra variables that not nentiored Structero.
Me will exanine the clauses in the Formelized Stracture one by one, and declare variables for the mencioned geontrric objects in
The first cleuses, "forntriangle R GB HJ d8', and "fomteiangge T P.d TP 7d ar', reguiiee the declaration of Points: G, B, J. I, F, and Linos: GE, BJ, co, IE, EJ, JI.
clacses, "diatinnttoi declorstion of Lines: HE, GI.
uP,, "nisttinetoo
requires soditional
The semaining clauses require additionsi declarstions.
Theretore, ve need to deciare all and only the tollowing gesmetris cajects as variablet:
(G Point)
Line)
Now xo con combine the doclorations, premises, and conciusicas to ccavert the Formslized Structure to Fermalized Statencnt. According to the quiselines, we will do the tolloving:
quantify the doclared variables correstiy.
2. Uee the confunction of all tornal clauses in the prenises as the antecrdent.
3. Use the con inntuction of all fornal clauses in the conclusions as the consequeat.
Connect the aatccedent
with implication (->). Mzap entire Fornslized stasement wita triple argie brackets Sean exprescion here Sase for parsing.
Finally, NO have the Formalized Statement:
Witorall i0 CEJIFE Point) (GH fermtrianyie I IF FJ JI Wiaad aistinctFointtcoidnn B F H2 Wiand clotinnteointsenndde G d2 W
EJ EF : Line), foumtriancle
8J
land wonobisttneciinnete www.LLiinnnnneessccee wnteesstttc.ooitt aI HP Wiland between J I. Wilnd between E J.F. Wilnd oualleaethBarios
triangiessiniiar
45

---

Published as a conference paper at ICLR 2026
D.2.3 PROOFNET-HARD INSTRUCTIONS WITH LEARNED ABSTRACTION
You ven Eng' iish Stat anent of nathenat foxl theoren, Target andi rorments Tean 4.2.0-re2 with Michlibe NOT
depresated iden Use only
4/Hathiibe
Your Leok is to Curmalixe the Roglish Scalmment inko Cornal theoren in Lean usang Lhe Nathlib Library and Isbrarien, strictly adhering to tollowing torall defirisions guidelires.
Stre set of helpers +ABRRECTYY USE. in an Mathlibs
ingort Mothilo
This file extends Mathlib with a snall, self-cortai coll fon of reusable definit lons used in undergratiuae level formel lisasion tasks, The design erghasizes generality, concise raning, and consistency with Kathlib conventions.
Con en:e:
Tterated
map VinathborRjaed and recursive seguence: "mnresi x aget (2 sart (0) on Vimetbb//R/=-0
"nnres
the nennegative real eqet (2) "nnreal SterrgrtSeg' the sequence defined 8 (21, 8_inil] sgrtt (2-agrt (8)_
Simple sequence predicates exarples:
"Strict yleendedkhooelyy scriet upger bound predicate for seguences
"ogrt Suc:Dct
the real sequence e. |+> sqrt(n-1) eget
Comparabliity topologies:
"Eppologtescooparssiee t Wier o
Subbasis and generated topslegics Masthabii):
"sSuabasisTor" tanily suboseis cogology topolcgy is generated trom Toverliimi Subbesie" and tergentreytopol (lower limit Sergentrey line)
#attRocppp' "rcpplooySubbasse""" and "kIepslogy" (K-topology ca Vinachab(3))
rational intervals)
Pointwise convergenes on set and limit points:
Internte the type Ise
the powiamitoonndiiinessva.. : peintvise
pawsogoaUnittatee
fcnctions
interval
"Pintti seConvergentn" pointwise convergence or a set
"IolinitFoiae" and "AiittPointCompact" Himit points and limit peint compactnesa
Neaced nenenpty fanillea:
"astaatloocdtoonapty""" antitons closed nonempty families het.:ddciooctoeammeeeeeeeeteeeee their intersection nonempty
dofinitions narked with "B[simo!" zoquested.
acncomputablc scction
open Real Filtor Set TopeloginalSpace open seaped KNBeal
The [[simp]
Mmathbb (R)240 given by [+> agrt sort (0)", +/
def nareal nareel8gs 1211eaagg
Wllnnl seat.aqrt
Maathbb/RR)
boat-agrt_neanneg MMrangia
for The nonnegative ive real number (21". -7
a[sine]
def 2ireel MnactbbrRRse6
Vilangle aget, (2 Maachab(R))) aqrttraa__ 2Virangle
I The recursively defined sequence (iaathabb/)))4e; sqrt and (arl] sqrt r))", D[sine]
def ImreellieeSqrtte ((aL)b61)) > Miathds(Rioo))
I C nnreal8qrt2
merealigtt.21ussttt I
for à predicate expreasing that a sequence "s Miaathbrr)) >> Walpha is acrictly bounded above by "e"v <o.
i.e. "[iforall
e(sing!
Beriedlyeuundedteeveayy Maalpha Typex] Malpha
[aachab/[]] +> Malpha (c Vallpha
Prop :- Worall
real sequence "n 1.5 (gro agrt (a)
M[sing]
def agrtSuoebifff Viaathbo(N11 Moncchbb/R3
Beal.sget (nnchbbrR)) ()) agrt (mathbb(()))
for Two topologies on the same type are comperable if one ie incllded in the ot her fis. de Wlre de (T).
#isingl
Topologien iopologiestooparaii (Walphh Typex) It Topal ogi Space Vallph 3 Prop =
46

---

Published as a conference paper at ICLR 2026
Wioz
(-- a tamily "s Set (9ct XI" is cuabasis for topoloay "e" on 1X"
"e" generated "8" [[sine]
def IsSubbacisfor IX : Typо*) 18 : Sct (Set XI) ( Topelogical@pore XI Prop 17
Sapological$pacs.gemm www.saaaa..arrraaooooooooo S
The generating fanily the lover limit (Baxgeafruy) Lopology on (Maathab(R)" all half-open intervals [a, bi" with "a < b", [[sing]
def Lewerlinittelbaaia Sel (aatlab(a)
[0 Mexiats a (R)t
Wiland 0 Set.Ico a bJ
f- The loaes limit (Bozgenfray) sopology on (Raathbb generated by [[xing]
1"."" 1".
def sorgeniteytspoloy : "apolocicalSpace (Ba := Iopoiool:salppaee.coo www.aaaac...ee..o.oooooooo.. Lonertanitsubbazia
The set "X :- [ 1/a I Man (Mathab(N))+ Maaabettg (inataa((R"', used definition the K- tepology. -/
[iving]
daf KlatBeaip Bet (R) PHat, (1 (RIthba(RR) / ((c (lnachbb(R]) (mathaa
ix Wexisss
f-r The generating fanily for the K-copology on (Blaathb/BB""
all open intervals "ta B[aing]
punctured intervals "la, b) Kt.
daf KiopolagySubbaai Bet (Bet (11athbb(R]] :- 10 Veexista b MawchabeRs, < Wiland 10 Set.Ton Wler 0 Set. Too b KNetReo
The <-topalogy "Mimathab gonerated by aubbasia consisting sots of the form (e, h) and (e, b) K', where "X - R[xing]
( 1/n I n Win Miethhbb(M) 1", -/
kTopology Topologicel l (lathbo/RR Topalogies Space.genersd caneeateeooo efron KTegologySubbee
for The generating familyy for the topology "Mostsbo(Ri" with basis of intervals having VinatibbOO)"
rational emdpoints: "Ioo M[aine]
b".
def Racional Tondubbasis : Set f8e: (lnachbb/R13 :- (0 I Vlexiata bbb Mowchabros, < Wland D Set. (e Moatlab(R() (inthbb/RR1)
The topal ogy on "unethbh12)" generated by the sahbasia of open intervels with racional endpoi nta. -7 [[sing]
det realTopol wyyoolooyrreemooiionnn
Topclogica 18pace VincchbbiR) TooSubeesis
Topal ogt gewse.generatee aeneerateerrn
for The unit interval "10,11" seen as a subtype or "Vlmatbb/RI"", -/
egsingl sborev Unit Interval "ype Set (C (imec 1
fo- The sequence of functions on the unit interval "[0,1]" given by (pondeghndni it interval n) x stn". -/ disingl
powseginntnt Interval 5 UnattbbiNN UnitInterval Vimatbbo for n (e (lnchbb(RR))
f-r The pointwine linit fonction "10,11" sesocisted with the sequence 'x 1-> xtets is "p" for "x #isingl
othervise (in particulor "x 17). -/
def pootinitonntiit
Intt -> VinachbbRR) :-
Ix Ammatab/RR]
Pointwise convergence on eess a sequence of functions "F Nonethbb[N) -> X Wheta converges
pointwise on "s" to 'q. x -> Wizeta " 12 "Uiforall Minn 8, Tenaste isun -i F n.n X) attop (ohdd (g X1)".
-/
2isingl
det foiatwiacionverresn (x Vibtta : Typos) [TopolegicolSpacc Wazeta ]
IF : Vinathaa:Ki -> x -> Vibeza [g X Vibeta is Set XI : Prop 1" Miforall Winn Tondsta (zun
attop (ahds x))
for A point "x" is a limit point incoumulation point! at a subset "A" et topologica.. space "x" if every naignbethcod of "x" neets 'x \. IxI". Bisingl
Typest [TepologicalSpecc XI IA X) Ox Prop Wiforall U Win rhds x, (3 Voop IA (X11) Reacepty
IelimitPoint
f-- capological D[sine] det CanitPointCompact (X Types] [TopologicaiSppce XI : Prop 1- Woorrlll A Bet &, A.Infinita +> Vexisss
limi
if every infinite subset lini: point. +/
IstinitPoint A
nested (decreacing) sequence VanthabiN)) Set X" closed, nonempty sets topolocical suace:
"iacitone Viland MMtorrall Isclosed (C a)) Wizad MMroral IC 6) Noncmptyy) -/
etaine]
def KestodilesodNooemeyyy (X Zypex) [Zopolecica1apace X] (C (Mn Sat Prop Antitone a Wiand (Witrrall n Vimatbb (N), Isclosed 12 m) Wandd (Mirorall n. (inathba (C 2).
Nonengty!
The propecty that every nasted (dccrcasing) sequense clased noncmpty subsets at "X"
47

---

Published as a conference paper at ICLR 2026
has conampty intersection "Mibsgopp B, 6."".""
[[sinp] det Necootieedioorrryyeerooooo IX Typex] (IopoLighoallSpaze X] Prop
Moraall Vinathb Set Ancitone
Metorall n. Umstabo/Kl,, Isclosed IC n]] +>
(M1orrall (iattbbajH), (C at .Noonnpty) ->
(aligaap Nenempty
Envicunment
Fosnaliza an Enelish statemant Lean using +.OILY.. Mathlib
**N0** other libreries or impert should be used.
Rovironnent: Lean 4.7.0-zo2 with Nathlib4. Uae only cuzrent Lean 4/Machlibb iden.iflers. Do NO? Jse Sean
3-eza
2. Porbidden Lean 3-Eea Ident iflera a Notat iona Idantifiars: "Converqunt",
srnelinttroup.cuotiin bourdee. "IsFerfact
'Bea'.chet',
Notationss: "Viaathh "2[LI", zaa "Mint (mathāb(B3, Nidota", binder aborthand "Moorall Viin 5, Nicazs", negstive exponents with 10.9., (-pi")-
Use "hingflon" / /'Alglion" Inot. "Function. IsFieldFon")
Uae "Buboreap.Peeceett
"quctlenttroup. quetient"))
Usa "2ornoooyyIsBoonnoo Iodounddd g" (noz "Matrie.bouaded E").
Avoid Reall.cbet use "Beal.spus" or cational expurents.
You need Lo generale <.B0TE the beader the Uhwaren your reagonaee
The +oOKDx. import stat antan you should generace is "Import Mathlib". After that, write "apen ..." and "open spsped ..." for the namespaces you need to use In the theoren, the <MAKE SUREs
you using upened
Please check Uhis i0
you receive аулсаx arrora!!!
4. Thauzen Posnal: ALMAYS include Uhworen
and HUST be wxautly "Lhm_C". (pazans) corclesion to sorry'
"theoren You LNDSTA use "by sarry" es the placebalder, Da o.00 generate prooft!! Notu that some fermalisationn of statwmet night not have pasametera abindeee,, only the Lype/goal. Pox example, "Prove that (ogrt(33)2)))osss (31 1319 is irracions), can be formalizen "theoren thn O sorry"
Regui
Terational (2-
331 Minchib
You should Lay to uae binder/pazanet form as mach as possible. Por examlle, tay to convert. existential scaterents to universs] statements y so that you can use the binder/paraneeer form.
Parameter
explicit parentheces for pezoneters/oinderz "(VlOnegs Bet Vmatabb/CH (E nathbbiC) Wnathhb//Gl (h Ts0gen Vinneg I", NEVER use iegi "(1innga 3",
Barameter/Bindes Naming:
For ooject neres,
exemple, if problen aent lona "coplle funct ion 5" Lhen you should name the porsespurding parameles "f" like "I W. machabiC) -> VimetaberCII"
nemes
in pres
For hypothesi names, the ohject with prefix "h" and index then from 1, For example, if the problem mentions "complex senction. that holonerpaic ther you should name corvesgonding hypotheeis "ht_1" Like (at_] : Ditferentiableda Minthbbici t XI".
Reasoning
xrite This is +EXTRSMELY CRUCIALl Please do not skip this!!! +VAY EXIRA ATTENTION TO THIS!!!++
caretully step-by-step
your incernediace reasoning stepe
finel Formel ined Statement,
there exarples provided the you must strictly follow the fomat and reasoning in the exampiss!!! AIIINN EXISA aARD!!!
3. Response Format: Mothlib
Return the header and the theoren togecher, aurrounded by triple angle brackets sec inport
open
open sogged ...
theoren
by sorry
Do ++ includo +* comeente or proot tactics in your final zeeponse! !! +*PAY EKTRA AITENTION TO THIS !!1ee
Example of CORRECT outpet (deciare all variables, cane must be thm
<<< Import Mathlib open
scaped
chooron tha Witorall R (Hsthbb(H), Wexitst bm H, (3xn42) PPrin Wilad (3<p+1) >n R by corry >3>
Example of INCORRECT output (xrong theoren acme, missing varialole declasation, includes commcnte, missing by corry"):
<ec import Mathlib open scoped ...
sonte random comment
randon_iane Mexisce (Eriai) Eerine Wllan (3xne1)
D.2.4 PROORNET-HARD ONE-SHOT EXAMPLE
48

---

Published as a conference paper at ICLR 2026
Bere an example:
Seglish Statement:
'suaset Amatabe [C)8 be (ncn-enpty) conracted open lot SELAS ba pequenes oz holomosphic functions detired on SU9, Suppose tast 9tnns converges unitornly to a runction 629 on every compact subset of SDS. show that 825 is holonorphis in $28.
Beni -ani-Foznalizd Scracture:
soni-formalize the Enelish Statenent into nested structure quantifications, prenisea conclusione, we xill excmine the English Statement sentence by sentenee, and break down each gentence into natural lang-age clauses that are atonic posaible.
/+
englyy connected upen and let 9 seguence holonarphic functions defirad on SUS.* indicates that choice and Sc are acbitrasy, s0 we should choese the universal quantifier for the entire statemant that quantifies over SUS, $f_ns, and pussibly other variables.
Yaubout hibi
Since SE_88 sequence functions cortain properties, will furthar break it into nested sub strumluc., Now, ve will fleat universally quantily over $UB as follows:
x/
"quant ion""tion:
possibly variables",
"preni sua":
/+
The xentence First declares that 508 is subses of the complex plane PlmechbbiC19, that it openn
exply, connected,
Lhe lollowing posnisws:
+/
*815 is subset of the complex plane Wimathbbc]15.
1838 is eaply",
connected",
*905 open",
/+
The sentence also declares that m8 is sequence of complex Funct tons, have the fol collowing prenise:
</
*g n5 is sequence of fonotione from (bCst to (1m1t
break down the apecitication St_ns, sequence holomorphie sunctions detined on Recall our nathenat teal kroul crouledge, seguence is countably indexed, which neans that for a Vin (nathib(X)s, $1_15 is holonorphie un sUS.
By the definition onorphie fonction, complex differentiable as every point sus.
$f_15 fanction from 511 #lmethbb/cis
"herefore, break it into nested sub-st ructore by universe quant iyring Bng Fol Tows:
"quant i flcat ion's *for I Bi5", "premisoo"; I
natural
iie, Vin \mathbb/N15*,
*soncLusione":
*st 18 in the sequence n8 holonorphic SUS, which neans that $f_19 19.1 is complex- diffcrentiable at every point AUS*
centence "Suppose that Stund converges unitorm.y to a tunction $15 on every compact subset 902" caticstes that there exiats a function 9F3 with certain property, which indicates a nosted exisccatiel quartifier over $29.
is holonopphie sug* requi Thersfore, the correct conciusion should really be "Show that it there exists a functions $29 such shat nt converges unitormaly to 9td on every conpact subset ot 509, then 919 is holonorphic s0s".
conclusion
declared beforehand,
According to the guidelines, xe should convert statement to universsily quantsties as much as poseilee that later se can casily formalize then in the hinder forn. Recall our mathenscical knowlerge, is limit exiets, it conclusion as of $U5, 525 is holencrphic in sus*.
resrito the exictentisi quantified all StS, euch that st_nd converges unitornsly
every compast subset
In addition,
other prenises before depends our zop-level quanticications 1.c. SE5 can quantificd outnest universel quanticier.
quanciflcation SE6
Tharefore, vo declare SI6 as Iollows:
*0es runction tron Pimachabici9 Pimsstabici"",
/s
Hex can break down the epecification sn sE6, a runction that for all conpact subect 5xS of SUS, the sequerce $c converçea unifomnl scs which indicates nested universal quanticies ovez 6XS.
ThareCore, break it inso nested sub-atractuze by universally quant 8X3 collowa:
49

---

Published as a conference paper at ICLR 2026
"quant io all 8x5",
"pramises"; I
*685 is a cubset of AU91,
rexS is corpact"
conclusione":
"Che sequence BI converges unifornly 928 885*
1.
"conclusiana":
zontence "Show that SE9 holonorphic sUs* means that BES complex-ditteran every point of 988, Since we have declered 519 beforehand in the premises, we con directly zefer the name SE9 in Lhe conclusion.
Therefore, have following concluxion:
1/
*826 is holonerphic on SU8, which means that 8ES is complxx-differottiant at evezy point of SU5*
Pormalized Sizucture:
To convext the Beni-Fornala Scructure into Fornalized Structuze, vo will exanine the natural language ir the is well furned and well deflned sccording to the guidelines.
one by
+/
First of all, we not ine that the prenises and coselus ions in the Seni Seni- lixd St ructure are quart if fied universal quantifiuz oows sUs, Accurding to the guidelines, for outioaa anivecaully qladt ststements, should
possible.
Theceforw, we put no formal quancifier over 806 in the Pornllied Btructare, but anavead fornaline the gremises reus is subset the complex plane Slmethbe(ci5"% "st9 is non-eraty", rous is comnested, barders like someltype)' (hB_1 some.propenty.oo
"quant ifi cet iont: tomitted since we will use the binder forn*, "greni swa":
should fornell the prenises one by are. The first prenize *8n8 is subset of the complex plane 8 slmatlob(c)s". check the provided helgers and recall our knowladgge of the required vereiors tean and Matalib in the inee,, there is direct corresgondents ot "the set up
complex numbers", so aliecnativell..
equive wey fornal iiee this
Me noticee that this preniiee is eeulwelert just aaying that $u8 is of complex numbers. Therstore, ve can use type tormer "Bes" and complex number type "Umattbbic]" to say that SC9 is of type "Set Misthobrd""",
Tharetore,
tormalize this premise tollows:
*UU : Set hbbhhCh))))",,
/+
The prenise *sus non-enpty", Check the provided he pers and recall knowledge roquired versions of Lean and Hathlib quidelinas, shore relation 'Nonenpty', Theretore, we can tomalize this property ot aus as collows:
corsesponding cormal
./
1h0_1 Henempty
The next prenise *9u2 se connected", Check the provided helpers and recal) our knowledge the required versions of Lean and Hathlib in the guidelinas, thare is direct correspording formal relation "Istonnectes", Theretore,
tomalize property gus tollows:
[h0_2 IsConnected U1"
Chesk the provided helvers recall kravledge the zequired versions of and Washiib in the quidelines, there is direct corcesponding tormal rolaticn "ZeOpen", Theretore, we can tormalize this property or 900 as tollows:
prenise *ous
-/
ih0_3 Is0pen
The next prenise is 196_n5 is a sequence of complex functions", Check the provided helpers and recall our knowledgs et the reqaired versions et Loan and Matalib in the guiseliaes, since a sequence 61
countably indexed, matbabi(C) -> Minttabb/0 when want talk about 615-th runction in the sequence, can use the function application notation "tin 1".
the curried function tyse (Viatthok W
Tharefore, formalize prenise rollows:
[C_0 Vanachbb/N] >> (CathabbC)) >> Minatbb/CC)"",
prenise universally quantified statenent sub-struct struascre) about each #1_18 the sequenes st_efs ffor all 81 vin Anathbl (8) we have *$5_18 in the sequence st is holonosphic on 509, which means that $EL18 is comploe-dt.ttreeniiaab at avezy poin: of SUS*.
send- Commallaaa
50

---

Published as a conference paper at ICLR 2026
*91S being natural numbez", check the provided halpara and recall our knowledoe the reqaized varsions of Lean and Natalib in the quteaziaes, we can say that 918 20 of type "Vantthob (3)",, so car ternalize the quartification over 918 as "Mrorall 1:1 (Aaathab
"98_48 conpiex-lliteeenttabbi at avery point of Aug*, check the provided heapara recall our knowledge of the required versions et Leen and Matalis in the quidelines, there is a direct corseapanding fornal rolation "Ditforontiableen to talk about Somplox-di by passing (1aatbba())
first arqunent.
Tharefore, ve can formalize this property of $6_16 au Collows: */ [[f__ul MMoral (hattha biffeeentiakeenn (enthta (f_n "
The next preniss is 1958 is a function fron Simatabo/Cis to Flastabb/C]3- Check the previded halpers and sucall our knowledge of the requiced versiona of Lean and Nathlib in the guidelines, of the fanation
say that
"Vinttbbe +> (aachab
Theretorw, ve can formalice this prenise as Collows: */
The next prenise is universally guantified statonsat la sub-structure in our strunicce) about each subses exs of S18; "ox all subeets eXS of 508, if EXS is conpect, then EXS*.
the sequence $1 convergea unitomly
Por *5x3 being a subses of $05*, check the provided helgers and secell our knocledge of the sequited versions of Lean and Mathlib in the guidelines, there is dizect corresponding formal notation the guidelines,
"Vauhheece ". llowever, according varisble first. Pherswooe, ve can funndiis the quant ificeiton uoes 5X8 as "Wforall maclab(C)" and the subsez relation as 'X Maubseteg U".
always declare type any
Set W
*5X5 being compact", check the provided helpera and recall knoeledge of the requized vecaioos bear and Machlib TaCerpaes', i Therefore, we can fornalize this property of 5XS as fol loll as "IsCopast X"
quidelines, there direct cocrespending fornal relacion
prows helpers knovleege of the required veraions of lean and Mathlib in the guidelines, there is a diress corresponding relation "Tendstolall fortollliifuuoooo Fonnlyon P. 1 X' for "B ; Miota -2 Vallla -> Vibla and Wbeta along filter "1", Here "p" is the limit 'E', the indes filter since we opened namespace "Filtez"), ", and the sut is "X", Be can formallze the conclusion of this quantifien statement as "Tendetouni form you WVSla n => i n 81 aop x",
sequence
converges formoyy to 518 5x8", check
"F Walgha f.n
"ap""p" sequence of forctions "Waanbde directly
Therezore, sesentling every piece together, we can toraalize this univereslly quantizied statement Followe:
iht 1 Wrorall X Sez VinennbbiCi, Vasuseteg 3. Waadd IsCompact X +> Tendstolhitomiyln (A) lambda
Top XI",
1. "conclusions":
Za
conclusion "529 holemouphic on sus, which means that complox-ciiterenttiee at every point or sus", Check the provided helpers and recall our knowledge of the required versions ot
lean and Machlib in the gu ideell inellnes, there is a direct corresponding fornsl relation oirterenciableon" argument.
taix about somploxeddtttreentiiiiii
passing VinathbbCC) the tirst
Tharetore, we can tormalize this property of 8t5 as tollows:
./
"Dittercatisblenn Vinaskabld; E u"
Cornslized Statement:
Now
the Formelized Structure Formslized Statement. According guidelines, will
the following:
1. Assemble the quatiitiaation, premises, and conclusions properly inte Formslized Statement, Hame the theoren following quideliaes "tharo", Jse correct systax if usiad the binder Msap the entiro Formslized stascment with triple angie brackets (eee Sean exprossion here sese for parsing.
Finally, No have the Formalized Statement:
theoren thn_0 nathib(N) -> Miaatbeecc) >> (instab(cc) (ht_n_1 : Witorall n:: (aatabb Sirserentistisen Manttbbb CI (t_n b) b) it (iaateaaCC -> Vinasaboic (ht_1 : Witorall x i Set Vimstabbio), X Vouheeteq J. W land IaConpact x Tendstotaifommyen (Vilanbaa fon attop Dirferent iabledo nathib(C) f by sorey
Set Wnatnbbici cut. Norempty th0_2 reConnected ShU Teopen UI It_a
51


Reviews:
[{"review_id": "S6d1ok1qUp", "reviewer": "Reviewer_mecL", "summary": "The paper “Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning” introduces DNA, a zero-training framework for translating informal mathematics into formal languages. It combines abstraction learning, which extracts and formalizes reusable concepts to extend target libraries, with hierarchical decomposition, which breaks complex statements into manageable clauses for accurate formalization. Tested on LeanEuclidPlus and ProofNet-Hard, DNA achieves up to 8.6× gains over baselines and enables strong generalization to low-resource languages, showing that decomposition and abstraction jointly enhance autoformalization performance.", "questions": "- What are the algorithms for step 4 and 5? And how to interpret the results of Table 3?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "- Dividing a complex task like autoformalization into multiple stages is very natural, and I particularly appreciate the authors’ idea of constructing a dependency graph.\n- The training-free framework is appealing and offers good portability.", "weaknesses": "- The core operations of 'abstraction learning' and 'hierarchical decomposition' are not rigorously formulated. For example, abstraction learning is described as extracting three types of concepts—definitions of mathematical objects, relations between objects, and functions mapping objects to objects—but the boundaries between these categories (e.g., relations vs. functions) are unclear. Moreover, the expected formal output for complex informal statements (such as “the space of continuous functions from a compact manifold to a Banach space forms a complete metric space under the supremum norm”) remains somewhat vague.\n- The paper lacks a qualitative study, particularly on non-Euclidean problems. The chosen Euclidean geometry tasks appear somewhat artificial and simplistic. It would strengthen the work to validate and qualitatively justify the proposed framework on more realistic datasets such as FATE [1].\n\n[1] https://frenzymath.com/blog/fate/", "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": "AqZMgosk43", "reviewer": "Reviewer_HnGH", "summary": "This paper proposes Divide and Abstract (DNA), a two-stage, training-free framework for autoformalization of mathematical statements. The Divide stage first extracts common mathematical concepts from a corpus and formalizes them into reusable abstractions. The Abstract stage decomposes each statement into structured informal clauses and uses the abstractions produced above to formalize them. Concretely, the Divide stage consists of concept extraction, concept filtering, concept dependency graph construction, concept formalization, refactoring, and documentation update steps; the Abstract stage consists of decomposition, formalization, and composition steps. Evaluation on subsets of LeanEuclid and ProofNet demonstrates the effectiveness of the DNA method across many LLMs.", "questions": "1. How are the correctness and recall metrics in Table 1, Table 2, and Table 3 defined? The main text does not appear to provide definitions or evaluation protocols for these metrics—please supply precise definitions and describe how they were computed.\n2. Dataset choice and subsets. The paper evaluates on subsets (LeanEuclidPlus and ProofNet-Hard) rather than the full LeanEuclid and ProofNet collections. Please clarify:\n   - What specific practical difficulties may arise if one attempts to apply the DNA method directly to the full LeanEuclid and ProofNet datasets?\n   - Will the selected subsets and any scripts used to produce them be released publicly to facilitate reproducibility?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1. The overall approach is very intuitive, while the experimental results show that it is effective. The results in Table 5 and the analysis in Section 4.3 indicate that the Divide and Abstract stages are complementary and produce synergistic benefits; in particular, their combination appears to yield a substantial performance boost on LeanEuclidPlus.\n\n2. The proposed method has high potential value for low-resource formal mathematical languages. Beyond low-resource languages, it should also be effective when facing rapidly evolving formal languages (for example, different versions of mathlib in Lean 4 as noted in Line 106). This aligns with the current trend of fast development in formal systems and their mathematical standard libraries.\n\n3. The paper addresses a long-standing but thorny problem: [missing mathematical dependencies](https://github.com/jsm28/IMOLean). The lack of formalized expressions for certain mathematical concepts in libraries such as mathlib creates difficulties for formalization; this issue has been widely overlooked by many autoformalization efforts. This paper partially addresses the problem by constructing the Abstract stage. (Although the example in Figure 1 is a simple composition of concepts, fully and rigorously formalizing complex mathematical concepts and structures and feeding them back into libraries like mathlib remains beyond the reach of current models.)", "weaknesses": "1. The effectiveness of the Divide stage appears to be limited to problems the LLMs have not seen (e.g., certain geometry problems). From Table 5, the performance gains of Divide stage on the ProofNet-Hard dataset are marginal. Those problems largely depend on mathlib (which is likely included in LLM pretraining data).\n\n2. The experimental baseline setup is somewhat misleading: Line 292 states that helper definitions are withheld in the baselines. Given that these Lean definitions are typically absent from training corpora and resemble a DSL, withholding helpers imposes an unnecessary handicap on the baselines and may exaggerate the contribution of Divide. A more reasonable comparison would retain the existing pipeline but add a baseline that is provided the helper definitions (without the Divide stage).\n\n3. The method’s generalizability is questionable. The approach seems to cover a single topic well, but extending the same method to other domains or languages appears to require substantial prompt rewriting for each component of the whole pipeline, demanding significant effort and therefore limiting transferability across different DSLs or math domains.\n\n4. Minor issues suggesting the manuscript may have been prepared in haste: the code link given on Line 29 does not contain any actual code; Line 37 mentions \"three transformative applications\" but does not specify what they are; and on Line 160 both quotation marks are closing quotes.", "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": "UIG3urLCCs", "reviewer": "Reviewer_v3kv", "summary": "This paper presents Divide and Abstract (DNA), a novel zero-training framework for autoformalization that addresses the generalizability challenges in translating informal mathematics into formal languages. The framework consists of two phases: Phase I extracts common mathematical concepts from corpora to extend the target language's capabilities, while Phase II decomposes complex statements into structured clauses for systematic formalization. Evaluated on LeanEuclidPlus and ProofNet-Hard benchmarks, DNA demonstrates significant performance improvements across multiple model families, achieving up to 9.6× gains compared to baseline approaches and enabling smaller models to match larger baselines on complex mathematical statements.", "questions": "The abstract mentions that code is available at https://github.com/anonymousauthor567/DivdedAndAbstract, but the repository appears to be empty. Will the code be available?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1.The framework's combination of corpus-driven abstraction learning and hierarchical statement decomposition represents a novel contribution to autoformalization research, addressing fundamental limitations of existing approaches that rely on direct generation of complete formalizations.\n2. The comprehensive evaluation across diverse model architectures (GPT-4.1/5, Claude-4-Sonnet, Qwen3 variants) and benchmarks demonstrates consistent performance improvements, with particularly impressive results on challenging domains where specialized models previously failed entirely.\n3. The zero-training design makes DNA highly practical for low-resource domain-specific languages, eliminating the need for extensive training data while still achieving state-of-the-art performance through its innovative abstraction learning mechanism.", "weaknesses": "1. The six-step language extension process and four-step decomposition pipeline introduce significant complexity that may limit adoption, particularly for researchers and practitioners without extensive expertise in natural language processing or formal mathematics.​\n2. While the paper demonstrates performance improvements, there is limited qualitative analysis of how the learned abstractions compare to human-crafted ones beyond basic correctness metrics, which would strengthen the validation of the framework's core innovation.", "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)