Reproduce “LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Hang Zhang, Qihao Ye, Litong Liu, Yunbei Zhang, Yugyung Lee, Yue Zhou, Bowen Liu, Emily First and 2 more
LeanContext tests how mathematical declarations affect proof generation and whether training changes usefulness. It compares selected declarations with matched replacements while holding targets, environment, checkpoints, and verification conditions fixed. After context-rich training, selected declarations improve Pass@32 by 6.0 points for LLaDA and 7.2 for Llama, versus 0.7 and 0.9 after environment-only training; this reference-assisted result compares declaration sets, not individual declarations.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.