We appreciate the reviewer's questions regarding the novelty, hyperparameter selection, and the role of specific parameters in our framework.

Q1: Novelty of the Proposed Framework

We 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.

Our 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:

• 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.

• 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.

• 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.

• 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.

In 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.

Q2: Hyperparameter Selection and Their Effects

Our framework includes several hyperparameters, each affecting different stages and aspects of the premise selection process. Their roles and selection considerations are detailed below:

Q3: Efficient Hyperparameter Selection

To efficiently select hyperparameters, we employ a multi-faceted approach:

• 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.

• 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.

Q4: Role of σ and Its Selection

σ (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.

This 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.

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.

σ Parameter Analysis

We 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.

The 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.

Hyperparameter Selection and Pipeline Impact

We 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.

While 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.

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.

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.

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.

Q1: Handling Nested Type Structures and GNNs

We 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.

To enhance our explicit tree pipeline and mitigate structural distortion from instance explosion, we should propose:

Regarding 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%."

It'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.

Q2: Automated Optimization of Fusion Weights

We 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.

We 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.

Q3: Integrating Type-Checking Information into TED's Cost Function

We 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.

To address this, we propose integrating type information directly into the TED cost function to improve accuracy for theorems with complex type signatures:

• 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).

• 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).

• 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).

Q4: Scalability of TED for Large Trees

We 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.

Our mitigation mechanisms include:

• Common Subexpression Elimination (CSE): This significantly reduces tree size by sharing repeated subexpressions, thereby lowering TED input scale.

• 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.

• 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.

While 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.

Limitations :

We 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.

1. Risk of Premise Selection Errors in Safety-Critical Applications:

   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:

   • 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.

   • 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.

   • 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.

2. Mathlib4's Domain Bias and Impact on Practical Deployment:

   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.

   The 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.

   However, 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.

   To address these potential implications and enhance the framework's robustness across diverse domains, we plan to implement the following improvements:

   • 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.

   • 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.

Reference:

[1] Xu, K., Hu, W., Leskovec, J., & Jegelka, S. (2018). How powerful are graph neural networks?. arXiv preprint arXiv:1810.00826.

We address each point below, focusing on the method's complexity, effectiveness, performance gains, and its underlying insights.

1. Method Design: Necessity and Synergistic Performance

Our 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.

Performance gains stem not from mere accumulation, but from each component serving a specific, synergistic purpose.

2. Lack of Unifying Insight and Engineering vs. Theoretical Innovation

This 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.

Our 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:

• 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.

• 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.

• 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.

• 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.

Q1: Scalability and Computational Costs in Large Theorem Libraries

We 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.

Here's a table, focusing on the computational time in real-world Lean4 environments for each stage:

Q2: Generalizability, Algorithmic Complexity, and Comparison with Large Neural Networks

1. Generalizability: Applicability Across Systems and Tasks

Despite 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.

2. Necessity of Algorithmic Complexity

Our 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.

The 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.

3. Comparison with Large Neural Networks

While 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.

Current 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.

Our 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.

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.

Finally, 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.

Reference:

[1] Xu, K., Hu, W., Leskovec, J., & Jegelka, S. (2018). How powerful are graph neural networks?. arXiv preprint arXiv:1810.00826.

We appreciate the reviewer's insightful questions regarding experimental details, baseline comparisons, algorithmic performance, and generalizability. We address each point below.

Q1: Experimental Details and Baseline Fairness

In 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.

Q2: Baselines and Deep Learning Methods

1. 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.

2. Retraining or Fine-tuning on Our Dataset:

   • 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.

   • 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.

Q3: Baseline Performance and Significant Differences

The fundamental reason for the performance disparity lies in the baselines' failure to explicitly leverage the structural information of Lean expressions.

• 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.

• 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.

Our 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.

Illustrative Misidentification Case:

Consider 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).

Q4: Comparison with Deep Learning and GNNs

1. 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.

2. 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.

3. 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.

4. Orthogonality and Potential Complementarity: We do not view TED + WL and GNNs as mutually exclusive; rather, they are highly complementary:

   • Feature Engineering: WL fingerprints and TED edit sequences can serve as high-quality structural features input to GNNs, alleviating their purely data-driven burden.

   • 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.

   • 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.

Q5: Method Specialization vs. Generalizability

1. 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.

2. Language Agnosticism of Core Technologies:

   • Expression Tree Representation: Any formal language capable of deriving an Abstract Syntax Tree (AST) can be mapped to a unified node-edge topology.

   • CSE Simplification: Common Subexpression Elimination relies on tree isomorphism and doesn't involve language-specific syntax.

   • Multi-Stage Filtering Pipeline: The WL kernel coarse-screening + TED fine-ranking steps depend solely on node labels and structure, not Lean-specific semantics.

     Therefore, the methodology itself is decoupled from the specific language; the key is obtaining a reliable tree-like structure.

3. Implementation Path for Migration to Other Systems:

   • 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.

   • 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.

4. Scenarios Where Tree Structures Are Not Directly Accessible:

   • 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.

   • 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.

Reference:

[1] Xu, K., Hu, W., Leskovec, J., & Jegelka, S. (2018). How powerful are graph neural networks?. arXiv preprint arXiv:1810.00826.