# Combining Textual and Structural Information for Premise Selection in Lean

arXiv: https://arxiv.org/abs/2510.23637 · HTML: https://mlsanity.com/paper/2510.23637/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 14 references that are in the map.
- First posted on arXiv 24 Oct 2025.

## Builds on (most cited first, 10 of 10)

- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [Optuna: A Next-generation Hyperparameter Optimization Framework](https://mlsanity.com/paper/1907.10902/) (2019)
- [Modeling Relational Data with Graph Convolutional Networks](https://mlsanity.com/paper/1703.06103/) (2017)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Exponential Moving Average of Weights in Deep Learning: Dynamics and Benefits](https://mlsanity.com/paper/2411.18704/) (2024)
- [InfoNCE: Identifying the Gap Between Theory and Practice](https://mlsanity.com/paper/2407.00143/) (2024)
- [MLFMF: Data Sets for Machine Learning for Mathematical Formalization](https://mlsanity.com/paper/2310.16005/) (2023)
- [On the Initialization of Graph Neural Networks](https://mlsanity.com/paper/2312.02622/) (2023)

## Built on by (most cited first, 1 of 1)

- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)

## Abstract (arXiv)

Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state-premise and premise-premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25% across standard retrieval metrics. These results suggest that relational information is beneficial for premise selection.