HammerRank: Symbolic Learning-to-Rank Premise Selection for the Lean Hammer

Premise selection, the choice of the few dozen library lemmas a hammer may use, largely determines what Lean 4's hammer can prove; the state of the art, LeanPremise, is a neural retriever trained on GPUs. We present HammerRank, a premise selector built entirely from symbolic signals. Candidates come from nearest-neighbour votes over past proofs, symbol overlap on the exact elaborated constants of each statement, usage priors and file locality; a gradient-boosted learning-to-rank model then orders them with 36 features. It contains no neural network and, from extracted proof data, retrains in about forty minutes on a laptop. On the LeanHammer benchmark, HammerRank proves 33.3% of held-out Mathlib theorems, against 31.9% for LeanPremise and 23.4% for the no-learning baseline MePo; the two learned selectors fail on different theorems, and running both, one hammer run each at twice the budget, proves 37.1%. Ablations on offline recall attribute the gain to exact elaborated symbols (+4 points over pretty-printed tokens) and the learned reranker (+20 over raw neighbour votes), while further symbolic signals add little. A symbolic machine-learning selector thus matches the neural state of the art on this benchmark, while trailing it by eight points of offline recall, with under an hour of laptop retraining in place of GPU-days.