DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving

LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas. Existing neural selectors rank candidates by semantic similarity, with three intrinsic limitations: frequency-skewed retrieval, isolated pairwise ranking, and degradation on out-of-distribution queries such as competition problems and informal language. Given that mathematics is structured by dependencies rather than similarities, we restore this signal to both the training data and the model. We conduct the first systematic mining of 53 Lean Blueprint projects, a previously untapped corpus of 3,805 manually curated informal+formal nodes that capture rare, research-level premises absent from Mathlib4. We further pair it with the extraction of comprehensive, typed, multi-level Mathlib4 dependencies. We then introduce DAPS, a dependency-aware premise selector with a structural neighborhood encoder, a group-level contrastive objective, and a Mathlib-then-Blueprint adaptation procedure. DAPS reaches Recall@32 of 89.31 on Mathlib4-Heldout, 11.47 over the strong selector LeanHammer, and holds its lead across out-of-distribution benchmarks. DAPS further improves three general-purpose LLMs on the informal IMO-ProofBench. Dependency graphs, benchmarks, and code are available and will be released under a permissive license upon publication.