Extracts typed dependency graphs from Mathlib4 and 53 Lean Blueprint projects to train a premise selector for Lean 4 LLM provers.
Abstract
LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas, because retrieval skews toward popular foundational lemmas, leaving the right premises buried among hundreds of thousands of candidates. 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 curate two underused dependency resources. 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 mean Recall@32 of 89.25 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer), and maintains this lead on two out-of-distribution benchmarks. Further experiments demonstrate that DAPS premises improve theorem proving on miniF2F and IMO-ProofBench. Project page: https://daps-eth.github.io/.
Problem
Neural premise selectors for Lean 4 LLM provers rank candidates by semantic similarity. As a result, retrieval favors popular foundational lemmas, ranks each lemma in isolation rather than as a usable set, and degrades on out-of-distribution queries such as competition problems and informal text.
Approach
The authors build a typed, multi-level dependency DAG from mathlib-4.22.0 with 15 edge categories and 6.5M edges. They also mine 53 Lean Blueprint projects, giving 3,805 informal and formal nodes, and derive four retrieval benchmarks from these resources. DAPS combines a structural neighborhood encoder with a group-level contrastive objective over premise sets. It is trained on Mathlib first, then continually adapted on Blueprint dependencies.
Figure 1 : One dependency graph spanning Mathlib4 (left) and a representative Blueprint project (right). The two resources differ in density and composition. Mathlib4 averages 24 edges per node with strong directional asymmetry across node types, while Blueprint dependencies are much sparser, averaging 1.2, but carry research-level out-of-Mathlib4 declarations and informal L a T e X signals.
Results
DAPS reaches a mean Recall@32 of 89.25 on Mathlib4-Heldout, 11.41 points above LeanHammer, and also leads on the DAPS-Collection and DAPS-Blueprint benchmarks. Supplying DAPS premises improves pass@k on miniF2F with Goedel-Prover-V2 and DeepSeek-Prover-V2, and raises informal proving scores on IMO-ProofBench.
Method
Mathlib4-R
Mathlib4-H
DAPS-Coll.
DAPS-BP
ReProver
36.97
43.48
1.24
32.04
LeanHammer
73.99
77.84
3.19
40.42
Qwen3-Embedding-8B
15.25
9.92
0.36
13.07
DAPS
80.68
89.25
23.53
50.08
Recall@32 (mean over three runs) across the four benchmarks
