LeanContext separates two kinds of input that a model can receive when writing a Lean proof. Hang Zhang and colleagues introduce the benchmark in a November 5 arXiv preprint, using 129,826 whole-proof generation problems to see which resources help and when.
What counts as proof context
The benchmark calls selected, complete mathematical declarations that precede the target mathematical context. Other selected local source commands form environment context. That separation gives the authors a way to compare useful declarations against comparable alternatives while keeping the target proof problem and its original verification environment fixed.
The team constructs four aligned views of each problem to evaluate Lean proof generation. The crossed design varies the material models saw during training and the material they receive during inference. This matters because a resource can be useful to a model trained to use it even if a different checkpoint gets less from the same input.
What improved Lean proof generation
Both diffusion-based and autoregressive models gained more from the selected declarations when their training included mathematical context. The paper then audits final inputs for omitted declarations used by target proofs and studies a policy that prioritizes target dependencies.
On 2,000 targets, prioritizing dependencies improved Pass@32 by 1.40 percentage points for LLaDA and 1.70 for Llama. The study holds checkpoints and inference budgets fixed, and the selection method operates without seeing the reference proof. The result concerns the fraction of targets solved within the evaluated attempt budget.
What the average improvement leaves open
The change did not help every target. The authors report that LLaDA gained 76 solved targets and lost 48, while Llama gained 88 and lost 54. This mix matters for researchers choosing how to allocate limited input space. An evaluation can record which proofs become easier or harder alongside the aggregate score.
Comments