DAPS: Dependency-Aware Premise Selection for Lean 4 Theorem Proving

DAPS improves LLM-based theorem proving by replacing semantic similarity retrieval with dependency-aware selection. By mining 53 Lean Blueprint projects, the method recovers rare, research-level premises that are typically ignored by frequency-skewed retrieval methods.