GARNET: Graph-Augmented Reranking for Premise Retrieval in Lean

Premise retrieval is a central component of LLM-based theorem proving: a prover must identify useful lemmas from a library containing hundreds of thousands of declarations. Most existing retrievers rely on direct matching with either a natural-language query or a local proof state, ignoring the structural relationships encoded in the library's dependency graph. We propose GARNET, a graph-augmented reranking framework for Lean that expands query- and state-conditioned anchor sets along local dependency neighborhoods and reranks candidates by combining direct retrieval evidence with structural context. On end-to-end retrieval benchmarks, GARNET improves R@20 by over 20 absolute points against strong baselines on Mathlib 4.28 and maintains strong performance on Lean Workbook. When integrated into an LLM-based proving agent for proof-sketch completion on a curated 60-theorem subset of ProofNet-Verified, it achieves $77.7\pm 3.0$% mean single-attempt accuracy and 88.3% pass@5, the highest among all evaluated systems, with a substantial margin over learned state-only retrievers. More broadly, our results show that effective premise retrieval benefits from combining complementary query- and state-conditioned evidence with structural relationships among library declarations.