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 current state of the art, LeanPremise, is a neural retriever trained on GPUs. We present HammerRank, a premise selector built entirely from symbolic signals. Candidates are generated from nearest-neighbour votes over past proofs, symbol overlap on the exact elaborated constants of each statement, usage priors and file locality, and a gradient-boosted learning-to-rank model orders them with 36 features derived from the same sources. The system 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, compared with 31.9% for LeanPremise and 23.4% for the symbolic baseline MePo; the two learned selectors are complementary: running both, one hammer run each, proves 37.1%. Ablations show that exact elaborated symbols and the learned reranker account for the gain, while further symbolic signals add little. A symbolic machine-learning selector thus matches the neural state of the art on this benchmark with under an hour of laptop retraining in place of GPU-days.