# LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation

> LEANCONTEXT benchmark reveals that mathematical declarations only improve theorem proving when models train with them, boosting Pass@32 by 7-8% after MC-inclusive training.

- **Source:** [arXiv](https://arxiv.org/abs/2611.08277)
- **Published:** 2026-11-14
- **Permalink:** https://picx.dev/p/KcTffN
- **Whiteboard:** https://picx.dev/p/KcTffN/image

## Summary

## 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

| Split | Targets | Both |
|-------|---------|------|
| Train | 90,879 | 51,628 |
| Valid. | 19,473 | 11,063 |
| Test | 19,474 | 11,064 |
| **Total** | **129,826** | **73,755** |

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 %):**

| Model | Training | C0 | CMath | CEnv | CFull | ΔM\|E | ΔE\|M |
|-------|----------|-----|-------|------|-------|--------|--------|
| LLaDA | C0 | 38.6 | 39.1 | 37.8 | 38.3 | +0.5 | -0.8 |
| LLaDA | CMath | 34.1 | 43.9 | 35.8 | 44.3 | +8.5 | +0.4 |
| LLaDA | CEnv | 34.7 | 35.3 | 44.8 | 45.2 | +0.4 | +9.9 |
| LLaDA | CFull | 31.2 | 40.1 | 41.6 | **48.7** | **+7.1** | +8.6 |
| Llama | C0 | 39.8 | 40.6 | 39.2 | 40.3 | +1.1 | -0.3 |
| Llama | CMath | 34.8 | 44.3 | 37.6 | 44.9 | +7.3 | +0.6 |
| Llama | CEnv | 34.5 | 37.3 | 44.9 | 45.7 | +0.8 | +8.4 |
| Llama | CFull | 32.8 | 41.8 | 41.1 | **49.6** | **+8.5** | +7.8 |

**Pass@k results for CFull-trained checkpoints:**

| Model | View | @1 | @8 | @16 | @32 |
|-------|------|-----|------|-------|-------|
| LLaDA | CEnv | 5.9 | 23.2 | 32.3 | 41.6 |
| LLaDA | CFull | 6.9 | 27.1 | 37.8 | **48.7** |
| Llama | CEnv | 5.9 | 23.1 | 32.0 | 41.1 |
| Llama | CFull | 7.2 | 27.9 | 38.6 | **49.6** |

### Matched Replacement Results (2,000 targets)

| Model | Train | CEnv | Selected | Replaced | Rθ |
|-------|-------|------|----------|----------|------|
| LLaDA | CMath | 35.6 | 44.1 | 37.8 | +6.3 |
| LLaDA | CEnv | 44.5 | 45.0 | 44.3 | +0.7 |
| LLaDA | CFull | 41.3 | 48.4 | 42.4 | **+6.0** |
| Llama | CMath | 37.4 | 44.8 | 39.2 | +5.6 |
| Llama | CEnv | 44.8 | 45.6 | 44.7 | +0.9 |
| Llama | CFull | 40.9 | 49.3 | 42.1 | **+7.2** |

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

| Model | C0 | CMath | CEnv | CFull |
|-------|-----|-------|------|-------|
| DeepSeek-Prover-V1.5-SFT | 20.7 | 26.4 | 25.8 | **30.9** |
| DeepSeek-Prover-V1.5-RL | 22.9 | 28.1 | 27.7 | **32.6** |
| DeepSeek-Prover-V2-7B | 29.4 | 35.6 | 34.8 | **38.9** |
| Goedel-Prover-SFT | 23.6 | 29.1 | 27.4 | **32.2** |
| TheoremLlama | 11.7 | 14.2 | 14.9 | **16.5** |

### Dependency-Priority Selection Results

| Model | Policy | @1 | @32 | Cov. | Tokens |
|-------|--------|-----|------|------|--------|
| LLaDA | Baseline | 5.94 | 43.90 | 47.70 | 696.8 |
| LLaDA | Priority | 6.17 | **45.30** | **72.26** | 701.2 |
| Llama | Baseline | 6.25 | 44.55 | 48.88 | 714.2 |
| Llama | Priority | 6.53 | **46.25** | **73.48** | 719.1 |

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.

---

_Markdown view of https://picx.dev/p/KcTffN, served by PicX — AI-generated visual whiteboard summaries of research papers._