TY  - RPRT
TI  - LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation
AU  - Hang Zhang
AU  - Qihao Ye
AU  - Litong Liu
AU  - Yunbei Zhang
AU  - Yugyung Lee
AU  - Yue Zhou
AU  - Bowen Liu
AU  - Emily First
AU  - Cheng Han
AU  - Qiao Zhuang
PY  - 2026
UR  - https://arxiv.org/abs/2611.08277
ID  - 2611.08277
ER  -