Directed Multi-Relational GCNs for Premise Selection in Lean

Premise selection is a central bottleneck for interactive theorem proving over large formal libraries. Semantic similarity can miss syntactic roles that govern premise applicability, while Lean elaboration can give similar expressions different tree representations through implicit arguments and typeclass evidence. We present R-DGCN, which learns from expression graphs designed to reduce this variation while retaining role distinctions. Retrieval preprocessing reduces recurring expression-tree variation. Typed edges encode constructor-field roles, and paired reverse edges expose subterms to their surrounding context. A relation-specific graph convolutional encoder combines mean and attention pooling to capture global structure and emphasize informative nodes in shared query–theorem embeddings. Precomputed theorem embeddings support retrieval, followed by directed collapse-match (CM) reranking that refines learned similarity using explicit structural coverage. Retrieval comparisons show complementary benefits from learned and structural scores, with recall gains most consistent at larger retrieval cutoffs. Precomputed theorem embeddings enable low online retrieval latency.