Summary (Overview)

• LEANCONTEXT is a benchmark of 129,826 Lean whole-proof generation problems from a fixed Mathlib4 snapshot, designed to disentangle Mathematical Context (MC) (complete mathematical declarations) from Environment Context (EC) (accompanying source commands like variable, namespace, open, notation).
• Four aligned input views (C0, CMath, CEnv, CFull) support crossed training and inference evaluations with shared targets and original Lean verification environments, enabling controlled comparisons of declaration visibility.
• For both diffusion-based (LLaDA) and autoregressive-based (Llama) models, adding MC to EC improves Pass@32 by 7.1% and 8.5% when training includes MC, versus only 0.4% and 0.8% after EC-only training.
• Matched replacement experiments show selected declarations outperform comparable alternatives by a larger margin (6.0% and 7.2%) when training includes MC, versus 0.7% and 0.9% after EC-only training.
• Final-input dependency audits identify omitted declarations; prioritizing these dependencies improves Pass@32 by 1.40% and 1.70% for LLaDA and Llama on 2,000 targets, without access to target reference proofs.

Introduction and Theoretical Foundation

Neural theorem proving increasingly relies on retrieved premises and project source context to generate proofs, reflecting the cumulative nature of formal mathematics where definitions introduce objects and subsequent lemmas establish properties that later proofs reuse. A proof about a newly defined object may combine its definition, an earlier lemma, and an instance required to apply that lemma.

Existing work has examined various forms of supporting information:

• LeanDojo studies retrieval-augmented proving with accessible premises
• Passport examines identifier representations
• Rango retrieves relevant premises and proof examples
• miniCTX extends evaluation to project source context, analyzing environment information, definitions, lemma statements, proofs, and comments

The key research questions addressed by LEANCONTEXT are:

1. Do target-selected declarations outperform comparable replacements?
2. How does this advantage depend on training when accompanying source commands are held fixed?

The theoretical foundation treats a complete declaration as the resource unit, allowing its identity to be tracked through selection, replacement, and dependency analysis. This enables measuring the advantage of selected content over matched alternatives under identical verification conditions.

Methodology

Task and Context Partition

LEANCONTEXT evaluates whole-proof generation: a model receives a target statement and visible preceding source commands, generating a complete proof without intermediate Lean feedback. Each candidate is verified at the original target location with Lean in the complete original environment.

• MC (Mathematical Context): definitions, lemmas, structures, classes, and instances (statements and bodies retained)
• EC (Environment Context): remaining commands such as variable, namespace, open, and notation

Dataset and Aligned Views

Each target has four views: C0 (neither category), CMath (MC only), CEnv (EC only), and CFull (both). Inputs fit under a 1,024-token limit; other views hide categories without refilling freed space.

Controlled Comparisons

Conditional category gains are defined as:

$$\Delta_{M|E}(\theta) = S_{\theta}(\mathrm{CFull}) - S_{\theta}(\mathrm{CEnv}) \tag{1}$$ $$\Delta_{E|M}(\theta) = S_{\theta}(\mathrm{CFull}) - S_{\theta}(\mathrm{CMath}) \tag{2}$$

Matched replacement tests the selected-content advantage:

$$R_{\theta} = S_{\theta}(E + M_{\mathrm{sel}}) - S_{\theta}(E + M_{\mathrm{rep}}) \tag{3}$$

where $M_{\mathrm{sel}}$ and $M_{\mathrm{rep}}$ are selected and replacement MC, and $E$ is the shared EC.

Dependency Diagnostics

Coverage of target dependencies in final inputs:

$$\mathrm{Coverage}_{T}(i) = |D_{i}^{T} \cap V_{i}^{M}| / |D_{i}^{T}| \tag{4}$$

where $D_{i}^{T}$ is the set of eligible preceding local MC commands referenced by the target's elaborated type, and $V_{i}^{M}$ contains visible MC commands in the final serialized input.

Empirical Validation / Results

Training-Dependent Declaration Benefits

Crossed training and inference views on 11,064 targets (Pass@32 %):

Pass@k results for CFull-trained checkpoints:

Matched Replacement Results (2,000 targets)

Released Lean Provers (Pass@32, no additional training)

Dependency-Priority Selection Results

The priority policy gains 76 solved targets and loses 48 for LLaDA (88 gained, 54 lost for Llama), with mean input growth below five tokens.

Theoretical and Practical Implications

• Declaration selection and training are coupled: The advantage of selected declarations over replacements is substantially larger when models are trained with MC, demonstrating that context value depends on training exposure.
• Both context categories matter: After combined-context training, both MC and EC provide additional value, suggesting a complementary relationship between mathematical resources and environment commands.
• Representation responses correlate with training: Checkpoints trained with a context category show larger representation changes (measured by 1 − CKA) when that category is supplied, providing a mechanistic view of how training shapes context sensitivity.
• Coverage analysis reveals opportunities: Among targets with computable coverage, 58.26% (LLaDA) and 57.76% (Llama) lack complete dependency coverage in final inputs, identifying a concrete avenue for selection improvement.
• Selection involves tradeoffs: The dependency-priority policy improves overall success but reduces coverage of additional reference-proof dependencies, highlighting the need to balance competing resource demands within limited context budgets.

Conclusion

LEANCONTEXT provides a benchmark of 129,826 Lean whole-proof generation problems that organizes complete mathematical declarations as MC and accompanying source commands as EC. Key findings include:

1. Checkpoints trained with MC show larger conditional gains from supplied declarations (7.1% and 8.5% for LLaDA and Llama) compared to EC-only training (0.4% and 0.8%).
2. Selected declarations show larger advantages over matched replacements after MC-inclusive training (6.0% and 7.2%) versus EC-only training (0.7% and 0.9%).
3. Dependency-priority selection improves Pass@32 by 1.40% and 1.70% for LLaDA and Llama without accessing target reference proofs, while revealing resource tradeoffs.

Limitations include the use of a fixed Mathlib4 snapshot, 1,024-token budgets, and focus on complete source commands. Future work could explore compact target- and prover-specific context subsets, adaptive selection policies, joint adaptation of selection and prover training, and analysis of generation trajectories to explain how declaration benefits develop during proof construction.