We introduce LeanContext, a benchmark comprising 129,826 Lean whole‑proof generation problems, to study how retrieved premises help neural theorem provers. The selected complete preceding mathematical declarations are grouped as Mathematical Context (MC), while the remaining selected local source commands form the Environment Context (EC). Four aligned input views are provided, enabling crossed training and inference evaluations with shared targets and the original Lean verification environment.
Both diffusion‑based and autoregressive models were tested. When training includes MC, the selected declarations outperform comparable alternatives by a larger margin. A final‑input audit reveals declarations referenced by the target but omitted from the input; adding these dependencies raises Pass@32 by 1.40% for LLaDA and 1.70% for Llama on 2,000 targets.
The selection experiment runs without access to target reference proofs and keeps checkpoints, EC, and inference budgets constant. The code and dataset are released at https://github.com/haaaardcvZ/LeanContext.
Review