Organizations: University of Missouri-Kansas City · Columbia University · Monash University Malaysia · Tulane University · LLM Core and Agentic AI, Capital One · Rutgers University
Neural theorem proving increasingly uses retrieved premises and project context to support proof generation. Evaluating these resources requires measuring the advantage of target-selected declarations over comparable alternatives and how this advantage depends on training. We introduce LeanContext, a benchmark of 129,826 Lean whole-proof generation problems, to investigate these questions. We group selected complete preceding mathematical declarations as Mathematical Context (MC) and the remaining selected local source commands as Environment Context (EC). Four aligned input views support crossed training and inference evaluations with shared targets and original Lean verification environments. For both diffusion- and autoregressive-based models, selected declarations outperform comparable alternatives by a larger margin when training includes MC. Final-input audits identify omitted declarations referenced by the target. Prioritizing these dependencies improves Pass@32 by 1.40% and 1.70% for LLaDA and Llama, respectively, on 2,000 targets. The selection experiment operates without access to target reference proofs and holds checkpoints, EC, and inference budgets constant. The code and dataset are available at https://github.com/haaaardcvZ/LeanContext.
Figures & tables
Figure 1: Overview of LeanContext . (Left) A complete mathematical declaration (MC) and accompanying source commands (EC) precede a proof target. (Right) Four aligned views support crossed training, inference evaluations, and matched replacement. Input comparisons retain the target and original Lean verification environment. Matched replacement also keeps EC unchanged.
Split
Targets
Both
Train
90,879
51,628
Valid.
19,473
11,063
Test
19,474
11,064
Total
129,826
73,755
Table 1: Dataset statistics. Both counts targets with nonempty selected MC and EC before model-specific budget handling.
Checkpoint
Inference view / Pass@32 (%)
Conditional gain (%)
Model
Training
C0
CMath
CEnv
CFull
ΔM∣E
ΔE∣M
LLaDA NeurIPS’25
C0
38.6
39.1
37.8
38.3
+0.5
-0.8
CMath
34.1
43.9
35.8
44.3
+8.5
+0.4
CEnv
34.7
35.3
44.8
45.2
+0.4
+9.9
CFull
31.2
40.1
41.6
48.7
+7.1
+8.6
Llama arXiv’24
C0
39.8
40.6
39.2
40.3
+1.1
-0.3
Table 2: Crossed training and inference views on 11,064 targets. Inference columns report Pass@32. Each row corresponds to one checkpoint. Conditional gains follow Eqs. ( 1 ) and ( 2 ). Bold highlights the MC-gain comparison between CEnv and CFull training.
Model
View
@1
@8
@16
@32
LLaDA NeurIPS’25
CEnv
5.9
23.2
32.3
41.6
CFull
6.9
27.1
37.8
48.7
Llama arXiv’24
CEnv
5.9
23.1
32.0
41.1
CFull
7.2
27.9
38.6
49.6
Table 3: Pass@ k on the main 11,064 targets for CFull -trained checkpoints , estimated from the same 32 candidate outcomes. Bold marks the higher score within each model and sampling budget.
Model
C0
CMath
CEnv
CFull
DeepSeek-Prover-V1.5-SFT ICLR’25
20.7
26.4
25.8
30.9
DeepSeek-Prover-V1.5-RL ICLR’25
22.9
28.1
27.7
32.6
DeepSeek-Prover-V2-7B arXiv’25
29.4
35.6
34.8
38.9
Goedel-Prover-SFT COLM’25
23.6
29.1
27.4
32.2
TheoremLlama EMNLP’24
11.7
14.2
14.9
16.5
Table 4: Released Lean provers on the same 11,064 targets. Scores are Pass@32. Each checkpoint is fixed across views, without additional LeanContext training. DeepSeek-Prover-V2-7B uses non-CoT generation. Bold marks the highest score within each checkpoint.
Figure 2: A paired proof-generation case with 32 attempts per view. Both views use the same checkpoint, EC, and verification conditions. A failed CEnv candidate leaves a type mismatch. A verified CFull candidate uses the supplied RightInverse.injective declaration. The right-inverse fact is available in the original Lean environment. These candidates are independently generated under the two input views.
Model
Train
CEnv
Selected
Replaced
Rθ
LLaDA NeurIPS’25
CMath
35.6
44.1
37.8
+6.3
CEnv
44.5
45.0
44.3
+0.7
CFull
41.3
48.4
42.4
+6.0
Llama arXiv’24
CMath
37.4
44.8
39.2
+5.6
CEnv
44.8
45.6
44.7
+0.9
CFull
40.9
49.3
42.1
+7.2
Table 5: Matched replacement on 2,000 targets, reporting Pass@32. Selected and Replaced combine their respective MC with identical EC. Rθ is the selected-content advantage (Eq. ( 3 )). Controls exclude identified target-type and reference-proof dependencies. Bold contrasts CEnv and CFull training.
Figure 3: Block-32 representation dissimilarity on 4,000 shared test targets under reference-proof conditioning. Rows identify backbones, and columns identify training views. Both axes within each panel are inference views. Cells report 1−CKA with a shared color scale. Larger values indicate lower representation similarity.
LLaDA NeurIPS’25
Llama arXiv’24
Coverage
Targets
ΔM∣E
Targets
ΔM∣E
Zero
2,500
+4.00
2,460
+4.88
Partial
2,650
+6.79
2,640
+8.33
Complete
3,690
+7.72
3,730
+9.12
Table 6: Independent final-input coverage evaluation on 11,064 targets. Coverage is computable for 8,840 LLaDA and 8,830 Llama targets. Gains are Pass@32 differences in %, computed before rounding.
Model
Policy
@1
@32
Cov.
Tokens
LLaDA NeurIPS’25
Baseline
5.94
43.90
47.70
696.8
Priority
6.17
45.30
72.26
701.2
Llama arXiv’24
Baseline
6.25
44.55
48.88
714.2
Priority
6.53
46.25
73.48
719.1
Table 7: Dependency-priority selection with a shared candidate pool and frozen EC. Pass@1 and Pass@32 retain all 2,000 targets. Cov. is macro target coverage (%) over 1,568 eligible LLaDA targets and 1,565 eligible Llama targets. Tokens is mean submitted-input length. Bold marks improvements over Baseline.