Tree-Based Premise Selection for Lean4
Authors: Zichen Wang
Anjie Dong
Zaiwen Wen
Venue: NeurIPS 2025 poster ()
Keywords: Premise Selection
Formal Theorem Proving
Lean Proof Assistant
Expression Trees
Structural Similarity
Weisfeiler-Lehman Kernel
Tree Edit Distance.
Primary area: machine_learning_for_sciences
TL;DR: Structure-first, training-free premise selection for Lean4: CSE trees with WL screening and TED reranking that beat semantic baselines on Mathlib4.

Abstract: Premise selection is a critical bottleneck in interactive theorem proving, particularly with large libraries. Existing methods, primarily relying on semantic embeddings, often fail to effectively leverage the rich structural information inherent in mathematical expressions. This paper proposes a novel framework for premise selection based on the structure of expression trees. The framework enhances premise selection ability by explicitly utilizing the structural information of Lean expressions and by means of the simplified tree representation obtained via common subexpression elimination. Our method employs a multi-stage filtering pipeline, incorporating structure-aware similarity measures including the Weisfeiler-Lehman kernel, tree edit distance, $\texttt{Const}$ node Jaccard similarity, and collapse-match similarity. An adaptive fusion strategy combines these metrics for refined ranking. To handle large-scale data efficiently, we incorporate cluster-based search space optimization and structural compatibility constraints. Comprehensive evaluation on a large theorem library extracted from Mathlib4 demonstrates that our method significantly outperforms existing premise retrieval tools across various metrics. Experimental analysis, including ablation studies and parameter sensitivity analysis, validates the contribution of individual components and highlights the efficacy of our structure-aware approach and multi-metric fusion.

Tree-Based Premise Selection for Lean4
Zichen Wang
Anjie Dong
School of Mathematical Sciences Peking University, China princherwangggmail.com
School of Data Science
The Chinese University of Hong Kong, Shenzhen, China anjiedong@link, cuhk edu.cn
Zaiwen Wen
Beijing International Center for Mathematical Research
Peking University, China wenzwēpku. edu. cn
Abstract
Premise selection is a critical bottleneck in interactive theorem proving, particularly with large libraries. Existing methods, primarily relying on semantic embeddings, often fail to effectively leverage the rich structural information inherent in mathe- matical expressions. This paper proposes a novel framework for premise selection based the structure of expression trees. The framework enhances premise selection ability by explicitly utilizing the structural information of Lean expres- sions and by means of the simplified tree representation obtained via common subexpression elimination. Our method employs multi-stage filtering pipeline, incorporating structure-awar similarity measures including the Weisfeiler-Lehme kernel, tree edit distance, Const node Jaccard similarity, and collapse-mate match sim- ilarity. An adaptive fusion strategy combines these metries for refined ranking. To handle large-scale data efficiently, we incorporate cluster-based search space optimization and structural compatibility constraints. Comprehensive evaluation on a large theorem library extracted from Mathlib4 demonstrates that our method significantly outperforms existing premise retrieval tools across various metries. Experimental analysis, including ablation studies and parameter sensitivity analysis, validates the contribution of individual components and highlights the efficacy of our structure- approach and multi-metric fusion.
Introduction
Automated Theorem Proving (ATP) is core research direction in the fields of Artificial Intelligence and Formal Methods 2 When constructing formal proofs, especially when faced with vast and continuously evolving libraries of mathematical theorems, key challenge is efficiently identifying relevant theorems, lemmas, and definitions from a massive pool of candidates. This task known significantly narrow down effective search space for subsequent proof generation, and it represents a critical bottleneck in achieving practical automated and interactive theorem proving systems. In recent years, with the development of Large Language Models (LLMs), Retrieval-Augee Augmentl- Generation (RAG) architectures have garnered attention in the theorem proving domain 4.. In this architecture, premise selection serves as the preceding retrieval step, and its performance directly impacts the success rate of subsequent proof generation.
as Premise Selection 2 3 Efficient and accurate premise selection
specific type formal system called a proof assistant, also known as an interactive theorem prover. These software tools are designed to assist human users in constructing and verifying mathematical proofs or verified software in a strictly formalized manner. Popular proof assistants
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

currently include, Coq [5], Isabelle [6] HOL Light [7]. Metamath [8] and the increasingly prominent Lean [9 [0] in recent years. Notably, Lean, with its powerful type system and active community, has fostered comprehensive libraries such as Mathlib [II] and Optlib [2 containing large amount of formalized mathematical knowledge. Efficient premise selection within these proof assistants possessing large theorem libraries is crucial for users performing formalization work. Currently, in the Lean formal proof assistant, mainstream premise selection tools, such as Lean State Search (15). Loogle [6]. Moogle (17], Lean Explore [8] and Lean Search [1]], typically employ methods based on semantic embeddings of target states, theorem statements, or mathematical expressions. They often fail to fully utilize the rich structural information inherent in mathematical expressions.
Given the inherent structured nature of mathematical formulas, machine learning research in the field of theorem proving began exploring how to leverage the underlying structure of formal statements for representation learning quite early on. This direction typically involves parsing formulas into structured forms such as trees or graphs and applying corresponding machine learning models [20+23] Early attempts combined formula structure with Convolutional Neural Networks (CNNs) or Recurrent Neural Networks (RNNs) 124 25 and evaluated their capabilities tasks such as proof strategy development, premise selection (26), and capturing and utilizing the structure of logical expressions 277 on datasets like HOLStep 24 As research deepened, neural network models specifically
designed for structured data, particularly tree-structured neural networks and Graph Neural Networks (GNNs), were more widely used to encode the structural information of formal statements [26 28
36.. These structured methods aim to capture logical invariances in formulas, improve graph representations BTJ, and have been applied to tasks such as higher-order logic proof search (29).
Furthermore, explorations utilizing structural information also include graph contrastive learning Collectively, these works demonstrate that explicitly modeling and utilizing the structural information of formal mathematical statements is crucial for improving the performance of machine learning in theorem- provinng related tasks. Although existing works have made important explorations in utilizing structural information designing a structured method for proof assistants like Lean, which have complex type systems and large libraries, that can both accurately capture expression structure and efficiently perform premise selection, remains problem requiring in-depth research.
47-40 and methods built upon theorem dependency graphs 41 42
43 44
To address the above challenges, we propose a novel tree-based premise selection framework for Lean4. The framework explicitly leverages the structural information of Lean expressions, aiming for efficient and accurate retrieval of relevant premises from large theorem libraries. We first apply Common Subexpression Elimination (CSE) to standardize expressions into trees, and then use two-stage pipeline: a computationally efficient, training-free Weisfeiler-Lehman (WL) kernel for rapid coarse screening, followed by Tree Edit Distance (TED) with principled fusion of struc- tural/semantic similarities for fine ranking. This unified design principle-struciin as complement- turns melti-metric fusion into consistent decision rule rather than ad-hoc stacking. To keep costs scalable, we separate offline bngerprinting/clustern bounded/pruned TED together with query-adaptive candidate budget. While instantiated in Lean4, the backend is language-lean; we envision the design of a lightweight adapter to facilitate portability to other proof assistants that expose (or allow reconstruction of) typed, binder-aware expression trees. We evaluate under a unified protocol and release code/configuration for reproducibility. Our main contributions are:
first, semantics
from online retrieval and employ
Structured theorem library and benchmark construction. We build a tree-structured repre- sentation of Mathlib4 and design two formal test sets for premise selection in Lean4, enabling systematic and reproducible comparisons.
Adaptive multi-metric similarity fusion. We introduce principled fusion of WL-cosine, TED, constant-level Jaccard, and Collapse-Match alignment under a structurecomppaiblity constraint, capturing both global shape and local edit consistency.
Scalable tree-based retrieval framework. We integrate CSE normalization, WL coarse filtering, and cluster- optimization with bounded/pruned TED and query- candidate budget, achieving superior performance across multiple retrieval metrics.
2

---

Expr Tree in Lean
WL Encode
Premice Selection
ME
Expressen
Consinint
Siilttty
Stage
Studiuiil Sinikrtty
Tree Edit Distance m larty
Matribi Cyti
Stage
Jasoard similaftt Const node
Pwence oM can 1
Nat. mull comm: Nettiter comm
We get 217865 Becorom
Nai..eti comi: Nul.wao_
Figure 1: Overview flowchart of our proposed tree-based premise selection method
2 Preliminaries
2.1 Premise Selection for Lean4
Premise selection is a critical step in Automated Theorem Proving (ATP) and Interactive Theorem Proving (ITP), aimed at retrieving the most relevant theorems and lemmas from a vast theorem library that are related to the current proof goal 22 3 relevant premises is crucial for managing large theorem libraries and reducing the proof search space. Lean4 is an advanced interactive theorem proving system known for its powerful functional programming capabilities and its continuously growing large mathematical library 9 10 In Lean4,
Efficient and accurate identification of
users decompose proof goals by applying tactics apply IW etc.) and existing theorems/lemmas.
As the Lean mathematical library continues to expand, the role of premise selection in enhancing the efficiency and scalability of the proof process becomes increasingly prominent. The complex tree structure and rich type system of Lean expressions pose challenges for traditional text-based or simple feature-based similarity matching methods, simultaneously highlighting the need for structure-awan and efficient retrieval methods.
2.2 Expr Tree in Lean4
In Lean4, the Expr data structure is the representation for formal mathematical formulas and proofs. It is a recursive structure that forms what is known as an expression tree (Expr Tree). Lean4 uses this structure to represent and process various linguistic constructs, including bound variables (bvar), free variables (fvar), constants (Const), function applications(App) lambda abstractions (lam), and quantified expressions, enabling efficient parsing, manipulation, and type checking of formulas. The Expr Tree maps complex mathematical formulas into a hierarchical structure: the root node represents the outermost expression, while each child node represents component of the formula. This recursive and hierarchical nature allows Lean4 to efficiently process, verify, and reason about formulas recursively. The node types of the expression tree are defined by the various constructors of the Expr structure, such as bvar, fvar, and lam, each storing necessary information related to the corresponding expression type.
For instance, the mathematical expression N - Prop p ir ++ Vy c N.x = represented in Lean4
as fun Nat forall y:Nat, y This expression is transformed into tree structure,
as shown in Figure 2 The recursive nature of the expression tree is fundamental to Lean4's efficient processing and reasoning about formulas.
Leveraging expression trees allows theorems in Lean4 to be modeled as structured trees. This hierarchical tree structure clearly expresses the internal composition of theorems and provides basis for measuring similarity between different theorems. By comparing the similarity of these expression trees, we can effectively quantify the structural and potential semantic relevance between theorems, which crucial for the automated processing and retrieval of theorems. Additionally, the proposed framework is language-lean, meaning that it is adaptable to other proof assistants, such
3

---

"he mish
The Litzr
The Louns sorel
Lorni Not LB
Cut Rat Forall 7 Ret, x
(heall cooe Nat
Capp
dellao
bear (entratarinee Bat)
LEWN
sert Lowall (a Lowes
Gearld Marld)
Arai
defaxx
cous Dleme (oecitene tuae (ax Jist Lawa))
(otreentae:: Nenel (strdergge bari
Joeet WNel
Agp
(6xb) Expr) (Med RiskeDafe)
(sleantaee Earr
(bady: (bledetafo Kistetidee)
lett (bew) (sactanne so0s: chpp Fare) (sstie: Foom)
[Ex0) Eapr) Owebbp test)
(P2) (hmm) Espalaann: Nenel (1o Netl Cotract : Expr]
scett (Kotta)
(eeg) Etor)
ABMI Eq Lenecaoe)
ceeei Nar3
Figure 2: Expression tree representation in Lean4. The diagram shows the translation of a mathematical expression into the corresponding Lean4 expression and its representation an expression tree. The definition of Expr Lean4, as shown the bottom left corner, includes constructors like bvar, fvar, lam, and app.
as Coq and Isabelle, provided that these systems can export or reconstruct similar expression tree structure.
Expression to Tree for premise selection in Lean4
3.1 Expressions to Trees with CSE
In the simplification of expression trees, crucial task is the elimination of common subexpressions. The CSE algorithm helps
to reduce redundancy in an expression by ensuring that each subexpression is evalu- ated only once. The process can be bro- ken down into several steps that systemat- ically identify and replace repeated subex- pressions. A simple example is presented in Figure 3
Ohgggroseet Loast
121 txpeance ne
bige the tae
Figure 3: Applying CSE to an expression tree
Next, we provide rigorous and formal explanation of the CSE algorithm adopted for Lean4's Expr structure. This algorithm primarily comprises the following three sequential stages, aimed at standardizing and simplifying the expression tree structure by replacing repeated subexpressions. We use symbolic functions C,C, R and auxiliary data structures to describe these stages and their interactions.
1. Processing de-Bruijn Indices (D). This stage, performed by function D, recursively traverses the expression tree to standardize the representation of bound variables (bvar), ensuring it is unaffected by local binder names for facilitating subsequent subexpression comparison. The output is the expression tree e' (ee with standardized de-Bruijn indices.
Counting Subexpression Occurrences (C). The objective of this stage operates on the output e' from the first stage. Function C traverses the tree, computes the structural hash value for each subexpression, and uses a global dictionary M to record its frequency of appearance, thereby identifying repeated subexpressions. The output is the dictionary M containing subexpression occurrence counts.
3. Replacing Repeated Subexpressions (R). This stage receives the standardized expression tree e' and the frequency dictionary M. Function R recursively traverses e', replacing subexpressions whose hash values appear more than once (excluding constants) with newly introduced free variables (fvar). Internal mapping V and set S are used for variable management. The output the CSE-simplifid expression tree.

---

The entire CSE algorithm cse(e) can be understood as the original expression e undergoing the se- quential processing of the three stages described above: cse(e) = (D((e, . after C, Vinit: Siaa) In this formula, (e, 2) is the output of the first stage, Mfnmll a is the frequency dictionary pop- ulated after running the second stage C on ((e, 2(), while Vinit. Smit are the initial empty map and set at the beginning of the third stage. After being processed by CSE, the original expression is transformed into an expression tree with a more compact and less redundant structure, where common subexpressions are replaced by unified variable references. This standardized representation significantly increases the efficiency of processing and analyzing expressions in Lean4 theorem proving tasks, providing optimized input for subsequent structural similarity caleulations and premise selection procedures.
3.2 The WL Kernel Method for Encoding
The WL kernel a graph kernel method used to measure structural similarity between graphs[45) iteratively aggregates node neighborhood information to generate graph representations, effectively capturing graph topological features. The WL kernel has been proven to be highly capable of distinguishing non-isomorphic graphs. Given expression tree T (V, E), where V is the set of nodes and is the set of edges, the WL kernel method encodes the tree through the following iterative process.
1. Initialization:
Assign each node e V an initial label ( typically based on its node type (e.g.. variable, constant, or function symbol).
2. Iteration: For each iteration i = NN (N is the predefined number of iterations):
For each node collect the multiset of current labels from its neighbor set N(v), (((-1) N(v)}.
Combine the node's current label (((-1) with the multiset of its neighbors' labels to form string, for example, ((t))) ( (((=))
(i-1) for u N (v)).
Use a deterministic hash or compression function to map this combined string to a new, unique label (())) Update the node's label to (()))
In each iteration, record the set of new labels for all nodes.
3. Feature Vector: After N iterations, compute feature vector for tree T by counting the frequency of all labels that appeared across all iterations.
The WL kernel is closely related message-passinng neural network (MPNN) mechanisms 23 and its Ist-order test (1-WL) has been proven to be highly capable of distinguishing graph structures [4). This powerful structural discriminative capability makes the WL. kernel particularly suitable for encoding Lean4 expression trees, which have complex and unique structures, effectively capturing local structural patterns and generating discriminative vector representations. The WL kernel value is defined as the inner product of two graphs' feature vectors kwr. (Ti, T2) (o(Ti). ). o(T2)) and similarity based on feature vectors (such as cosine similarity) can quantify structural similarity be- tween trees. In the premise selection method proposed in this paper, we utilize the WL kernel method to encode CSE-simplified expression trees. These feature vectors are used in the initial screening phase to compute and rank the structural similarity between the query and library theorems, selecting a Top-A candidate set, thus efficiently leveraging structural information in the preliminary stage.
3.3 Tree Edit Distance Similarity
TED is a common measure for structural similarity between ordered labeled trees, defined as the minimum total weighted cost required to transform one tree into another using insertion, deletion, and substitution operations [47]. Computing ordered tree TED is classic problem, often solved by dynamic programming algorithms. The zss algorithm 48 is classic method with time complexity of O(T,, x [Ty) x min( depth(T;) (T;). leaves(Ti) x min depth(T2)) lea,teeTT) leaves(Tz)) and space complexity O(Ti [T&),, theoretically efficient and supporting parallelization.
In our application to Lean4 expression trees, editing operation costs Cn (substitution). On (deletion), C₁ (insertion) are finely tuned based on Lean characteristics. Specifically, costs are set as follows. Define set of node label prefixes with smaller change costs P (BVar, FVar, MVar, Sort, Const). For node substitution CR, the cost is 0 if the two nodes are identical or if the label of either node starts
5

---

with any string in P; otherwise, the cost is the preset value CR. For node insertion (C1) or deletion (Cp), if the involved node's label starts with any string in P. the cost is oC, or oCD. respectively, where a [0. 1] is scaling parameter for simple node operations: otherwise, the cost is the preset value (C₁ or CD). This tiered cost structure reflects the differing impacts of operations on expression structure and logical core. Operations on simple nodes representing variables, types, or constants (low cost) typically have less impact on overall mathematical meaning compared to modifications of complex expression structures (high cost). By defining cost functions adapted to the semantics and structural characteristics of Lean4 expressions, TED can more precisely capture subtle and logically relevant structural differences between trees. Based on the TED d T2), the normalized similarity tree edit distance similarity (TEDS) s (Ti, T2) is defined as:
d(Ti.T) C. max (1T1), (Te)
s (T),TT) = 1-
where [2] is the node count, and C' = max CR. CD. CT) is the normalization factor ensuring e [0. 1]. In the premise selection method proposed in this paper. TEDS serves as the fine-grained metric in the second stage, applied to CSE-simplified expression trees. After WL kernel method preliminarily screens Top-k candidates, TEDS scores are computed against the target tree for re-ranking. TED's fine fine-grained comparison aids more accurate relevance assessment, optimizing final premise selection.
4 Tree-Based Premise Selection
4.1 Core Tree-Based Selection with Multi-Stage Filtering
The core premise selection mechanism proposed in this paper employs two-stage filtering pipeline designed for efficient retrieval of the most relevant theorems from a large theorem library, balancing computational efficiency and retrieval accuracy. The inputs are the target expression tree T query and the premise theorem database SCSE, where each theorem is preprocessed via CSE and represented as an expression tree.
Stage I: Coarse Filtering via WL Kernel
The objective of this stage rapidly reduce the search space. We first encode the target expression tree Tquery and all theorem trees T; E Sese using the Weisfeiler-Lehman (WL) kernel method (with iterations, see Appendix B). generating feature vectors @wr. e N that reflect the tree's 's structural features. Subsequently, we compute the cosine similarity between the WI. feature vector of the target expression tree @ww (Tquery) and the feature vector Φww (T;) of each theorem tree 7; in the database:
simeus (Tquery: T:) [@we(TTamn (ww((:)]] Based on the cosine similarity scores, we rank the theorems
dwn (dw (TT,)(T;))
in the database and select the top theorems as the coarse candidate set Ceuase = (Ti, -..,,-.. T&}- The parameter k is a tunable threshold balancing recall and the computational overhead of subsequent refined filtering. To adapt to target expressions of varying complexity, the value of ls can be adjusted adaptively based on the number of nodes (Tquery in T Tuwery: k= min (Kmax 8- B-ITquer)) (Tquery). where kmux. is the upper bound for k and |3 is a scaling factor used to determine the initial number of candidates based on the target tree size.
Stage 2: Refined Filtering via TEDS
This stage aims to perform more precise structural similarity assessment the coarse candidate set Coearse- For each theorem tree T, E Ceoarse in the candidate set, we compute the normalized TEDS score between it and the target expression tree Tquary, as shown in Eq. [ simrEDs (Tquery. T2) d(Tavoy))))
1 @
The final similarity score for the core method combines the results from both stages, using weighted sum to calculate the hybrid similarity: simmybridTquery TT) a cos (T query: T2) (1- a:) (Tornasssqurrr T,), where a é [O, 1] is a weight parameter controlling the relative importance of WL cosine similarity and TEDS in the final score. The coarse candidate set Crearse is re-ranked based on the hybrid similarity simnghrid. and the top theorems are selected as the final premise selection result for the core method, to be used for subsequent tactic application or proof search.

---

4.2 Enhanced Selection via Clustering and Multi-Strategy Expansion
Building upon the core two-stage filtering pipeline proposed in Section 4.1, this subsection introduces several enhanced mechanisms to further improve the efficiency, accuracy, and flexibility of premise selection. These enhanced mechanisms include cluster-based search space compatibility constraint filtering, additional structural simplification, collapse-match similarity, Jaccard similarity of Const nodes and an adaptive similarity metric fusion strategy, collectively forming more powerful premise selection framework.
optimizatiiiii optimization, structural
Cluster-Based Search Space Optimization. To accelerate the initial screening process for large premise theorem database ScSE. we employ cluster-based search space optimization techniques. The core idea is to group theorems based on their structural features (encoded via the WL kernel method and converted into vector representations, typically after dimensionality reduction), thereby restricting the search scope during online retrieval within the cluster(s) most relevant to the query expression T Tquery significantly reducing computational overhead. This mechanism comprises an offline phase, where library theorem vectors are clustered into K groups and centroids are computed; and an online phase, where the query expression vector's s similarity to each cluster centroid is computed to select relevant clusters for restricting the Stage 1 search. For dynamically updated theorem libraries, maintenance mechanisms (such as incremental updates or periodic re-clustering) should be considered to ensure the effectiveness of the clustering structure. Appendix C show the detail.
Structural Compatibility Constraint Filtering. Before performing detailed structural similarity calculations, we introduce structural compatibility constraints based on the node count [T] pre- liminarily filter candidate theorems, aiming to exclude theorems differing significantly in size from the target expression tree Tquery. thereby improving efficiency and reducing false positives. Only theorems satisfying the following set of size constraints Cvalia proceed to the next stage of detailed {T' c1 ququry) S [2'| s 02) query)) n [11|//11 /Zqueryl s A }.J.hreee C1 < 1 < 02
comparison: Cvalid
Absolute Size Constraint are constants defining relative node count boundaries, and A specifies the maximum allowed absolute difference in node count. Only theorems belonging to Cvalid proceed to the detailed comparison stage.
Relative Size Constraint
Additional Structural Simplification. Given the sensitivity of TED structural details, we apply an additional structural simplification step to expression trees before computing the TEDS. This step aims to remove redundant binding structures that are structurally similar but differ little in their logical core, particularly bindings involving simple types such as BVar, FVar, MVar, Sort, Const. Specifically, this process recursively traverses the Cim-siipliiiedd expression tree. For a ForallE node, if its binderType belongs to these simple types, the node is replaced with its body, and this simplification iterates until the tree structure no longer changes. This additional simplification helps to reduce TEDS's s sensitivity to these secondary structural changes, allowing the computed TEDS to better reflect the similarity of the expression's core logical structure.
Coltapse-Match (CM) Similarity. (im Tb) is a structural similarity metric designed to measure the degree to which the structure of the souree tree Ta. after simplification according to specific collapse rules, aligns with the target structure Tg Its computation method involves calculating a raw match score for T₂ aligning with T, through recursive process and normalizing this score by dividing by the total number of nodes [To] in the target tree T,, yielding a score between 0 and 1. This metric is particularly suitable for evaluating whether premise structure can match a segment of the proof goal structure by applying specific proof rules or tactics. See Appendix for the details.
Jaccard Similarity of Const nodes. sim (Ta, Tb) measures the semantic overlap between two expression trees T, and Tb, specifically based on the sets of declNames of their Const nodes. The computation involves collecting all unique declNames Const nodes in T2 and To to form sets S. and S,, respectively. and then computing the sizes of their intersection and union. It is defined as: simjaccard (Ta, Ta. Tb) [SanSs]
[ When the union is empty, the similarity is 1 if Sa, Sb are both empty, otherwise O. The details are provided in Appendix [
Adaptive Similarity Metric Fusion. We generalize the similarity fusion strategy from the core method, employing more flexible parametric approach that considers multiple similarity metrics. The final method fuses four structural and semantic similarity metrics introduced in the preceding text. The final enhanced similarity score simeshanced is computed via the following weighted sum:
simenhancd Q simeos + B- siMTEDS + 7 simJaccard ô simCM.
(2)
7

---

where 9, 8 are weight parameters satisfying + + 8 1, dynamically adjusted based on the characteristics of the target expression and candidate theorems to optimize retrieval performance. Through this adaptive fusion, we can dynamically adjust the importance of different similarity metrics, achieving more precise premise selection based on target expression and candidate theorem character- istics. Overall, our method employs two-stage strategy: Stage performs rapid coarse screening by combining tree node count, collapse-match based structural alignment similarity, and computationally efficient WL cosine similarity; Stage 2 then utilizes this comprehensive adaptive fused similarity for refined ranking of the preliminary results to obtain the final premise recommendations.
Numerical Experiments
5.1 Dataset Preparation
The theorem library is constructed by extracting 217,555 valid mathematical theorems from Lean4's Mathlib4 version 14.18.0-rc1. The structural characteristics and domain distribution of the theorem library are evaluated by statistical analysis, with results visualized and detailed complexity and domain statistics provided in Appendix Each theorem tree in the CSE-preprocessed database is encoded using the WL kernel method with iteration count k, and the encodings are stored in the database. We construct two test sets for the evaluation of the method. The test set A consists of 100 small-scale problems, categorized into substitution-type condition -wappipgg traipppiggttpp,,,,.. and mixed -tppe, aimed at assessing the method's ability recognize structural similarities, adapt premise reordering, and handle combined transformations. The test set consists of m = 61 19 (state, theorem) pairs extracted from the Lean proof environment, where each pair transforms the proof state prior the application of the theorem into a problem statement. See Appendix A for the test set details.
5.2 Theorem/Lemmi Retrieval Experiments
We compare our method with existing Lean premise retrieval tools, including Lean Search [19]. Moogle [17), Lean Explore [8] and Lean State Search ([5), as baseline methods. The experiments carried out local machine (Macbook Pro) equipped with Apple M3 Pro chip (11 cores). The objective is to compare the retrieval performance of the proposed method with the baseline methods in test sets A and B. Performance is evaluated using common Top-k retrieval metrics: Top-k Recall, Top-k Precision, Top-k F1-score, Top-k nDCG, and Mean Reciprocal Rank. We present in Appendix F examples where query expressions and their corresponding matched theorems
depicted tree structures. For these experiments, the weights were set to (a, 7, = (0.1, 0.3, 0.5), and 0.2. C₁ Cn 1 and CR 0.4, with low-cost scaling factor of
the TED costs The performance metrics for test sets A and B are summarized in Table | Experimental results demonstrate that the proposed tree-based method achieves retrieval performance significantly superior to existing baseline tools on both test sets. This is particularly evident on the large test set B, validating the effectiveness of our structured approach for handling complex mathematical expressions. Table 2 and further presents Recall @ performance on Test Set B, stratified by mathematical domain and complexity (node count: simple < 50, medium 50-200, complex 200). Analysis indicates that retrieval performance varies significantly across different domains and generally decreases with increasing problem complexity.
Table Performance (%) on test sets
Recall@k
Precision@1.
Fl Fl-ssmee@k
nDOG@1
Test
Method
@1
@5
@ @00
@1
@5
@00
@1
@5
@ 10
@
@5
@
Lean Search
1.0
3.0
5.0
1.0
0.6
0.5
1.0
1.0
0.9
1.0
2.1
2.7
2.0
Mongle
7.0
3.7
Lean Search (Augument)
1.0
4.0
8.0
1.0
0.8
0.8
1.0
1.3
1.5
1.0
2.5
3.7
2.7
Lean Explore
5.0
Lean State Search
45.0
83.0
85.0
45.0
16.6
8.5
45.0
27.7
15.5
45.0
65.3
66.0
60.2
Tree-hused Search
28.0
Lean Scarch
7.2
15.2
18.0
7.2
1.8
7.2
5.1
3.3
11.4
12.3
Moogle
4.8
10.9
13.6
4.8
2.2
1.4
4.8
3.6
2.5
4.8
8.0
8.8
7.5
(Augument)
6.6
Lean Explore
1.0
7.7
13.0
1.0
1.5
1.3
1.0
2.6
2.4
1.0
4.3
6.0
4.4
Search
2.2
5.9
Tree-bused Search
25.8
28.0
28.7
25.8
5.6
2.9
25.8
9.4
5.2
25.8
27.0
27.2
26.9
8

---

Table 2: Domain-Complexity Cross-Performance (%)
Table 3: Domain-Complextt Cross-Performance
Domain
Complexity
Count
Recall
Domain
Complexity
Count
Recall @*
@1
@
@
@0
@
@
@
10
Simple Medium
47
4.3
4.3
Simple Medium
136
7.4
7,4
7,4
Algehra
346
1.7
2.3
2.6
Order Theory
351
4.8
5.4
5,4
Complex
240
0.0
0.4
0.4
Complex
238
1.3
2.1
2.1
Simple
75
68.0
81.3
82.7
Simple Medium
34
52.9
55.9
58.8
Natural Number
Medium
126
38.9
42.1
44.4
Theory
31
35.5
38.7
38.7
Complex
21
23.8
38.1
38.1
Complex
0.0
0.0
0.0
Simple
22
36.4
40.9
40.9
Simple Medium
577
17.5
21.3
21.5
Logic
Medium
22
22.7
22.7
Others
2976
41.0
43,3
44.3
Complex
24
20.8
20.8
20.8
Complex
762
9.2
11.5
12.1
Table Framework hyperparameters and their roles.
Parameter
Stage
Description
h
WL Kernel
Iteration count for neighborhood aggregation
Weight parameters for cosine, TEDS, Jaccard, and Collapse-
a, a,9,Y,
Adaptive Fusion
Match similarities
TEDS Operation Costs
Low-cost scaling factor for simple node operations
5.3 Ablation Study
Hyperparameters and Their Impact. We introduce several key hyperparameters that govern the premise selection process. Table summarizes these hyperparameters and their roles.
WL Kernel Iteration Count (h): The number of iterations in the Weisfeiler- Weisann kernel determines the depth of neighborhood aggregation. Larger h captures more global structural features but increases computation and may cause oversmoothing. We select h to balance efficiency with structural expressiveness.
Adaptive Fusion Weight Parameters (ax, (e,3,, 3, 5): These parameters control the relative contributions of cosine similarity,
edit distance similarity, Jaccard similarity, and Collapse- Match similarity. They satisfy a + 3 + 8 = 1 and are dynamically adjusted to optimize retrieval performance. Low-Cost Scaling Factor (a)): TEDS computation, operations on simple nodes (e.g., BVar, FVar, MVar, Sort, Const) are scaled by a e [0, 1].
Similarity Metric Contribution Analysis. We remove a single similarity metric time from the full fusion model, which includes all four similarities (WL cosine, TEDS, Const Jaccard, and CM), and compare their retrieval performance (Top-k Recall) on the test set comprising 299 natural number problems. Results show that removing any single similarity metric impacts performance. Notably, removing Const node Jaceard similarity leads the most significant performance drop, underscoring its critical contribution via semantic overlap measurement, indicating that semantic information remains vital in a structured approach. The main results are summarized in Table
Parameter Sensitivity Experiments. We primarily examine the WL iteration count and the weights o, 3, 7.0 used for adaptive similarity fusion (as in Eq. 2 We evaluate the impact of the WI. iteration count on the performance of the preliminary screening stage (Top-k Recall) and the filtering time per query. Experiments on the test comprising 200 natural number problems indicate that increasing the number of WL iterations improves Recall, but simultancously significantly increases the filtering time per query. Results reveal trade-off between accuracy and efficiency, with Recall improvements tending to plateau after a certain number of iterations. Performance and time results for different iteration counts are shown in Table g We also examine the impact of the weights a, r, 8 on the final screening stage performance (Top-k Recall). Analysis on the test set comprising 100 natural number problems indicates that different weight configurations impact retrieval performance. Results show that optimizing weight settings can yield further improvements Top-k Recall compared to equal weights, confirming the importance of weight tuning for enhancing fusion effectiveness. Experimental results are shown in Table

---

Table Impact of
In addition, we conducted a new experiment specifically analyzing the impact of a on retrieval performance. This parameter con- trols the scaling of node edit costs in Tree Edit Distance (TED), influencing both precision and efficiency. The results, shown Table 5) indicate that 0.2 yields the best performance, with optimal Recall @@k. k. Lower values decrease recall, while higher values significantly reduce it. This highlights the importance of moderate penalty for simple node edits, enabling TED to better capture structural differences in Lean4 expressions.
@
Value
@
@
10
0.0
62
67
0.2
67
69
0.4
63
69
0.6
65
69
0.8
61
62
1.0
59
62
Table Accuracy comparison (%)
Table Impact of weights on performance (%
Recall @k
Weights
Recall
Configuration
@5
@
10
B
@
@
0.25
0.25
0.25
0.25
63
Full Model
42.8
51.1
52.5
0.20
0.20
0.10
64
Without WL
44.5
50.5
51.8
0.20
0.50
0.20
0.10
59
65
68
Without TEDS
44.5
50.5
51.8
0.20
0.20
0.50
0.10
57
63
69
Without Jaceard
37.1
42.8
44.2
0.10
0,20
0.20
0.50
58
65
68
Without CM
38.2
49.3
52.4
0.30
0.30
0.20
0.20
59
63
67
0.20
0.20
0.30
0.30
59
64
68
0.15
0.40
0.30
0.15
67
Table 8: WL Iterations vs. Screening accuracy (%. Wi.,othuut TEDS
3.3
and filtering time
Recall @@k
Iterations
Time (s)
@ 100
@500
@ 1000
@ 3000
@ 5000
54.0
66.5
71.5
77.5
81.0
20.70
55.5
67.0
73.5
80.0
81.5
27.55
57.0
68.0
73.0
79.5
82.0
32.92
10
55.5
65.5
70.5
78.5
83.0
47.89
20
55.5
66.0
70.5
78.5
82.5
55.37
40
56.0
65.5
70.5
78.5
83.0
54.79
Conclusion
We address the challenge of premise selection in interactive theorem proving systems with large theorem libraries by proposing a novel tree-based method that explicitly leverages the structural in- formation of Lean expressions. Our approach integrates multi-stage filtering, clustering optimization, structural constraints, and adaptive similarity fusion, significantly improving retrieval accuracy. Ex- periments the Mathlib4 library show that method outperforms existing baselines across various Top-k retrieval metrics, demonstrating its superiority for large-scale formal libraries. Furthermore, the framework is designed to be language-lean. offering the potential for efficient adaptation to other proof assistants with minimal changes. The inclusion of advanced graph representation techniques and further investigation into Lean expression information are promising directions for future work. Expanding the scale of theorem libraries (e.g., including Optlib), along with tighter integration with automated proof search LLM proof generation, could provide further advancements end-to-end proof automation.
Acknowledgements
This research was supported in part by the National Key Research and Development Program of China (2024YFA 101 1012903), the National Natural Science Foundation of China (12331010 and 2288101), and the Guangdong Provincial Key Laboratory of Mathematical Foundations for Artificial Intelligence (2023B 1 20000001).
10

---

References
[I] Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: new frontier in Al. arXiv preprint WrXi:22412.16075, 2024.
[2] Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey deep learning for theorem proving, arXiv preprint arXiv:2404.09993 2024.
[3] Daniel Kühhwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings 6, pages 378-392. Springer, 2012.
[4] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with etrreval-auggmene language models. 2023.
[5] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, ShanCChrittophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq Proof Assistant Reference Manual. INRIA, 1999.
[6] Lawrence C Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
[7] John Harrison. HOL Light: A Tutorial Introduction. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 1996.
[8] Norman Megill and David A Wheeler. Metamath: Computer Language for Mathematical Proofs. Lulu Press, 2019.
[9] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). 2015.
[10] Leonardo de Moura and Sebastian Ullrich. The Lean theorem prover and programming language. 2021.
[11] The mathlib community. The Lean mathematical library. 2020.
[12] Chenyi Li, Zichen Wang, Yifan Bai, Yunxi Duan, Yuqing Gao, Pengfei Hao, and Zaiwen Wen. Formalization of algorithms for optimization with block structures, 2025. URL https /arxiv.org/abs/5503. 18806)
[13] Chenyi Li, Shengyang Xu, Chumin Sun, Li Zhou, and Zaiwen Wen. Formalization of optimality conditions for smooth constrained optimization problems, 2025. URL https::/arxii.orgg//
2503. 1882.18821
[14] Chenyi Li, Ziyu Wang, Wanyi He, Yuxuan Wu, Shengyang Xu, and Zaiwen Wen. Formalization of complexity analysis of the first-order algorithms for convex optimization, 2024. URL
https:/aardv.or///b//40......1 14377
[15] Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. Assisting mathematical formal- ization with learning-based premise retriever, 2025. URL httpss//aarrw.orrga/b25555..13.0
[16] Joachim Breitner. Loogle!, 2024. URL https:://ooolee.cau lang.org
[17] Morph Labs. Moogle: Semantic search over mathlib4, https://www.moogle.al 2023.
[18] Justin Asher. Lean Explore. https:/www.lcneexpprr.ccm 2025.
[19] Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. semantic search engine for mathlib4, arXiv preprint 1333 2024.

---

[20] Kai Sheng Tai, Richard Socher, and Christopher D Manning, Improved Semantic Represen- tations From Pree-Structure Long Short-Term Memory Networks. In Proceedings of the Annual Meeting of the Association for Computational Linguistics and the International Joint Conference on Natural Language Processing, 2015.
[21] David K Duvenaud, Dougal Maclaurin, Jorge Iparraguirre, Rafael Bombarell, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P Adams. Convolutional Networks Graphs for Learning Molecular Fingerprints. In Proceedings of the International Conference on Neural Information Processing Systems, 2015.
[22] Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Lio, and Yoshua Bengio. Graph Attention Networks. In Proceedings of the International Conference on Learning Representations, 2018
[23] Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How Powerful are Graph Neural Networks? In Proceedings of the International Conference on Learning Representations, 2019.
[24] Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A machine learning dataset for higher-order logic theorem proving. arXiv preprint arXiv: 1703.0042, 2017.
[25] Kebin Peng and Dianfu Ma. Tree-structure enn for automated theorem proving. In Neural Information Processing: 24th International Conference, ICONIP 2017, Guangzhou, China, November 14-18, 2017, Proceedings, Part 24, pages 3-12. Springer, 2017.
[26] Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. Advances in neural information processing systems, 30, 2017.
[27] Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment?, 2018. URL https://aaraw.agg/b/////2233333
[28] Miroslav Olšák, Cezary Kaliszyk, and Josef Urban. Property Invariant Embedding for Au- tomated Reasoning. In Proceedings of the European Conference on Artificial Intelligence, 2019.
[29] Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 2967-2974, 2020.
[30] Zarathustra Goertzel and Josef Urban. Usefulness of lemmas via graph neural networks. In URL http://aiit--coffereneee /abbtrrc/astt 2_11222111_0 2019__appe_322 pdf. 2019.
[31] Maxwell Crouse, Ibrahim Abdelaziz, Cristina Corelio, Veronika Thost, Lingfei Wu, Kenneth Forbus, and Achille Fokoue. Improving graph neural network representations of logical formulae with subgraph pooling. arXiv preprint arXiv: 1911199199900 2019.
[32] Michael Rawson and Giles Reger. Directed Graph Networks for Logical Reasoning (Extended Abstract). In Joint Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR) and the Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020.
[33] Qinghua Liu, Yang Xu, and Xingxing He. Attention Recurrent Cross-Graph Neural Network for Selecting Premises. International Journal of Machine Learning and Cybernetics, 2022.
[34] Zarathustra A Goertzel, Jan Jakubüv, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock. and Josef Urban. The Isabelle ENIGMA. In Proceedings of the International Conference on Interactive Theorem Proving. 2022.
[35] Edvard K Holden and Konstantin Korovin. Graph Sequence Learning for Premise Selection. In Proceedings of the Conference on Artificial Intelligence and Theorem Proving, 2023.
[36] Jan Jakubūv, Karel Chvalovský, Zarathustra A Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In Proceedings of the International Conference on Interactive Theorem Proving, 2023.
12

---

[37] Aaron van den Oord, Yazhe Li, and Oriol Vinyals. Representation Learning with Contrastive Predictive Coding. arXiv preprint vxXiv:880.003748 2018.
[38] Ting Chen, Simon Kornblith, Mohammad Norouzi, and Geoffrey Hinton. A Simple Frame- work for Contrastive Learning of Visual Representations. In Proceedings of the International Conference on Machine Learning, 2020.
[39] Zhaoyu Li, Binghong Chen, and Xujie Si. Graph Contrastive Pre-Training for Effective Theorem Reasoning. International Conference Machine Learning Workshop Self-Supervised Learning for Reasoning and Perception, 2021.
[40] Qika Lin, Jun Liu, Lingling Zhang, Yudai Pan, Xin Hu, Fangzhi Xu, and Hongwei Zeng. Contrastive Graph Representations for Logical Formulas Embedding. IEEE Transactions on Knowledge and Data Engineering, 2021.
[41] Deborah Ferreira and André Freitas. Premise Selection in Natural Language Mathematical Texts. Proceedings of the Annual Meeting of the Association for Computational Linguistics, 2020.
[42] Andrej Bauer, Matej Petković, and Ljupco Todorovski. MLFMF: Data Sets for Machine Learning for Mathematical Formalization. Proceedings of the International Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023.
[43] Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher-order theorem proving (extended version). arXiv preprint arXiv:1904.000 03241, 2019.
[44] Mare Brockschmidt. Gnn-film: Graph neural networks with feature-wise linear modulation. In International Conference Machine Learning, pages 1 1144-1152. PMLR, 2020.
[45] Nino Shervashidze, Pascal Schweitzer, Erik Jan Van Leeuwen, Kurt Mehlhorn, and Karsten M Borgwardt. Weisfeiler-lemman graph kernels. Journal of Machine Learning Research, 12(9), 2011.
[46] László Babai, Paul Erdos, and Stanley M Selkow. Random graph isomorphism. SlaM Journal on computing, 9(3):628-66 635, 1980.
[47] Philip Bille. A survey on tree edit distance and related problems. Theoretical computer science, 337(1-3):117-33) 2005.
[48] Kaizhong Zhang and Dennis Shasha. Simple fast algorithms for the editing distance between trees and related problems. SIAM journal on computing, (866):245511 1262, 1989.
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The abstract and introduction accurately summarize the key contributions and the scope of the work presented in the paper.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
We discuss the limitations of approach in Appendix G
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
14

---

Justification:
This paper does not include theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated referenced in the statement of any theorems.
The proof' can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: We provide detailed descriptions of the experimental setup including dataset, model architecture, and parameters- Section 3 and Appendices A
D
and B to
ensure reproducibility.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that appropriate to the research performed.
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
15

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification: We provide open access to our code and data and detailed instructions for reproduction in the supplemental material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (httpss/nniss.c/ppbbicc
guidessCoodSubbissioooooeyyyy for more details.
While encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to to reproduce the results. See the NeurIPS code and data submission guidelines (https: for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Question:
Answer: [Yes]
Justification: All essential experimental details, including data, parameters, and methods, are provided in Section 3 and Section 4
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: We report Top-k Recall (Recall @ k), Top-k Precision (Precision @k), Top-k Fl-score (Fl-score @k), Top-k nDCG (nDCG@k) and Mean Reciprocal Rank (MRR) for our main experimental results to indicate statistical significance, as shown in Table |
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emoor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
16

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
If error bars reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: Details regarding the compute resources used for experiments, including hardware specifications are provided in Section 5.2
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental rums as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't fidn't make it into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics http:://ccurisssccpupbii/hheeeee
Answer: [Yes]
Justification: We have reviewed the NeurIPS Code of Ethics and confirm that research adheres to all guidelines and principles.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: We discuss potential positive and negative socictal impacts of our work the dedicated Broader Impacts Appendix
Guidelines:
17

---

The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negatíve societal impacts include potential malicious or unintended uses (e.g.. disinformation, generating fake profiles, surveillance), fairness considerations (c.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of MI.).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our work does not involve the release of data or models identified as having a high risk for misuse.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: All existing assets used in this work are properly credited, and their licenses and terms of use are respected and documented.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
18

---

For scraped data from a particular source (e.g., website). the copyright and terms of service of that souree should be provided.
assets are released, the license, copyright information, and terms of use the package should be provided. For popular datasets, paperswithcode. wtw.tthoo.e..o/attseeeeeeeeeeeee has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors encouraged to reach out to the asset's 's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: New assets introduced are well-documented, and documentation will be provided alongside the assets upon release.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question:
For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: This paper does not involve crowdsourcing or research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
This paper does not involve research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
19

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if' applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Question:
Answer: [NA]
Justification: Large Language Models were not used as an important, original, or non- standard component of the core methods in this research.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to our LLM policy http:://leeiinsssccoooccreeeeess for what should or should not be described.
20

---

A Data Extraction and Theorem Library Construction
The theorem library used this study sourced from Lean4's Mathlib4 version v4. 18.00l.. initial extraction yields 339,746 theorems. To construct high-quality, non-redundant theorem library suitable for the premise selection task, we apply a series of filtering rules to remove theorems that do not meet the requirements, such internal implementation details, auxiliary lemmas, and theorems from specific namespaces. These filtering rules include excluding theorems from Lean, Std, Mathlib Tactic namespaces those whose names contain patterns like .rrof -- auxLemma.. Lemmas or pprivate.. After this filtering process, the final library comprises 217,555 valid mathematical theorems. Each theorem in the library is parsed and converted into expression tree structure, and stored in a database with key fields including id (unique identifier), name (theorem name), stwtement_sseeeeeeee str (formalized statement Lean4's s underlying level), expr_json (raw pression tree JSON), _sepr_ce____assee nodes). To assess data quality and understand the characteristics of the theorem library, we conduct statistical analysis on the final set of theorems, focusing on the node count and depth distributions of the theorem expression trees. The node count distribution histogram is shown in Figure 4 and the depth distribution histogram is shown in Figure [ Statistics on the distribution and structural characteristics of the theorem library across different mathematical domains are detailed in Table
(CSFE-pocessed tree JSON), and node_ _ouutt (number of
Node Count Distribution
Statistics
1000
Avg frequency: 295.9
Frequency
Max frequency: 4,314
1000
Min frequency:
Most frequent node count: 49
2000
Max node count: 1849
150
210
1050
1200
1sse
1650
1860
Node Count Value
Figure 4: Node Count Distribution Histogram
Expression Tree Depth Distribution
14000
Statistics
12000
Avg frequency: 1919.3
Frequency
Max frequency: 14,292
Min frequency: 1
Most frequent depth: 13
Weighted avg depth: 17.16
1000
2000
Tree Depth
Figure Depth Distribution Histogram
21

---

Table Mathematical Domain Analysis (partial) in mathlib
Node Count
Depth
Domain
Count
Features
Max
Min
Median
Max
Min
Median
Algebra
11718
1325
5
95.0
130
2
17.0
Polynomial/Ring
Analysis
8689
1147
125
78
2
20
Convew/mnerPrrodneeSper
Geometry
1595
973
11
165
4
Euclidean/Mamifldd
Topology
5720
819
5
75.0
72
2
16.0
BornologyUnnformmpan
NumberTheory
2551
986
3
855
59
I
15
Clas.Number/Harrmont
Category Theory
5570
1077
5
113.0
84
2
20.0
Adjunction/Functton
Logic
535
707
3
51
35
1
13
Eimbedding/Demmmeabbl
B WL Kernel Encoding Process
This section describes the WL kernel method used for encoding expression trees in this paper. The WL kemel is an effective technique for extracting graph structural features, generating compact vector representations that capture the tree's structural properties by iteratively aggregating neighborhood information of nodes. The encoding process can be broken down into the following steps:
1. Label Initialization (initialize) ie_beellel Initial labels are assigned to each node in the expression tree. The initial label based on the node's original type; for specific types like BVar, FVar, MVar, Sort, Const, the label is simplified to the type prefix. Furthermore, each node's label combined with its depth information the tree.
2. Iterative Label Refinement (s1_ (=l_iterad itteraiion:: h iterations are performed. In each iteration, node's label is updated based on its label from the previous round and the labels of all its children from the previous round via hashing function. Specifically, the children's 's previous labels are collected, sorted lexicographically, concatenated with the current node's 's previous label to form string, and finally, the MD5 hash of this string is computed as the node's 's new label for the current round.
3. Generate Label Histogram (get_label) [get_Labe__histogram)) After each iteration, the distribution of all nodes' new labels for the current round is counted to generate label histogram.
4. Combine Histograms (compute_ w1 wl__ncoding): The final tree encoding is generated by com- bining the label histograms from all iterations. To distinguish identical labels originating from different iteration rounds, each histogram's 's labels are prefixed with the corresponding iteration number. The number of iterations h is determined based on the tree's ' depth and a preset maximum number of iterations, taking the minimum of the two. These combined label counts form the final feature vector used to represent the expression tree.
Through this iterative aggregation process, the WL kernel method is able to capture information about different structural patterns within the expression tree and encode it into fixed-dimensional feature vector, facilitating subsequent similarity calculations.
C Clustering Process
This section describes the process of clustering the WL-encoded theorem vectors. The core objective of clustering is to group theorems with similar structural features to accelerate the preliminary screening speed during subsequent theorem search. We first read the pre-processed theorem trees from the database. These trees are transformed into more canonical and compact form by applying structural simplification techniques, such as common subexpression elimination (CSE). Subsequently, we apply the Weisfeiler-Lehmen (WL) algorithm to encode these simplified trees. These encodings are converted into high-dimensional numerical vectors using bag-of-features approach, where features correspond to the structural patterns extracted during the WL encoding process. In the feature extraction stage, we select the top 8000 most frequent features as the final feature by counting feature occurrences across the entire dataset. To measure the distinctiveness of these features and reduce the influence of high-frequency generalized features, we apply an IDF-like weighting scheme to the feature counts in each vector. Considering the high dimensionality of the generated feature vectors, we use Principal Component Analysis (PCA) for dimensionality reduction to mitigate the 'curse of dimensionality' and reduce retrieval computational cost. PCA aims to find
22

---

directions of maximum variance in the data, projecting the vectors into lower-dimensional space comprising 1200 principal components, thereby removing some noise and compressing the data representation. The reduced-dimensione vectors are then clustered using the Mini-Batch K-Means algorithm, an optimized variant of the K-Means algorithm particularly suitable for handling large datasets. Clustering is configured to find 10,000 clusters, utilizing an incremental learning approach where Mini-Bater Mini-Batches of 10,000 samples are processed iteratively to update cluster centers. The algorithm converges after set number of iterations. Upon completion of training, each theorem's vector in the database assigned the cluster ID corresponding to its nearest learned cluster center, and the results stored.
The entire clustering pipeline is implemented in Python, primarily utilizing the PCA and MiniBatchKMeans modules provided by the scikit-lesn library for core computation, and psycopg2 for database interaction with the PostgreSQL. database. Table 10 presents illustrative examples of clustering results, showing theorems grouped into the same clusters due to structural or semantic similarities, such as the cluster containing Nat. add_comm which includes several theorems related to the commutative property of addition. The effectiveness and characteristics of the clustering results are further visualized Figure and Figure 7 Specifically, Figure presents the sizes the top-N largest clusters, illustrating the scale of the most populated groups. Complementing this view, Figure 7 shows the histogram of cluster sizes across various predefined bins, providing insight into the overall distribution of cluster memberships, particularly the prevalence of smaller clusters. As is common in clustering diverse datasets, the distribution reveals a substantial number small clusters, with rapid decrease in frequency for larger cluster sizes.
Table 10: Display clustering results some classical theorems
Cluster 9881
Cluster ID 9182
Cluster 6559
Nat Wattadd_ee aad__comm
Nat. Nat.add_ add_leeft_cancel
Nat. www.eeg_eer___c of cftoooo__ddeeee add____zero__eet
Nat. Nat.add_ccmm comm
Nat.add @add_le_ad___t iff _fff_
Nat Nat eq_one_ off_mul_ee___ louu___e_oee_ereee Nat regozer_ooo _ddddd_____ooooaooddaaaddddddddd _dd__e__________________________ _e_t_ee_eeer zero_left. Nat new.nneezeoode saarrroof_oll_aaa mul hea___n__eerr_rre__ AddSubgroup. Normal. Normal.conj_mee.. Filter. aiteer.mem_imee mem_inf_orf _f_igghtt Function. Function..ePerroddin www.riediit...coo.o.o...o
Nat add_ leefl_efttomm
Nat. add_ fead__eft_ccaneee cancel_iff
Nat.
st__add__t__dd_ttt _if___f________ _fddifffflfftt_ __let ringhtii
Nat.min_coom mrc.minn_comm
Nat.min comm
Nat.xor_ jat.xtt_right
ast.mul_left_co
BitWec.neg_inj
Bool polloor_eft__co
BitVec.
srcVec.neg_mu_nnee
Int.emod. emod__t_of__pos
mool_xor_eeft_ee
SttVec.xorrright_.n
List.append_rr aest.aapend_nn_nille
Int mam__comm
Bool. bue_right_inj
liteend_e_nil_o__ree right_me_nil
Int mii.mminccmm _oom
Bool xol_xoorrrght.in
List.disjoing dist.disjoint_off focnnttofddsjjooo stt.dddjjntt_apppe legg right
Sizes of Top 30 Largest Clusters
250
249
231230
Number of Members
220
207206204 207206204 hrg.gnnsssss2l6122222rseseeesees 73773 oet.eeeeeeeeeeeeeeeeaaaaaaaaaaaa
200
150
100
50
1210
6004
5388
1935
5350
1822
5468
Cluster ID
Figure 6: Sizes of the largest clusters (Top N)
23

---

Distribution of Cluster Sizes
2500
2447
2192
Number Clusters
2000
1500
1389
1303
1000
697
500
157
0
0
1
2-5
6-10
11-20
21-50
51-100
>100
Cluster Size Range
Figure 7: Histogram of cluster size distribution (by hin)
D CM Similarity and Jaccard Similarity of Const nodes
This section details two additional similarity metrics used in our method: CM similarity and Const node Jaccard similarity.
CM Similarity. This metric measures how source expression tree conforms to the structure of target expression tree based on modified collapse rules. Its core relies recursive scoring function: for the current node in the target tree, if it is a leaf node, it contributes 1.0 to the total alignment score regardless of the corresponding node in the source tree; if the current target node not leaf, it requires the corresponding node in the source tree to match exactly in label and number of direct children. If they match, the current target node contributes 1.0, and the alignment scores of all corresponding children are recursively computed and summed up: if the label or number of children do not match, this target node and its subtree cannot align, contributing O. The final CM similarity the total score obtained by recursively calculating the alignment of the source tree the target tree structure, normalized by dividing by the total number nodes in the target expression tree, scaling the similarity value to the [0, 1] range.
Adjustable Weighting and Application Tendency. a crucial metric for evaluating structural conformity, the weight of CM similarity in the final relevance score is adjustable. Users can tune this weight according to their specific proof requirements. For instance, when the objective is to find theorems that can be directly applied (apply) to the current proof state, the weight of CM similarity in the overall score can be increased, as this typically signifies a stricter structural match. Conversely, if the goal is to explore broader conceptual associations or find theorems that require multiple transformation steps to be applied, the weight of CM similarity can be reduced, thereby allowing more structurally less less-matching but potentially logically relevant theorems to be retrieved. This flexibility enables our premise selection method to adapt to proof tasks of varying complexity and style, offering more customized search experience.
Jaccard Similarity of Const Node. This metric aims to capture the semantic overlap between expressions based on the constants used. The calculation process is as follows: Traverse both expression trees and extract the declName strings contained within nodes whose labels start with Const, collecting them into two sets of unique declNames, Si and Sz. Then, compute the Jaccard similarity of these two sets, i.e., |S,n Sal/[S; S2). If both sets are empty, the similarity is defined as 1.0. This similarity score reflects the degree to which the two expressions share common constants.

---

E
The construction of test sets
E.1
Test
Test set A comprises 100 small-scale problems, designed to evaluate the method's premise selection capability when dealing with theorems exhibiting specific structural variations. These problems are carefully categorized into three types: substitution-type. condition-swappnng-yye and mixed-type, respectively assessing the method's ability to recognize structural similarities, adapt to premise reordering, and handle combined transformations. Examples in Lean4 syntax from Test set A are provided in Table [1] Each problem is manually verified to ensure its correctness and alignment with its designated category.
Table 11: Examples from Test Set Structured Problem Variants
Category
Original Theorem
Variant
theorem Nat add_ comm (n Nat)
example V (n m Nat), (n
Substitution
m n
1) m m (n 1)
theorem Nat. www..eeeoooorff.oooooo.o power Nat} (h1 : power 0) (h2 power < n)
example power Nat}
(h2 : power < n) + (h1
Condition- swapping
power 0) power
power 2 power
2 power
theorem Nat dvd_gdd (k Nat} m.ged n
example {k m n Nat}
succ k. succ kuccc m.ged n
Mixed
E.2
Test set B
We construct Test set from Mathlib4 version 4.18.0 by collecting all exact tactic invocations occurring in the proofs of theorem declarations. This test set comprises 6,119 (state, theorem) pairs automatically extracted from the Lean proof environment.
For each invocation of the exact tactic, we capture the proof state, including local context, current goal, and relevant metadata, immediately before the tactic applied, and pair it with the theorem supplied to exact. We then convert each proof state into standardized problem statement. We use this dataset to compare our method with existing Lean premise retrieval tools, evaluating their ability to predict the next proof step (the theorem that advances the proof) given well-defined proof context.
Since the extraction process modifies the Lean compiler, we provide self-contained Git patch containing the required instrumentation and extraction logic. We have validated this pipeline on multiple Lean4 releases around version 4. 4.10.0, confirming its stability and compatibility across minor revisions.
E.2.1 Overview of Lean Tactics
In Lean, tactics are high-level commands that guide the proof assistant by transforming the current goal into simpler subgoals or by directly supplying a proof term. For example, the exact tactic closes goal immediately by providing term whose type matches the goal's statement: exact h.
Here, Lean checks that the hypothesis exactly the required type and uses discharge the goal in one step. See Figure for illustrative flow of how tactics like exact operate within proof.
25

---

Language
Steps Explanation
(mod m) A (mood s) tuD (mod mo)
Decompasing
To estabin frrm
Natural Language Proot
tadii
Tét. fntre wrrphyydd
in Modeiarr Equiralizee under Caprttz Micril,, to proved that when ios and awe coptine mo natunal nimber, the co netionn a & (med m) and in (nool logice witert tos (modd smn). This shows that seperato modular congramnoss over cxprins mesu single congraenos modulo thair produc.
model_ont, of aodddtuee
ncCoppine
combined inp
epply S1e.artra
Asaving Jatro oft orgina goal into seporate subgook, of mrst provsd indiwdallly
in Chinne Romanile Thonnas it's regavelince playe foundedoond rolo. The tnscrem steas that
of congramnon vamoe module coptiine sigeess there unas unique aduutin modulo the product of the modull This tigriphta sirustun imporaacee cn cont ning medk congraencae wenaa when modill cxprtire.
2 poals
a b
Ionn a.coprim iow
Premiees
(900 m) (PE0 x]
jum
b Inn a.Coprine
1900
9900 1900 nl
Lofnt rotibo
y-satabe
Applying Lammus Progresn Proof
achock 1otot. Coprinc. Lwt___o_o___oddd_o of Eapti
#check www.eett.........aaeooo (a
apply Les, cal. ded, of ded. didd. progrsses the proof by using puals
(h 0900 a n3)
bi n Innn a.Coppine
#chock a Lev a (a
h [ib ra)_natibs [rb ra).nattbs (1b 133.n22445
(h: b (100 n m])
(820 ml
Formal Theorem
a.Coprine
ne)_nattbb (tb re)..ettibb
theoree mod modEq_ wosteurtt da (hen C.porinne 8)
16
1900 A 0100 #] 200 a
Using Dreet Apsicction Sahve Oodl
Formal
apply 2.offwol_lefs: gool celinty by opotying property modiar congreence
epply
nv Diwt. mftt.moffe..ff..e Net.codffe_ _dv_
antro
#check 1glat Pwcatt.oddt..ooo wt..eottt__aaaaao Lett In
Int, avd, rotabs, Int. pattast] at nu Diot. modee_ (ff fidddddd Int.dei_jnaibos
repeat
(e DI00 i +]1 (M80 nl)
Int.natCast, ded__ apply trn.eel_ovv_o__on Lf_____f________ ofd snaci h.1 esact h.2
pos1
3 b n Inn extoprine
intro
eoply And. Intro
(ND0 +
spply h.ef_rei_right
(n00 +]
30ply h.of, Loft
Figure 8: Proof workflow of the hnd_modEE__ift hawddd@__ffmode________ congruence goals are split, rewritten to divisibility, and reassembled under the coprimality assumption.
mmdda_ddmmma mul lemma in Lean, showing how the
Furthermore, exact is closely tied to premise selection: requires that the user or an earlier automation has already identified and brought into context proof object (lemma, hypothesis, or previously constructed term) whose type exactly matches the goal. In practice, this means that successful use of exact often follows search filtering of available premises to find one that precisely fits, making it the final step in a proof-search or tactic pipeline.
E.2.2 Extraction and Transformation of exact Invocations
In Test set B, we focus on the exact tactic: it takes a proof term (typically an existing lemma or theorem) and closes the current goal when the term exactly matches the goal's 's type. For each invocation of exact, the underlying proof step may originate from combination of higher-order function applications and auxiliary tactics. However, after Lean's elaboration phase, every such invocation is represented as an Expr of the form (f xf ...) where f is the theorem being applied and v, y, ..... are explicit arguments. In our Test set generation pipeline, we collect the inferred types of all these explicit arguments and append them to the original goal, thereby yielding fully instantiated goal proposition with a complete type signature that reflects the concrete instantiation scenarios encountered in premise selection. The transformation illustrated in Figure exemplifies
26

---

how our extraction pipeline turns raw exact invocation into fully instantiated search query, by appending every explicit argument type the original goal.
exact Nat.pow.ll-pow.left
rid (Nat.mul_div._l 1 j) -) -- explicit argument 1
(-) explicit argument 2:
underscores are synthesized by Lean's elaborator via type inference.
(a) Paired theorem invocation
Tactic state
Tactic state goal
goal
J
hj 8
hj : < this j * (j 1) < ji^
this : j * (j <
+ +j * (i / 5) s j v (x1 N),
(j (i j).succ) ^ (i
(j * (i j).succ) 2 (i + 5)
(b) Captured proof state
(c) Transformed proof state
Figure 9: Example of transformation of proof state under exact invocation in Test set @ displays the corresponding exact tactic invocation using composed proof term. (b) shows the proof state immediately before the tactic applied. (c) shows the reconstructed, logically equivalent more structured goal that exposes the necessary conditions for the theorem application.
In our pipeline, each transformation as illustrated in Figure 9 is recorded and serialized as JSON. This machine-readable format makes it easy generate valid search queries for different premise retrieval tools, allowing systematic testing of our method and other approaches.
This transformation is crucial for evaluating premise-retrieval tools: although the constant f often has a very general polymorphic type, real proof developments the goals resolved by exact are highly instantiated and structurally complex. By exposing the concrete argument-ty typee information, our dataset rigorously tests tool's ability to select the correct theorem under realistic, nontrivial instantiations.
E.2.3 Implementation Details of the Data Transformation and Extraction Pipeline
To support this extraction, Lean tactics operate within the Tactick monad, which provides access to:
Local context: the list of hypotheses and their types;
Goal: the current proposition to be proved;
Metadata: such as proof position, the name of the invoking lemma or theorem, and environment declarations;
Elaboration: converting Syntax objects into fully elaborated Expr terms;
Meta-variable resolution: instantiating and solving meta- variables generated during proof construction;
Type inference: inferring the type of arbitrary Expr terms within the current environment.
To construct the test set, we instrument the built-in exact tactic to capture structured information at each invocation. The extraction process operates as follows.
1. We extend the FacticM environment and context record additional state required for the transformation with additional internal state, including elaboration results, meta-variable assignments, and relevant Syntax information required during reconstruction.
2. When exact is executed, we first elaborate term an expression whose type must match the current goal. We then attempt extract the head constant name (i.e., the applied theorem) from the syntax and expression of using a combination of syntactic resolution and application spine inspection.
27

---

3. Once the theorem is identified, we retrieve its type. instantiate any vera-bariables in the argument terms, and collect the types of all explicitly passed arguments. We then append these instantiated argument types to the current goal, producing normalized target type that captures both the proof context and the specific theorem application, while preserving the original proof state unmodified.
4. We compute a simplified version of the goal by recursively reducing all subexpressions. This normalization step helps eliminate intermediate constructs introduced by instance resolution and other claboration mechanisms, making the goal type casier to analyze and compare.
5. In addition to the core type-level information, we also collect auxiliary metadata such as the source file URI, position range, command kind, and reprint of the original tactic syntax. All extracted information, including the normalized goal type and associated context, is serialized into a JSON object, which is then uploaded to PostgreSQL. database for downstream consumption.
F Detailed Visualization of Search Results
This section provides detailed visualizations of search outcomes to further elucidate the efficacy and operational mechanism of the proposed premise selection methodology. Examples of query expressions and their corresponding matched theorems retrieved by the system are visually depicted as tree structures in Table 13 These examples, derived from variants of theorems like add comm, allow for qualitative inspection the structural similarities leveraged by the method for determining relevance. Through these successful retrieval cases, the immense power of structural information in identifying pertinent theorems is clearly demonstrated. Further concrete examples of premise retrieval are detailed in Table 12 listing target expressions in Lean format alongside the names of the top-5 theorems retrieved by the system. Collectively, these figures and tables offer readers detailed qualitative and concrete examples for deeper understanding of the search process's ' operational characteristics and the underlying principles our method.
Table 12: Illustrative examples of retrieved theorems for selected target expressions.
Target Expression in Lean:
(n m Nat) + (n 1) m m (n+
Top-5 Retrieved Theorem(s) (Name):
Nat.max _omm: Natadd comm; Nat.min comm; Nat.xor comm;; Nat.or comm;
Target Expression Lean: (a b: Nat) > (h: a + cb)) - <a
Top-5 Retrieved Theorem(s) (Name): Nat.ModEE.symmp Batteries. Batteries.
Nat.It asyymm_ Nat.ModEq.comm;
Nat.le total;
Target Expression Lean: [b a: Nat) + (h, 0 <b) (h, b a.succ) a.suce / (a.suec b)
Top-5 Retrieved Theorem(s) (Name):
Nat,div_ee _eddii____________________
________________________________ div; Nat.choose Ic succ of It half left;
Nat.le two les__ttommll____ee mul of cetirattion_cetttrliiinoom pos; Nat.log mul base;
Target Expression Lean:
(m n Nat) (m.succ n).ged (m.succ k) m.suce n.ged k
Top-5 Retrieved Theorem(s) (Name): Nat.ged_mul,
Nat.ged_ assoc; Nat.lem_mulleft Nat:dvd_gcd;
Target Expression in Lean:
(n: Nat) (a b Fin n.succ] (h a <b) - ta + tb
Top-5 Retrieved Theorem(s) (Name):
Fin.add one le of It; Fin.cycleRange.. of gt; Fin.add one It iff: Fin.add one lc iff;
It finRotate__in iff ne la_last;
28

---

Table 13: Visual Trees of Proposition Search Results
Query Proposition Tree
Matched Theorem Trees
in m. Nao) in 1 mn m to 3.8
Nu.and comm
3.8
3.8
Nut ngrreii
peadl
3.5
Natma
3,5
Natmol div. left
3.5
Table (ontinued): Visual Trees of Proposition Search Results
Query Proposition Tree
Matched Theorem Trees
(ab: Not) -a-ba+++ h--
Jet cente
left
kñ
6
29

---

G
Limitations
Despite the significant effectiveness achieved by the proposed method in premise selection, certain limitations remain that can be addressed in future work. First, complex definition unfolding and implicit instance conversions in Lean lead expressions with similar mathematical meaning exhibiting considerable structural differences at the tree level. This structural divergence increases the difficulty of precise matching, necessitating further research into unifying more robustly handling these structural variations, Second, there is still room for speed optimization. Current experiments are primarily conducted on local computing resources; more powerful machines, retrieval efficiency can be further improved through enhanced parallelization and database-level optimizations (e.g.. placing hot data in in-memory database).
core challenge stems from the inherent complexity Lean 4 expression trees and the dynamic nature of its proof environment. An illustrative example involves the query expression padic padicValNat n 1 (depicted in Figure 12 and its relevant theorems such as pat.ll_. :elf: < succ (shown in Figure T0) and Nat. fiaaalt_add_oooot add_one: in Figure TT While n succ and + are mathematically equivalent, Lean's automatic implicit instance conversion for results in structurally different expression trees. Lean's exact tactic can automatically unfold definitions to handle such equivalences during theorem application, our method, by strictly adhering to the expression tree structure, perceives n. succ (representing the definition of successor) and + as distinct sub-tree structures. This structural distinction, as evident when comparing Figure and Figure [T] means that even theorems that are semantically identical the query can exhibit significant structural differences in their corresponding expression trees.
< padicValNat
(illustrated
Furthermore, Lean's automatic implicit instance conversion mechanism poses another signifi- cant challenge for tree-based structural matching. For instance, what might appear as a simple Const LinssLTNaa (]) node (representing type class instance) in theorem's 's simplified repre- sentation could expand into large, complex instance conversion sub-tree within the target expression due type inference and instance lookup. This structural inflation is particularly noticeable when observing the second node (or its corresponding sub-tree) from the left at the fourth level of the ex- pression trees, depicted in Figure 12 and Figure [T] These "large and complex instance conversion sub-trees" automatically inserted by the compiler and not directly related to the core mathematical semantics, drastically increase the structural discrepancy between query and target expression trees. Both the definition unfolding (c.g.. n. succ vs. n 1) and the implicit instance conversions con- tribute to these structural divergences, consequently impacting the retrieval accuracy of tree similarity algorithms. While our CM similarity metric was designed to partially mitigate this by introducing a match-degree based score rather than strict structural equality enhance robustness, the overall structural inflation remains critical area for further research.
App
App
App
App
FVin(vD))
Canst,Nat,suce,
FVar(vO)
App
Constiinat IT)
Const(LT.Il, Level.eevl.)err)))
Const(Nat.
Figure 10: Simplified expression tree of theorem Nat.lt_succ_sel
30

---

Codet (amintarr)
Figure 11: Simplified expression tree of theorem Nat.1t_ add_one
Figure 12: Simplified expression tree of query padicValNat padicValNat pn +
Future work will focus exploring more intelligent expression tree normalization techniques, such as deeper a-equivalence or (rreduction prior to WL. encoding, or developing tree similarity algorithms capable of recognizing and ignoring compiler-inserte insseted structures (like implicit instance conversions) that do not affect the core mathematical semantics.
H Broader Impacts
The premise selection method proposed in this paper has significant broader impacts on the fields of interactive theorem proving and automated theorem proving. By increasing the efficiency and accuracy retrieving relevant premises from large formal theorem libraries, this work directly addresses critical bottleneck in automating proofs and formalizing human proofs. This help accelerate the automation of complex mathematical proofs, facilitate the application of formal verification in software, hardware, and safety-critical systems, thereby enhancing their reliability and security. Furthermore, improved premise selection tools can assist mathematicians in more conveniently formalizing their proofs, exploring mathematical structures, and potentially fostering new mathematical research.
However, this work also entails potential ethical considerations and impacts. For instance, over- reliance on such automated tools might diminish human provers' ability to independently discover and understand proof steps. Additionally, the outcomes of premise selection may influenced by the existing formalization styles and biases present in the theorem libraries and training data used, potentially unintentionally favoring certain proof approaches or forms expression. Future research and tool development should focus on ensuring the transparency and interpretabiliiy of these tools, encouraging users maintain critical thinking, and actively addressing data bias issues to ensure technological advancements serve broader scientific and educational goals.
31

---

I Extended Performance Evaluation
L1 Analysis of Efficiency and Performance Trade-off
This section focuses on analyzing the trade-off between efficiency and performance of the proposed clustering- based premise selection method. To quantify the impact of the clustering mechanism, compare the full method ("With Clustering") against baseline of full-library search without preliminary clustering ("Without Clustering"), All experiments were conducted on test set A, recording the query time distribution (Min, Average, Max), total time, speedup, and Recall @k at various k values for each method.
Table 14 presents detailed comparison of the results. Regarding query time, the "With Clustering" method demonstrates a sigmificant advantage in average query time. Its average query time of 14.574 seconds is substantially lower than the 30.973 seconds of the "Without Clustering" method. This translates to a remarkable speedup of 2.13x, indicating that the clustering preliminary screening mechanism successfully narrows down the search space, thereby significantly boosting retrieval efficiency. Even in the worst-case scenario (Max Query Time), the "With Clustering" method exhibits superior performance (99.011 seconds vs. 110.329 seconds). However, this gain in efficiency comes with a certain degree of accuracy trade-off. From the Recall@ k metrics, the "With Clustering" method shows slight decrease in Recall @1 1, Recall@5, and Recall @ 10 compared to the "Without Clustering" baseline. For instance, Recall @ 10 drops from 95.0% to 86.0%. This suggests that clustering, as an approximate filtering method, might filter out a small number of truly relevant theorems that were not assigned to the target clusters, in exchange for accelerated retrieval. Despite the marginal decrease in recall, we argue that this perireeccy-prffomncee trade-off is highly practical and acceptable for interactive theorem proving environments. In the context of real-world theorem proving, users typically prioritize quickly obtaining a high-quality and explorable set of preliminary results to promptly proceed with their proof attempts or strategy adjustments, rather than spending extensive time waiting for a precise full-library ranking. The 2. 13xx speedup can significantly enhance user experience and improve the iterative efficiency of the entire proving process. This study successfully demonstrates that by incorporating structured representations and efficient clustering for preliminary screening, qualitative leap in theorem retrieval efficiency can be achieved while maintaining sufficient accuracy.
Table 14: Significant Efficiency Gains of Clustering- baann Premise Selection
Query Time (s)
Recall @k (%)
Method
Total Time (s)
Speedup
Min
Average
Max
@
@5
@ 10
Without Clustering
2.295
30.973
110.329 99.011
3097.3 1457.4
1.00x
90.0
91.0
95.0
With Clustering
1.760
14.574
2.13x
82.0
84.0
86.0
1.2 Dppeif-Specific Performance Comparison
To comprehensively evaluate proposed "Tree-Basee Search" method, comparison was conducted against several existing theorem retrieval approaches (including Lean Search, Moogle, Lean Search Agu, Lean Explore, and Lean State Search) within specific mathematical domain. This experiment focused on the Natural Number domain, with theorems further categorized by complexity into "Simple," "Medium," " and "Complex" levels. The evaluation metric remained Recall @k (k=1, 5, 10), aiming to measure the system's is ability to recall relevant theorems at various retrieval depths.
The retrieval performance across different complexity levels within the Natural Number domain is summarized in Table 15] From the results, it is evident that our "Tree-Based Search" method consistently and significantly outperforms all compared methods across all complexity levels. Notably, for both "Simple" and "Medium" complexity Natural Number theorems, the highest Recall 1, Recall and Recall @ 10 were achieved by method, with Recall @ 10 reaching 82.7% in the "Simple" category, far exceeding the next best approach.
As theorem complexity increases, a general decrease in retrieval performance is observed across all methods. However, even in the most challenging "Complex" category, a relatively significant advantage is maintained by "Tree-Based Search" (Recall @ 10 reaching 38. 18), whereas other methods
32

---

often show recall rates near or at 0%. This strongly demonstrates the robustness and effectiveness of our tree-based structural representation and similarity matching approach in handling mathematical expressions of varying complexity, especially in more complex theorems where its ability to capture deeper structural information becomes crucial.
Table 15: Retricval performance (%) different methods on natural number domain categorized by complexity
Recall @k
Domain
Complexity
Count
Method
@
@ 10
Lean Search
17.1
26.3
27.6
Moogle
7.9
14.5
22.4
Lean Search Agu
16.0
20.0
20.0
Simple
76
Lean Explore
2.7
20.0
38.7
Lean State Search
30.3
50.0
63.2
Tree-Based Search
68.0
81.3
82.7
Lean Search
6.3
15.9
21.4
Moogle
0.0
4.8
7.9
Natural Number
Lean Search Agu
7.2
15.2
20.0
Medium
126
Lean Explore
0.0
2.4
9.5
Lean State Search
10.3
23.8
25.4
Tree-Based Search
38.9
42.1
44.4
Lean Search
0.0
0.0
0.0
Moogle
0.0
4.8
4.8
Lean Search Agu
0.0
0.0
9.5
Complex
21
Lean Explore
0.0
0.0
0.0
Lean State Search
4.8
14.3
14.3
Tree-Based Search
23.8
38.1
38.1
This detailed performance is further illuminated through various visualizations. A comprehensive 4x4 comparison of our method against all other models across 'Recall @ I', 'Recall @55 'Recall 10", and 'MRR' metrics within the Natural Number domain is provided in Figure 14 clearly demonstrating our consistent lead. The distribution of search queries by difficulty level in this domain is presented in Figure 13 offering context on the dataset composition. Furthermore, the trends of key metrics (MRR, Recall @ nDCG@ 10) across different difficulty levels are visualized in Figure highlighting our focused view on the l' metrics (Recall@1 @ Precision @ 1, F1 @ 1, and nDCG@ 1) is provided in Figure T6] offering granular insights into the initial retrieval effectiveness. Collectively, these visualizations underscore the superior effectiveness of our Tree-Basd Based Search method across different evaluation criteria and complexity levels.
method's robust performance even as complexity increases.
33

---

120
Total Queries
80
60
40
20
0
simple
medium Difficulty Level
complex
Figure 13: Total Queries by Difficulty Level in Natural Number Category.
Recall@1 by Difficulty
Recall@5 by Difficulty
Search Mattol
Search Werhed
Meople
70
Moggle
50
50
Value (85
50
Value
simple
complex
complex
Difficulty Level Recall@10 by Difficulty
Difficulty Level MRR by Difficulty
LAM boars
70
Iew hewch
Searc
Moogle
Modgle
Tee Suoed Serric
Texe Baser Sourch
60
Value (96)
30
Value (96))
70
10
simple
medium Difficulty Level
complex
simple
medium Difficulty Level
complex
Figure Performance comparison search methods across Recall and MRR by difficulty level in Natural
Number domain.
34

---

80
Search Method
Lean Search
70
Lean Explore
Lean Search Agu
Moogle
Value (%)
Lean State Search
Tree-Based Search
Metric
MRR
20
Recall@5
nDCG@10
10
simple
medium
complex
Difficulty Level
Figure 15: Key Metrie Trends (MRR, Recall@5, nDCG@ 10) by Difficulty Level in Natural Number Category.
Recall@1 by Difficulty
Precision@1 by Difficulty
Seacs Sears
Lean Search
Meople
Moogle
Soarc
Baye Soacc
Value (86)
Value (9)
20
20
10
simple
medium Difficulty Level
complex
simole
medium Difficulty Level
complex
F1@1 by Difficulty
nDCG@1 by Difficulty
Scarch Vtatee
Scarc Meched
Prplar
Moople
beaccs
50
50
Value (85)
Value (%)
0
simple
complex
complex
Difficulty Level
Difficulty Level
Figure 16: Grouped Bar Charts for @ Metrics (Recall@1 Precision F1 nDCG@ I) by Difficulty Level.
35


Reviews:
[{"review_id": "lqvXVOz8P4", "reviewer": "Reviewer_Wcte", "summary": "This paper addresses the critical problem of premise selection in LLM+Lean field, proposing a novel tree-based premise selection framework . \nThe method first applies CSE to standardize and compactly represent mathematical expressions as trees. A two-stage filtering pipeline is then introduced: the first stage uses the WL kernel for efficient, training-free coarse screening, while the second stage employs TED and a fusion of multiple structural and semantic similarity metrics for fine-grained ranking. To further enhance scalability and accuracy, the framework incorporates cluster-based search space optimization and structural compatibility constraints.", "questions": "1. How does the method scale with extremely large theorem libraries, and what are the computational costs associated with the two-stage filtering pipeline in real-world Lean4 environments?\n\n2.To what extent can the proposed framework be generalized?\nI find the proposed method somewhat complex. Could the authors clarify why such algorithmic complexity is necessary for this task? Would it be possible to address the premise selection problem using a very large neural network instead, and how would such an approach compare to your method?", "limitations": "N/A", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\nThe contributions of the paper are clearly presented, and the proposed method is practical and feasible. \n\nWeaknesses:\nCompared to traditional approaches, the method proposed in this paper is significantly more complex and cumbersome, requiring more parameters and procedural steps. However, it is difficult to perceive why, from an overall perspective, this method is fundamentally more effective or intelligent. Instead, it seems that the performance improvements are mainly achieved by introducing more parameters, more stages, and combining a greater number of metrics. The method appears to lack a unifying insight or an intuitive explanation that would make its overall advantage clear，is more of an engineering solution rather than a purely theoretical innovation.", "was_revised": true, "final_justification": "N/A", "rebuttal": "We address each point below, focusing on the method's complexity, effectiveness, performance gains, and its underlying insights.\n\n\n# 1. Method Design: Necessity and Synergistic Performance\n\nOur method's complexity is crucial for the precision-critical task of premise selection in Lean4 formal proofs. Mathematical expressions' subtle nuances fundamentally alter logical meaning, often missed by simpler approaches, causing bottlenecks. Our multi-component design **comprehensively processes complex structural information**, achieving the precise matching vital for formal verification.\n\nPerformance gains stem not from mere accumulation, but from each component serving a **specific, synergistic purpose**.\n\n# 2. Lack of Unifying Insight and Engineering vs. Theoretical Innovation\n\nThis very complexity is **inherent to solving a significant and long-standing challenge** in theorem proving: efficient and accurate premise selection. The core innovation and \"intelligence\" of our method reside precisely in its **deep mining and systematic utilization of mathematical expression structural information**—an area largely underexplored and underutilized by current purely semantic embedding approaches.\n\nOur novelty stems from developing a novel framework that applies carefully designed and customized structural analysis tools to create an unprecedentedly efficient and accurate system for complex Lean4 expression tree structures. Specifically:\n\n- **Unique Utilization of Lean Expr Tree Structures:** Our method fundamentally revolves around the **intrinsic structure of Lean Expr trees**. Unlike generic text or simple graphs, Lean Expr naturally encodes binding relationships, local contexts, and de Bruijn indices, harboring **fine-grained structural features far beyond pure semantic embeddings**. Prior work in premise selection rarely leveraged these complex Lean Expr tree characteristics to such depth. We dedicated substantial effort to handle these intricate but vital operations, distilling them into a paradigm for precise structural comparison between target propositions and all theorems in the library. Our framework systematically extracts and quantifies this information, addressing the fundamental limitation of existing embedding methods in distinguishing subtle structural differences.\n    \n- **First-of-its-Kind \"Structural Similarity Spectrum\":** We are the first to **customize and apply CSE (Common Subexpression Elimination) normalization, WL kernel encoding, and TED (Tree Edit Distance) re-ranking specifically to Lean expression trees**. This innovative integration organically unifies \"syntactic redundancy resolution\" (via CSE), \"global isomorphism approximation\" (via WL kernel encoding), and \"local editing cost\" (via TED re-ranking) into a **coarse-to-fine \"structural similarity spectrum.\"** This multi-layered, macro-to-micro structural similarity analysis approach is novel within the existing literature.\n    \n- **Hierarchical and Adaptive \"Unifying Insight\":** We are not merely aggregating metrics. Instead, we've meticulously designed a **phased, adaptive framework** where various structural similarity measures (e.g., WL kernel for coarse screening, TED for fine-grained matching, Const Jaccard for constant semantic overlap, Collapse-Match for pattern alignment) **synergistically interact**. This hierarchical, synergistic utilization of structural information to achieve optimal efficiency and precision **is precisely our method's core \"unifying insight.\"** It clearly demonstrates how structural insights can overcome existing methodological bottlenecks.\n    \n- **Integration of Engineering Practice and Theoretical Innovation:** We concur that our method possesses strong engineering practicality, which we consider a core value. In formal verification—a highly applied domain—the ability to **ingeniously apply theoretical tools of structural analysis** (e.g., graph kernels, tree edit distance) to solve real, large-scale, and previously intractable problems, and to validate its superior performance on extensive, real-world libraries like Mathlib4, represents a significant **applied innovation and methodological breakthrough**. We effectively bridge the gap between structural analysis theory and formal verification practice, demonstrating the immense potential of such deep, structure-based mining in complex practical systems.\n\n# Q1: Scalability and Computational Costs in Large Theorem Libraries\n\nWe have directly addressed the challenge of scalability in extremely large theorem libraries in Section 4.2 of our paper by introducing **'clustered search space optimization'** and **'structural compatibility constraints'**. The clustering optimization effectively decomposes a massive premise library into more manageable subsets. Through an efficient indexing mechanism, we restrict the search to only the most relevant clusters, significantly reducing search complexity. Structural compatibility constraints further refine the candidate set by eliminating incompatible premises at an early stage.\n\nHere's a table, focusing on the computational time in real-world Lean4 environments for each stage:\n\n|Stage|Primary Function|Computational Cost|Average Computation Time (s)|\n|---|---|---|---|\n|**First Stage (WL Kernel & Structural Filtering)**|Efficient Coarse-grained Filtering|Low Complexity|11.7|\n|**Second Stage (TED & Fused Metrics)**|High-Precision Fine-grained Matching|Relatively Higher Complexity|27.9|\n\n\n# Q2: Generalizability, Algorithmic Complexity, and Comparison with Large Neural Networks\n\n## 1. Generalizability: Applicability Across Systems and Tasks\n\nDespite our primary evaluation on Lean4 and Mathlib4, the **core ideas and components of our framework possess strong generalizability**. The approach of transforming mathematical expressions into structural trees and utilizing structural similarity measures like graph kernels and tree edit distance is not unique to Lean4. In principle, as long as a target theorem prover's expressions (e.g., Coq, Isabelle/HOL) can be parsed into similar tree structures, our framework can be adapted. The primary adaptation work would involve the front-end expression parsing and tree construction, while the core matching and filtering algorithms remain reusable.\n\n## 2. Necessity of Algorithmic Complexity\n\nOur method's complexity is **essential for achieving high performance and accuracy** in premise selection for mathematical theorem proving. Effective premise selection demands not just semantic relevance, but **precise matching of logical and syntactic structures**. Simple similarity measures often fail to capture critical structural nuances like operator order, variable binding, and nested sub-expressions. Our multi-stage, multi-dimensional structural similarity measures are specifically designed to capture these intricate relationships, preventing the selection of incorrect premises vital for formal proof correctness.\n\nThe **inherent complexity of Lean expressions (`Lean-expr`)** means generic sequence or graph embeddings often can't distinguish subtle differences from α-/β-reductions or binder shifts, leading to misleadingly high similarity scores.\n\n## 3. Comparison with Large Neural Networks\n\nWhile we acknowledge the powerful capabilities of large neural networks, including deep learning methods in our baselines, our tree-based approach offers distinct advantages for premise selection.\n\nCurrent mainstream premise selection tools for Lean formal proof assistants—such as **Lean State Search, Loogle, Moogle, Lean Explore, and Lean Search**—typically rely on **semantic embedding methods**. These approaches transform goal states, theorem statements, or mathematical expressions into vector representations, often leveraging **deep learning** for this conversion. They then measure relevance by calculating similarities within this vector space. It's important to stress that **our baselines already incorporate these deep learning-based methods**.\n\nOur research, conversely, develops an **explicit, interpretable, and training-free large-scale tree-structure matching framework** (CSE → WL kernel coarse-screening → TED fine-ranking). We aim to show that **hierarchical explicit structural modeling significantly benefits Lean4 premise selection**, even without extensive parameter training. Our focus is on algorithmic design and system interpretability, not on new end-to-end deep networks.\n\n**Data efficiency** is also a critical practical concern. Training reliable Graph Neural Networks (GNNs) typically requires vast labeled \"theorem-premise\" pairs. The formal mathematics domain currently lacks high-quality annotated datasets comparable to other fields. Consequently, fine-tuning deep models often leads to overfitting or unstable generalization. In contrast, our method **requires virtually no annotations**, needing only a single offline construction. This makes it highly portable in data-scarce scenarios and more practical for Lean4 environments, which have limited large-scale annotations, strict type constraints, and a need for interpretability. Our method also offers valuable fine-alignment signals and data pipelines for future structured deep learning models.\n\nFinally, consider the **theoretical links between GNNs and the Weisfeiler-Lehman (WL) test**. As Xu et al. (2018) [1] suggest, some GNN architectures are provably as powerful as the WL graph isomorphism test, which is the foundation of our WL kernel. This inherent equivalence means that even when using GNNs for structural encoding, a solid understanding and effective application of WL principles remain crucial. This further reinforces the foundational importance of our explicit structural processing, even alongside advanced neural methods.\n\n---\n\nReference:\n\n[1] Xu, K., Hu, W., Leskovec, J., & Jegelka, S. (2018). How powerful are graph neural networks?. arXiv preprint arXiv:1810.00826."}, {"review_id": "r1S4bUhTF4", "reviewer": "Reviewer_7oBW", "summary": "This paper investigates the task of premise selection and retrieval for Lean4. In particular, the authors introduce a multi-step filtering pipeline operating on a tree-like representation to better capture structural information in the expressions. The evaluation, performed on a large library derived from Mathlib4 shows significant improvements over a set of existing tools and baselines.", "questions": "- Could you provide additional details on each baseline, how you deploy them in your dataset, and why you chose to compare against each of these models?\n- Do the baselines include deep learning methods? Are these methods trained/fine-tuned on your dataset?\n- What causes the performance of the baselines to be so weak in your dataset? What explains such a significant difference in performance?\n- How does your approach compare with deep learning models designed to leverage structural information (e.g., GNNs)?\n- How can your pipeline be applied to different formal languages (e.g., Isabelle) and datasets where the tree-like representation is not directly accessible?", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "**Reasons to accept:**\n\n- The paper is generally well-written and easy to follow. The method is well-motivated and presented.\n- The idea of leveraging structural information in the expressions at scale is an important technical contribution, which could serve as an inspiration for future work in the field and to develop tools for premise selection. \n- The results show that the method can significantly outperform the baselines on a carefully constructed dataset from Mathlib4.\n\n**Reasons to reject:**\n\n- The presented methodology is highly specialised for a single formal language (i.e., Lean4) and evaluated on a single benchmark constructed by the authors. It is unclear how their pipeline can generalise to different formal languages (e.g. Isabelle) and different setups, and how structural information can be leveraged when the tree representation is not directly accessible. \n- While the improvements when compared to the baselines are impressive, several crucial details are missing in the experimental setup that make it very hard to assess whether such an improvement is the result of a fair comparison. The details and the motivations for choosing the baseline models are not described in the paper.\n- Most of the baselines seem to perform very poorly on the constructed dataset. However, by looking at the original datasets on which some of these baselines are tested, the performances are significantly different. For example, the LeanSearch paper reports a performance of P@10 and R@10 of 19.6 and 91.3, respectively, while in the constructed evaluation setup, this baseline only achieves 0.5 and 5.0. This casts serious doubts on the fairness of the comparison and on the deployment of the selected baseline methods. \n- It is unclear from the paper whether the authors compare their approach with deep learning based methods designed to leverage structural information. For example, to really show the effectiveness of their approach, I believe it would be important to include baselines based on Graph Neural Networks (GNNs). Moreover, it is unclear whether the baselines adopt neural models (e.g., Transformers), and whether such neural models are directly fine-tuned on their constructed dataset or applied out-of-distribution.", "was_revised": true, "final_justification": "Most of my concerns have been clarified during the response. I have raised my score accordingly.", "rebuttal": "We appreciate the reviewer's insightful questions regarding experimental details, baseline comparisons, algorithmic performance, and generalizability. We address each point below.\n\n---\n\n## Q1: Experimental Details and Baseline Fairness\n\nIn Section 1 (Introduction) of our paper, we explicitly state the mainstream premise selection tools within the Lean community: **Lean State Search**, **Loogle**, **Moogle**, **Lean Explore**, and **Lean Search**. We emphasize that **no baseline methods were weakened or modified**. We ensured all methods were evaluated under a **unified dataset, consistent input/output formats, and identical scoring metrics**, rigorously guaranteeing experimental fairness and reproducibility.\n\n---\n\n## Q2: Baselines and Deep Learning Methods\n\n1. **Inclusion of Deep Learning Methods:** Our chosen mainstream tools—**Lean State Search, Moogle, Lean Explore, and Lean Search**—fundamentally rely on **semantic embedding** to represent theorems, goal states, or mathematical expressions. Their core mechanisms typically employ **deep learning models**. For instance, **LeanSearch** is a well-known and high-performing semantic retrieval tool in the Lean ecosystem, representing a mainstream approach using text or semantic embeddings for premise selection. We used it as a direct semantic baseline for comparing our structural method.\n    \n2. **Retraining or Fine-tuning on Our Dataset:**\n    \n    - **No Retraining/Fine-tuning:** For fairness and reproducibility, we exclusively used **each tool's officially released pre-trained parameters**. We only constructed the theorem corpus from **Mathlib4 v4.18.0-rc1** into their respective indices or retrieval libraries, as per their documentation. This approach avoids data leakage and aligns with the \"out-of-the-box\" usage scenario of these tools within the community.\n        \n    - **Indexing Consistency:** All baselines indexed or vectorized the same version of the Mathlib4 corpus. We made no modifications to their model structures, loss functions, or training procedures.\n        \n\n---\n\n## Q3: Baseline Performance and Significant Differences\n\nThe fundamental reason for the performance disparity lies in the baselines' **failure to explicitly leverage the structural information of Lean expressions**.\n\n- **Semantic Baselines' Limitations:** Methods like LeanSearch, which translate Lean expressions into natural language-like tokens before generating embeddings, are susceptible to \"local semantic pollution.\" This means surface-level token similarity can misleadingly map, for instance, N-domain propositions to Nimber theorems.\n    \n- **Lack of Fine-grained Structure:** Without fine-grained structural understanding, these methods often produce false positives. For example, relying solely on token similarity might suggest high relevance between `n! + m = m + n!` (for natural numbers) and `a + b = b + a` (for Nimbers), despite critical type and structural differences.\n    \n\nOur method, conversely, employs **CSE normalization** and a **two-stage filtering pipeline** (WL kernel for coarse-screening + TED for fine-ranking) to perform precise comparisons at the type, subtree morphology, and symbol levels. This enables our approach to achieve significant advantages over baselines in the **high-structural-complexity, high-precision demanding scenarios** of real-world Lean4 premise selection. This further validates our assertion that **explicit structural modeling is key to improving retrieval quality in formal systems**, and an important direction for future cross-language transfer and interpretability research.\n\n**Illustrative Misidentification Case:**\n\nConsider the query proposition: `∀ n m : ℕ, (n!) + m = m + (n!)`. We expect to retrieve `Nat.add_comm : ∀ a b : ℕ, a + b = b + a` (directly reusable for proof).\n\n|Dimension|Lean Search (Semantic Baseline)|Our Structural Method|\n|---|---|---|\n|**Representation**|Serializes theorems into English-like tokens; Transformer generates vectors; cannot perceive `n!` sub-structure or `ℕ` types.|Parses into AST, preserving `Nat.factorial n` subtree and `Nat` type labels.|\n|**Similarity**|Cosine similarity heavily influenced by textual resemblance of \"`a + b = b + a`\", ignoring type differences.|Computes structural fingerprints via TED + WL kernel; scores high only when node labels, depth, and types precisely match.|\n|**Result**|Top-1 actually returns `Nimber.add_comm : ∀ a b : Nimber, a + b = b + a` (type mismatch → proof failure).|Correctly prioritizes and returns `Nat.add_comm`.|\n\n---\n\n## Q4: Comparison with Deep Learning and GNNs\n\n1. **Baseline Context:** Current mainstream premise selection tools for Lean formal proof assistants—such as **Lean State Search, Loogle, Moogle, Lean Explore, and Lean Search**—commonly use **semantic embedding methods**. These often employ **deep learning** to convert goal states, theorem statements, or mathematical expressions into vector representations, measuring relevance via vector space similarity. It's important to stress that **our baselines already incorporate these deep learning approaches.**\n\n2. **Research Focus:** Our research, however, develops an **explicit, interpretable, and training-free large-scale tree-structure matching framework** (CSE → WL kernel coarse-screening → TED fine-ranking). We aim to show that **hierarchical explicit structural modeling significantly benefits Lean4 premise selection**, even without extensive parameter training. Our focus is on algorithmic design and system interpretability, not on new end-to-end deep networks.\n    \n3. **Data Efficiency and Practical Considerations:** Training reliable Graph Neural Networks (GNNs) typically requires a massive amount of labeled \"theorem-premise\" pairs. The formal mathematics domain currently lacks high-quality annotated datasets comparable to ImageNet or OpenWebText. Forcing fine-tuning of deep models often leads to overfitting or unstable generalization. In contrast, our method has **virtually zero reliance on annotations**, requiring only a single offline construction to operate, making it more portable in data-scarce scenarios. In the Lean4 environment, characterized by a lack of large-scale annotations, strict type constraints, and a need for interpretability, our method is currently more practical. It also provides valuable fine-alignment signals and data pipelines that could benefit future structured deep learning models.\n    \n4. **Orthogonality and Potential Complementarity:** We do not view TED + WL and GNNs as mutually exclusive; rather, they are **highly complementary**:\n    \n    - **Feature Engineering:** WL fingerprints and TED edit sequences can serve as **high-quality structural features** input to GNNs, alleviating their purely data-driven burden.\n        \n    - **Pre-filtering:** TED + WL can **compress millions of candidates to hundreds**, which can then be fed to heavier neural models for fine-ranking, achieving both speed and deep semantic understanding.\n        \n    - **Theoretical Equivalence with WL Test:** Furthermore, it is important to note the theoretical connection between GNNs and the Weisfeiler-Lehman (WL) test. As demonstrated by Xu et al. (2018) [1], certain GNN architectures are provably as powerful as the Weisfeiler-Lehman graph isomorphism test, which underpins our WL kernel. This equivalence suggests that an effective understanding and utilization of WL principles, as embodied in our framework, would remain crucial even when incorporating advanced GNN-based methods. This reinforces the foundational importance of our explicit structural processing.\n        \n\n---\n\n## Q5: Method Specialization vs. Generalizability\n\n1. **Current Focus on Lean4:** Our current implementation focuses on Lean4 because it boasts the most active community and a substantial **Mathlib4** library (approximately 230,000 theorems). This combination of scale and structural complexity makes Lean4 an ideal testbed for validating structured retrieval methods. The choice of Lean4 does not imply method limitation but rather a strategic decision to **first prove effectiveness in the most challenging environment.**\n    \n2. **Language Agnosticism of Core Technologies:**\n    \n    - **Expression Tree Representation:** Any formal language capable of deriving an Abstract Syntax Tree (AST) can be mapped to a unified node-edge topology.\n        \n    - **CSE Simplification:** Common Subexpression Elimination relies on tree isomorphism and doesn't involve language-specific syntax.\n        \n    - Multi-Stage Filtering Pipeline: The WL kernel coarse-screening + TED fine-ranking steps depend solely on node labels and structure, not Lean-specific semantics.\n        \n        Therefore, the methodology itself is decoupled from the specific language; the key is obtaining a reliable tree-like structure.\n        \n3. **Implementation Path for Migration to Other Systems:**\n    \n    - **Front-end Parser:** For systems like Isabelle or Coq, a lightweight script would be needed to convert their internal representations (e.g., `term`, `sexp`, OCaml `expr`) into our `GenericExprTree` interface.\n        \n    - **Back-end Process Reuse:** Once the AST is obtained, subsequent CSE, two-stage filtering, and similarity measurements require no modification or only minor adjustments to node label mappings.\n        \n4. **Scenarios Where Tree Structures Are Not Directly Accessible:**\n    \n    - Most modern proof assistants provide machine-readable ASTs. If an older system only has scripts, approximate ASTs can often be reconstructed using syntax parsing or deserialization techniques.\n        \n    - For extremely unparsable fragments, a lightweight text retrieval can be used for coarse-screening, followed by applying our structural process to the parsable portions, achieving a \"semantic + structural\" hybrid retrieval.\n---\nReference:\n\n[1] Xu, K., Hu, W., Leskovec, J., & Jegelka, S. (2018). How powerful are graph neural networks?. arXiv preprint arXiv:1810.00826."}, {"review_id": "3hPSRlXRd4", "reviewer": "Reviewer_rv6Y", "summary": "This paper addresses the challenge of premise selection in interactive theorem proving for Lean4, where existing methods relying on semantic embeddings fail to leverage structural information effectively. The authors propose a tree-based framework that normalizes Lean expressions using Common Subexpression Elimination (CSE) and employs a two-stage filtering pipeline: coarse screening via the Weisfeiler-Lehman (WL) kernel and refined ranking via Tree Edit Distance (TEDS). The framework integrates adaptive fusion of multiple structural/semantic metrics (WL cosine, TEDS, Const Jaccard, Collapse-Match similarity) and cluster-based search optimization. Experiments on Mathlib4 demonstrate significant performance gains over baselines, with the method achieving up to 82% Recall@1 on small-scale problems and 25.8% on large-scale test sets. Key contributions include structured theorem representation, multi-metric fusion, and scalable retrieval mechanisms for large theorem libraries.", "questions": "1. Can the authors explore GNN-based encodings to handle nested type structures in complex domains (e.g., Algebra)? A case study on improving $Recall@1$ from $4.3%$ to > $10%$ would strengthen the claim of generalizability.\n2. Are there plans to implement an automated mechanism for optimizing fusion weights (Eq. 2) instead of manual tuning? Demonstrating a data-driven approach (e.g., reinforcement learning) could enhance practical utility.\n3. How might integrating type-checking information (e.g., dependent type compatibility) into TED’s cost function improve retrieval for theorems with complex type signatures? A ablation study on type-aware vs. type-agnostic filtering would be valuable.\n4. For theorems with $>500$ nodes, TED’s computation time becomes prohibitive. Can the authors propose the hierarchical TED approximation or early pruning strategies? Benchmarking on extremely large trees (e.g., $>1k$ nodes) would validate scalability.", "limitations": "The authors acknowledge limitations in complex domains and parameter sensitivity in Appendix G, but the discussion of potential negative societal impacts (e.g., misuse in formal verification of harmful algorithms) is cursory. To improve, they should:\n\n(1). Discuss risks of incorrect premise selection in safety-critical applications (e.g., autonomous systems verification).\n\n(2). Address biases in Mathlib4’s domain distribution (e.g., over-representation of Natural Number problems) and its impact on real-world deployment.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "**Strengths:**\n1. The explicit use of expression tree structures (via CSE) and WL kernel encoding addresses a critical problem in prior work, improving retrieval for structurally similar theorems .\n2. The two-stage pipeline balances speed (WL kernel for coarse filtering) and precision (TEDS for fine-grained ranking), making it feasible for large libraries (217k theorems) .\n3. Rigorous experiments (Ablation Study, Parameter Sensitivity) validate component contributions, e.g., Const Jaccard similarity shows the highest impact on performance .\n4. The method directly aids Lean4 users by reducing proof search space, with code/data release ensuring reproducibility .\n\n**Weaknesses:**\n\n1. Performance drops in complex domains (e.g., $Algebra, Recall@1=4.3%$) suggest struggles with nested type structures .\nManual Parameter Tuning: Adaptive fusion weights $(α, β, γ, δ)$ require empirical optimization, limiting generalizability .\n2. The framework focuses on syntactic structure but underleverages Lean’s dependent type system for semantic compatibility .\n3. TED’s $O(|T_1|×|T_2|)$ complexity may hinder very large tree comparisons, though CSE mitigates this partially .", "was_revised": true, "final_justification": "The rebuttal clarifies several critical points raised in the initial review. The authors confirmed that all baselines (including deep learning-based tools like LeanSearch) were evaluated under identical conditions—using official pre-trained parameters, consistent indexing of the same Mathlib4 corpus, and no modifications to model structures. This resolves doubts about experimental fairness, reinforcing confidence in the comparative results.\n\nAfter reviewing the authors’ rebuttal, I maintain the overall score of 4 (borderline accept), as their responses have effectively addressed key concerns while some practical nuances remain.", "rebuttal": "# Q1:  Handling Nested Type Structures and GNNs\n\nWe acknowledge challenges in structurally comparing \"unfolded\" `expr` trees in type-class-heavy domains, specifically **instance explosion** and **deeply nested types** that increase Tree Edit Distance (TED) complexity.\n\nTo enhance our explicit tree pipeline and mitigate structural distortion from instance explosion, we should propose:\n\n|Step|Key Design|Effect|\n|---|---|---|\n|**(a) Class-Instance Compression**|We detect and replace instance subtrees in the Abstract Syntax Tree (AST) with a placeholder node (`⟨Class⟩`), while recording the \"omitted depth\" and \"main class name\" in edge attributes.|This shortens paths, retains semantic intent, and focuses on high-level dependency structures.|\n|**(b) Type-Context Nodes**|We add a `Type-Context` node layer to each `expr` tree, summarizing its upstream type-class constraints.|This explicitly provides contextual features, differentiating structures with distinct rings/modules.|\n\n\nRegarding **GNN-based encodings**, we consider this a promising future direction. While our method effectively captures structural information, GNNs could learn deeper graph structures, like Lean's implicit type compatibility graph. Integrating GNNs could involve learning richer, structure-aware node embeddings or modeling implicit type/concept dependency graphs. This combined approach could boost performance and potentially achieve the reviewer's target of \"improving Recall@1 from <20% to >40%.\"\n\nIt's also crucial to note the **theoretical equivalence between GNNs and the Weisfeiler-Lehman (WL) test**. As demonstrated by Xu et al. (2018)[1], certain GNN architectures are provably as powerful as the WL graph isomorphism test, which underpins our WL kernel. This implies that effective handling of WL principles remains foundational even when incorporating advanced GNNs.\n\n---\n\n# Q2: Automated Optimization of Fusion Weights\nWe agree that the current manual tuning of fusion weights (Eq. 2: $sim_{enhanced} = \\alpha ⋅ sim_{cos} + \\beta ⋅ sim_{TEDS} + \\gamma ⋅ sim_{Jaccard} + \\delta ⋅ sim_{CM}$​) is a limitation that can impact generality. For this research stage, manual adjustment facilitated a detailed analysis of each similarity measure's independent contribution and combined effect, crucial for our ablation studies and understanding the method's internal mechanisms.\n\nWe highly recognize the necessity of an **automated optimization mechanism** and consider it a significant future research direction. Introducing data-driven methods—such as grid search, random search, Bayesian optimization on a validation set, or even more advanced reinforcement learning strategies—would allow the model to adaptively learn optimal weight combinations. This would significantly enhance its generalizability and practical utility across different theorem libraries or specific mathematical domains, marking a critical step toward improving our framework's robustness and ease of use.\n\n---\n\n# Q3: Integrating Type-Checking Information into TED's Cost Function\n\nWe appreciate the suggestion to integrate type information to enhance retrieval effectiveness, particularly given Lean4's dependent type system where traditional structural TED may miss subtle type differences crucial for theorem application.\n\nTo address this, we propose integrating type information directly into the TED cost function to improve accuracy for theorems with complex type signatures:\n\n- **Type Difference Penalty:** For structurally similar theorems with mismatched type signatures, we can introduce an additional penalty in TED calculations (e.g., larger penalty for `Nat` vs. `Real` types).\n    \n- **Type Constraint Matching:** We can incorporate a **Type Compatibility Metric** to ensure structurally matched theorems also align with type-class constraints (e.g., `Ring`, `Module`).\n    \n- **Type Hierarchy Matching:** A type hierarchy matching metric at each TED layer can allow for disregarding type differences if nodes belong to compatible type hierarchies (e.g., `Type 1` vs. `Type 2`).\n---\n\n# Q4: Scalability of TED for Large Trees\n\nWe acknowledge the $O(N^3)$ computational complexity of Tree Edit Distance (TED) as a potential bottleneck for extremely large mathematical expression trees. However, our framework incorporates built-in mechanisms to effectively reduce TED's overhead, enabling practical handling of larger trees.\n\nOur **mitigation mechanisms** include:\n\n- **Common Subexpression Elimination (CSE):** This significantly reduces tree size by sharing repeated subexpressions, thereby lowering TED input scale.\n    \n- **Two-Stage Filtering Pipeline:** Our initial Weisfeiler-Lehman (WL) kernel coarse-filters the library, ensuring TED calculations are performed only on a small, pre-pruned set of highly relevant trees.\n    \n- **Distance Thresholding/Depth Limits:** We can set thresholds to terminate TED computations early if distance exceeds limits or a certain depth is reached, using WL similarity as a proxy.\n    \n\nWhile these methods effectively mitigate TED's burden, we agree with the reviewer that **hierarchical TED approximation and early pruning strategies** are valuable for further enhancing scalability for extremely large trees. We will pursue these as future research directions, alongside **benchmarking on trees exceeding 1,000 nodes** to validate scalability gains.\n\n---\n\n# **Limitations :**\n\nWe appreciate the reviewer's feedback regarding potential social impact, particularly concerning **safety-critical applications** and **Mathlib4's domain bias**. We fully concur with these concerns and have already acknowledged relevant limitations in **Appendix G** of our paper. We plan to further elaborate on these discussions in the **final version** to ensure comprehensive awareness of potential risks and careful consideration for practical deployment.\n\n1. Risk of Premise Selection Errors in Safety-Critical Applications:\n    \n    In safety-critical applications (e.g., autonomous driving, aerospace verification, medical devices), premise selection errors can lead to faulty reasoning and severe consequences. We've added a discussion on this, emphasizing:\n    \n    - **Cruciality of Correct Premise Selection:** While our framework aims to reduce search space and improve retrieval precision, selecting irrelevant or incorrect premises can mislead the reasoning process, impacting the entire proof chain's validity. For dependent type systems and automated theorem proving in safety-critical systems, premise selection errors could lead to algorithmic mis-verification, affecting system safety and reliability.\n        \n    - **How Our Method Addresses These Risks:** We've implemented **type-matching mechanisms** and **early pruning strategies** to reduce interference from irrelevant premises and prevent erroneous reasoning. In the future, we plan to integrate **trustworthiness evaluation mechanisms** into the framework, offering a tunable confidence threshold (based on query relevance and type match) to ensure only highly confident premises are selected.\n        \n    - **Countermeasures:** In the paper, we will further emphasize applicability to safety-critical applications, particularly in **automated verification tools**, highlighting the **rigor of premise selection** and the **robustness of verification processes**. We also plan to include case studies in the appendix discussing potential risks in safety-critical scenarios and proposing mitigation strategies.\n        \n2. Mathlib4's Domain Bias and Impact on Practical Deployment:\n    \n    We acknowledge that the distribution of theorems within Mathlib4 is not entirely uniform across all mathematical domains. While some areas are extensively developed, others may have fewer theorems.\n\n\tThe reviewer specifically mentioned an \"over-representation of Natural Number problems.\" We've analyzed our theorem database and found that theorems with names starting with \"Nat.\" constitute approximately **1.85%** of the total. While this represents a significant number of theorems given the library's size, it does not suggest an overwhelming over-representation that would fundamentally bias our method's overall performance or generalizability across broader mathematical fields.\n\n\tHowever, we recognize that even subtle domain imbalances in large libraries like Mathlib4 can affect a framework's universality in **smaller or less-represented mathematical branches** during practical deployment. For instance, our framework might perform exceptionally well in areas with dense theorem coverage but less effectively in more niche or data-scarce domains like certain advanced topological or analytical concepts, simply due to the availability of comparable examples.\n\n\tTo address these potential implications and enhance the framework's robustness across diverse domains, we plan to implement the following improvements:\n\n\t- **Expanded Test Set:** We'll broaden our evaluation by including more diverse data from various mathematical domains, particularly those that are less extensively covered in Mathlib4, such as topology or advanced number theory. This will allow for a more thorough assessment of our framework's performance beyond the most commonly represented areas.\n    \n\t- **Domain Adjustment Strategies:** For real-world deployment, especially in domains with fewer theorems, we'll explore **domain balancing strategies**. This could involve leveraging techniques like **few-shot learning** or **transfer learning** to help our model adapt effectively to different theorem distributions, thereby improving its performance in underrepresented areas without requiring extensive new annotations.\n---\nReference:\n\n[1] Xu, K., Hu, W., Leskovec, J., & Jegelka, S. (2018). How powerful are graph neural networks?. arXiv preprint arXiv:1810.00826."}, {"review_id": "4YZi8PCoXK", "reviewer": "Reviewer_AB1f", "summary": "The paper proposes a graph-based approach to premise selection for Lean 4. The framework consists of multiple filtering stages. It employs two major steps: the WL kernel for search-space reduction and tree edit distance (TED) for fine-grained retrieval. Experimental results indicate improvements across two test sets and at different iteration levels (@k).", "questions": "Based on the Weaknesses section, I have the following questions:\n- What is the novelty of the proposed framework?\n- How can we efficiently choose hyperparameters?\n- What does each hyperparameter affect?\n- What is the role of $\\sigma$ and how can we choose it?\n\nAnd recommendations:\n- Conduct a similar experiment to Table 5 but for $\\sigma$\n- Add one more paragraph about hyperparameter selection and their effect on the pipeline", "limitations": "The limitations of the work are discussed in the Weaknesses section.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 2, "originality": 2, "strengths_and_weaknesses": "## Strengths\n**The paper is easy to follow.** Definitions appear naturally and are well explained.\n\n**The proposed method can run on consumer‑level hardware**, as it balances precision and speed without relying on heavy computations.\n\n**Experimental results support the main claims.** Improvements are shown across two test sets and various iteration levels.\n\n**The method leverages Lean expression trees directly**, rather than relying on embeddings or other generic encodings, the framework is tailored to graph representations of Lean theorems.\n\n## Weaknesses\n**Concerns regarding novelty.** The presented work does a good job of conveying the choices behind each part of the pipeline; however, all of these methods have been explored before, and some are fundamental to working with graphs. The authors combine these methods, but what is novel about this work specifically? Which part of the pipeline was or is underexplored in the literature?\n\n**Parameter selection is confusing.** The authors present Table 5 with parameter selection results but do not offer guidelines for choosing them. It would be helpful if they explained how each parameter impacts the results (e.g., sensitivity, relevance to the query) rather than just presenting numbers. Moreover, the accuracy differences across these selections are quite small, how do the authors interpret this? They use $(\\alpha, \\beta, \\gamma, \\sigma) = (0.1, 0.3, 0.1, 0.5)$ but fail to explain the rationale behind these values. The choice of parameter $\\sigma$ also seems underexplored.", "was_revised": true, "final_justification": "Overall, I find the tree-based premise-selection approach reasonably novel. With a stronger emphasis on transferability and clearer guidelines for parameter selection, this work has become more compelling in my view. For these reasons, I am inclined to raise my score to 4.\n\nMy recommendations for the authors are:\n- Better highlight the novelty and key contributions\n- Improve the hyperparameter-selection section, especially regarding the choice of $\\sigma$\n- Emphasize the method’s transferability to other languages", "rebuttal": "We appreciate the reviewer's questions regarding the novelty, hyperparameter selection, and the role of specific parameters in our framework.\n\n---\n\n# Q1: Novelty of the Proposed Framework\n\nWe appreciate the reviewer's rigorous assessment of our work's depth and novelty. Our method's complexity is precisely what enables us to address the significant and long-standing challenge of efficient and accurate premise selection in theorem proving. The core innovation and \"intelligence\" of our method lie in its **deep mining and systematic utilization of mathematical expression structural information**—an area largely underexplored by current semantic embedding approaches.\n\nOur novelty stems from developing a novel framework that applies carefully designed and customized structural analysis tools to create an unprecedentedly efficient and accurate system for complex Lean4 expression tree structures. Specifically:\n\n- **Unique Utilization of Lean Expr Tree Structures:** Our method fundamentally revolves around the **intrinsic structure of Lean Expr trees**. Unlike generic text or simple graphs, Lean Expr naturally encodes binding relationships, local contexts, and de Bruijn indices, harboring **fine-grained structural features far beyond pure semantic embeddings**. Prior work in premise selection rarely leveraged these complex Lean Expr tree characteristics to such depth. Our framework systematically extracts and quantifies this information, addressing the fundamental limitation of existing embedding methods in distinguishing subtle structural differences.\n    \n- **First-of-its-Kind \"Structural Similarity Spectrum\":** We are the first to **customize and apply CSE (Common Subexpression Elimination) normalization, WL kernel encoding, and TED (Tree Edit Distance) re-ranking specifically to Lean expression trees**. This innovative integration organically unifies \"syntactic redundancy resolution\" (via CSE), \"global isomorphism approximation\" (via WL kernel encoding), and \"local editing cost\" (via TED re-ranking) into a **coarse-to-fine \"structural similarity spectrum.\"** This multi-layered, macro-to-micro structural similarity analysis approach is novel within the existing literature.\n    \n- **Hierarchical and Adaptive \"Unifying Insight\":** We are not merely aggregating metrics. Instead, we've meticulously designed a **phased, adaptive framework** where various structural similarity measures (e.g., WL kernel for coarse screening, TED for fine-grained matching, Const Jaccard for constant semantic overlap, Collapse-Match for pattern alignment) **synergistically interact**. This hierarchical, synergistic utilization of structural information to achieve optimal efficiency and precision **is precisely our method's core \"unifying insight.\"** It clearly demonstrates how structural insights can overcome existing methodological bottlenecks.\n    \n- **Integration of Engineering Practice and Theoretical Innovation:** We concur that our method possesses strong engineering practicality, which we consider a core value. In formal verification—a highly applied domain—the ability to **ingeniously apply theoretical tools of structural analysis** (e.g., graph kernels, tree edit distance) to solve real, large-scale, and previously intractable problems, and to validate its superior performance on extensive, real-world libraries like Mathlib4, represents a significant **applied innovation and methodological breakthrough**. We effectively bridge the gap between structural analysis theory and formal verification practice, demonstrating the immense potential of such deep, structure-based mining in complex practical systems.\n    \n\nIn conclusion, the core strength and novelty of our method lie in its **deep customization, systematic utilization, and multi-dimensional fusion of Lean expression tree structures**. We firmly believe that this sophisticated handling of the intrinsic structural information of formal mathematical language constitutes a significant advancement in the field of premise selection.\n\n---\n\n# Q2: Hyperparameter Selection and Their Effects\n\nOur framework includes several hyperparameters, each affecting different stages and aspects of the premise selection process. Their roles and selection considerations are detailed below:\n\n|Hyperparameter Name|Stage/Function|Description & How It Affects Results|\n|---|---|---|\n|`h`|WL Kernel|**WL kernel iterations:** Determines the depth of neighborhood information aggregation. Larger `h` captures more global structural features but might increase computational cost or lead to \"oversmoothing.\" Selection balances efficiency and information capture.|\n|α,β,γ,δ|Adaptive Fusion|**Enhanced hybrid similarity weights:** Control the relative importance of simcos​, simTEDS​, Jaccard similarity (simJaccard​), and Collapse-Match similarity (simCM​) in the final enhanced similarity (simenhanced​). Sums to 1. Dynamically adjusted to optimize retrieval performance, balancing contributions of different metrics.|\n|σ |TEDS Operation Costs|**Simple node operation scaling factor:** For insertion/deletion operations involving simple nodes (e.g., BVar, FVar, MVar, Sort, Const), their costs are scaled by σ∈[0,1]. This makes modifications to simple nodes less costly than complex structures, allowing TED to better reflect core logical structure similarity. (See Q4 for more details)|\n\n---\n\n# Q3: Efficient Hyperparameter Selection\n\nTo efficiently select hyperparameters, we employ a multi-faceted approach:\n\n- **Grid Search with Cross-Validation:** We begin with grid search to broadly explore the hyperparameter space, testing various combinations. Cross-validation then evaluates each parameter set's performance, systematically identifying optimal configurations.\n    \n- **Ablation Studies:** To gain deeper insight into each hyperparameter's specific role, we conduct ablation experiments. By individually adjusting hyperparameters and observing their impact on retrieval performance, we quantify their contributions within the framework and gain guidance for fine-tuning.\n\n---\n\n# Q4: Role of σ and Its Selection\n\n**σ (sigma)** is a scaling parameter, ranging from [0,1]. Its role is to adjust the cost of insertion (CI​) or deletion (CD​) operations for **simple nodes** (those with labels like `BVar`, `FVar`, `MVar`, `Sort`, `Const`) during Tree Edit Distance (TED) calculations. Specifically, if a node involved in an insertion or deletion is one of these simple types, its cost is scaled by σ⋅CI​ or σ⋅CD​. For complex nodes, the preset CI​ or CD​ values are used directly.\n\nThis tiered cost structure reflects that operations on simple nodes (with lower costs) typically have a smaller impact on the overall mathematical meaning than modifications to complex expression structures (with higher costs). This allows TED to more precisely capture subtle, logically relevant structural differences between trees.\n\n**How σ is chosen:** As stated in the paper, σ is **finely tuned based on the semantic and structural characteristics of Lean4 expressions**. This implies an empirical selection process—involving experiments on validation sets, ablation studies, or parameter sensitivity analysis—to ensure the TED cost function most accurately reflects the practical structural similarity and logical relevance of Lean4 expressions. The choice of σ is ultimately driven by optimizing TED's alignment with Lean4's semantics.\n\n\n\n#  σ Parameter Analysis\n\nWe conducted a new experiment, similar to Table 5, specifically analyzing σ's impact on retrieval performance. This parameter is crucial for scaling node edit costs within our Tree Edit Distance (TED) calculations, thereby influencing both matching precision and computational efficiency.\n\n|σ Value|Recall@1 (%)|Recall@10 (%)|\n|---|---|---|\n|0.0|62|67|\n|0.2|67|69|\n|0.4|65|69|\n|0.6|65|69|\n|0.8|61|62|\n|1.0|59|62|\n\nThe results show that **optimal performance is achieved at σ=0.2**, yielding the highest Recall@1 and Recall@10. Lower σ values (e.g., 0.0) lead to decreased recall, while higher values (e.g., 0.8, 1.0) cause a notable drop in both recall metrics. This suggests that a moderate penalty for simple node edits (as controlled by σ) is vital for balancing precision and recall, allowing TED to accurately reflect the logical relevance of structural differences in Lean4 expressions.\n\n---\n\n# Hyperparameter Selection and Pipeline Impact\n\nWe agree that clear guidelines for hyperparameter selection and a deeper understanding of their impact on the pipeline are crucial. As detailed in our general rebuttal (Q2), we systematically select hyperparameters using **grid search with cross-validation**, conduct **ablation studies**, and perform **sensitivity analysis**.\n\nWhile Table 5 presents numerical results, we will expand our discussion in the final version to clarify the rationale behind specific parameter choices like (α,β,γ,δ)=(0.1,0.3,0.1,0.5) and how each hyperparameter influences different stages of the pipeline.\n\n**Impact on Overall Performance:** We will use both **ablation studies** and **hyperparameter sensitivity analysis** to further explain how each parameter contributes under varying query conditions. This will elucidate why even seemingly small accuracy differences are significant in a precision-critical domain like formal proof, where slight variations can dictate proof success.\n\n**Guidelines for Optimal Combinations:** Through comprehensive experimentation, we will provide concrete **hyperparameter selection guidelines**, helping readers understand how to choose appropriate parameters for different theorem libraries and query types.\n\n**Comparison of Combinations:** We will include additional tables and figures in the final version to illustrate experimental results for various hyperparameter combinations, further explaining the trade-offs between different parameters and their synergistic effects on retrieval performance."}]

Author rebuttal:

Meta-review: I recommend accepting this paper on tree-based premise selection for Lean4. The authors address a critical bottleneck in interactive theorem proving by effectively leveraging structural information in mathematical expressions through a multi-stage filtering pipeline incorporating the Weisfeiler-Lehman kernel, tree edit distance, and adaptive metric fusion. All four reviewers ultimately recommended acceptance with scores of 4, having their initial concerns about complexity, generalizability, and novelty addressed during rebuttal. Comprehensive evaluation on Mathlib4 demonstrates significant performance improvements over existing tools, with ablation studies validating each component's contribution. This work represents an important advancement in structure-aware premise selection for formal verification systems.
Decision: Accept (poster)