---
title: "LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2611.08277v1"
permalink: "https://feed.astralor.com/items/itm_5aa76bc961fc6477dd9144cc"
published: "2026-11-05T16:44:59.000Z"
score: 58
channel: "tech"
tags: ["推理效率","LeanContext","Disentangling Mathematical Resources","Local Formal Context","Lean Whole-Proof Generation","Neural","Evaluating"]
---

# LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation

## At a glance

Neural theorem proving increasingly uses retrieved premises and project context to support proof generation. Evaluating these resources requires measuring the advantage of target-selected declarations over comparable al…

## Key points

- Neural theorem proving increasingly uses retrieved premises and project context to support proof generation.
- Evaluating these resources requires measuring the advantage of target-selected declarations over comparable alternatives and how this advantage depends on training.
- We introduce LeanContext, a benchmark of 129,826 Lean whole-proof generation problems, to investigate these questions.

## Full text

Neural theorem proving increasingly uses retrieved premises and project context to support proof generation. Evaluating these resources requires measuring the advantage of target-selected declarations over comparable alternatives and how this advantage depends on training. We introduce LeanContext, a benchmark of 129,826 Lean whole-proof generation problems, to investigate these questions. We group selected complete preceding mathematical declarations as Mathematical Context (MC) and the remaining selected local source commands as Environment Context (EC). Four aligned input views support crossed training and inference evaluations with shared targets and original Lean verification environments. For both diffusion- and autoregressive-based models, selected declarations outperform comparable alternatives by a larger margin when training includes MC. Final-input audits identify omitted declarations referenced by the target. Prioritizing these dependencies improves Pass@32 by 1.40% and 1.70% for LLaDA and Llama, respectively, on 2,000 targets. The selection experiment operates without access to target reference proofs and holds checkpoints, EC, and inference budgets constant. The code and dataset are available at https://github.com/haaaardcvZ/LeanContext.

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_5aa76bc961fc6477dd9144cc