LeanContext：在 Lean 完整证明生成中解耦数学资源与局部形式化上下文

神经定理证明越来越多地使用检索到的前提和项目上下文来辅助证明生成。评估这些资源需要衡量针对目标选取的声明相较于可比替代项的优势，以及这种优势如何取决于训练。我们提出 LeanContext，这是一个包含 129,826 个 Lean 完整证明生成问题的基准，用于研究这些问题。我们将选取的、位于目标之前的完整数学声明归为数学上下文（MC），并将其余选取的局部源代码命令归为环境上下文（EC）。四种对齐的输入视图支持训练与推理的交叉评估，各评估共享相同的目标和原始 Lean 验证环境。对于基于扩散和基于自回归的模型，当训练包含 MC 时，所选声明相较于可比替代项的优势更大。对最终输入的审查识别出了目标引用但输入中遗漏的声明。在 2,000 个目标上，优先选取这些依赖项使 LLaDA 和 Llama 的 Pass@32 分别提高了 1.40% 和 1.70%。该选择实验在无法访问目标参考证明的条件下进行，并保持模型检查点、EC 和推理预算不变。代码和数据集已发布于 https://github.com/haaaardcvZ/LeanContext。