Automated theorem proving in real-world software projects is a substantially harder problem than it might appear from benchmark results. Most neural theorem provers are evaluated on self-contained problems where the proof depends only on standard library lemmas. Project-level Lean 4 code is different: proofs routinely depend on local definitions, project-specific naming conventions, and lemmas scattered across thousands of lines of surrounding context. This paper, available on arXiv, addresses this gap directly by proposing a search framework that treats the Lean compiler not as a final binary judge but as a continuous source of structured feedback for guiding iterative proof construction.
The broader motivation connects to a well-documented tension in LLM-based code and proof generation. Independent sampling, measured by pass@k, discards all information from failed attempts. When a proof is 90% correct but fails on a single tactic, that partial progress is simply thrown away. In project-level theorem proving, where a model may correctly identify a relevant project-specific lemma but mis-apply it, this is particularly wasteful. Compiler-guided refinement offers an obvious remedy, but prior work has shown that iterative self-correction is not reliably beneficial: revisions can introduce new errors, and some starting proofs are so far from correct that no amount of refinement helps.
Key Contributions
The paper makes three concrete contributions worth separating out:
- A dual-model exploration strategy that draws candidates from a Lean-specialised prover (DeepSeek-Prover-V2-7B) and a general-purpose reasoning model (GPT-5-mini). The intuition is that these models fail in complementary ways: the specialist produces precise tactic sequences but underuses long project context, while the generalist handles context better but more often produces ill-typed tactics.
- A current-best refinement protocol with compiler-grounded pairwise comparison. Rather than always refining the most recent proof attempt, the system maintains a single best proof state and only replaces it when a revised candidate is judged superior. This guards against the common failure mode where a revision fixes one error while degrading previously correct subgoals.
- Stagnation-triggered resampling: when refinement stops making progress for N consecutive steps, the system returns to exploration and draws fresh candidates from both models. This provides a principled escape from stuck trajectories without committing to unlimited refinement budgets.
The pairwise comparison mechanism is worth understanding carefully. Rather than using a scalar score, the system asks a model to compare two proof candidates and select the more promising one. This is grounded in compiler output, meaning the comparison has access to structured error messages rather than just surface-level text. The same comparison mechanism controls all three decision points: initial candidate selection, refinement acceptance, and post-resampling selection.
Methodology and Experimental Setup
Evaluation uses seven real-world Lean 4 projects from miniCTX-v2, which is a more demanding benchmark than library-based alternatives precisely because it requires project-specific context. A secondary evaluation on RLMEval-FLT3 tests the framework when informal proof sketches are available as additional input.
The baselines are sensible: single-model pass@k for each model separately, and a dual-model baseline that simply pools independent samples from both models without any refinement or search control. This last baseline is important because it isolates the contribution of the search procedure from the contribution of model diversity alone.
The refinement budget K is varied across {8, 12, 16, 20, 24, 28} calls, with stagnation threshold set to ceil(K/4). Plotting pass rate against average LLM calls per theorem rather than against a fixed budget is the right way to present this kind of result, since it makes the efficiency-effectiveness tradeoff explicit rather than hiding it behind a single operating point.
Results and What They Actually Show
The headline numbers are a 12.8 percentage point improvement in average pass rate over the better of the two base models at a pass@32 budget, with 21.9% fewer LLM calls. This is a meaningful result, not a marginal one. A few aspects of the detailed results are worth highlighting:
- Dual-model generation alone already outperforms either single model, confirming that the two models do fail in genuinely complementary ways rather than being interchangeable.
- At higher call budgets, the dual-model generation baseline plateaus (the paper notes Carleson flattening at 0.50 after roughly 16 calls), while the full framework continues to improve. This is the clearest evidence that refinement is adding value beyond what diversity alone provides.
- The model selection rate analysis (Table 5) shows GPT-5-mini is selected in 58.6% of pairwise comparisons overall, but DeepSeek is preferred in over 40% of cases and dominates on some projects. This validates the dual-model design: neither model is uniformly better.
- On RLMEval-FLT3, the framework reaches 39.3% pass rate at 13.5 average calls per theorem, exceeding both single-model pass@32 results. The availability of informal proofs as additional context appears to amplify the generalist model's advantage.
- The robustness check with Gemini-2.5-Flash replacing GPT-5-mini is reassuring. The framework is not tuned to a specific model pair.
Table 6 provides a useful breakdown of which component actually proves each theorem. The generalist contributes substantially at initial generation (8.71 average theorems proved), while refinement from both models adds meaningful incremental coverage. Resampling contributes relatively little in absolute terms, which suggests either that the stagnation threshold is well-calibrated or that the cases where resampling would help are genuinely hard.
Limitations and Open Questions
The authors are candid about the main limitation: the framework operates entirely at inference time with pretrained models and does not learn from the multi-turn interaction with Lean. A system trained with reinforcement learning on compiler feedback would likely do better still, and the search procedure described here could serve as a data generation mechanism for such training.
There are a few questions the paper does not fully address. The pairwise comparison mechanism is central to the whole framework, but its reliability is not characterised independently. If the judge model makes poor comparisons, the search could systematically preserve worse proof states. The selection rate analysis is suggestive but does not directly measure comparison accuracy against ground truth. A calibration study would strengthen confidence in this component.
The computational cost of the pairwise comparison calls is also not broken out separately from generation and refinement calls. If comparison calls are cheap relative to generation, this is a minor concern; if not, the reported efficiency gains may be somewhat optimistic in practice.
Finally, the framework is evaluated on a fixed set of seven projects. Project-level Lean proving is heterogeneous enough that results on a broader set of projects, or on projects from different mathematical domains, would be valuable for understanding generalisability.
Despite these caveats, this is a well-executed paper that makes a clear methodological contribution. The core insight, that compiler feedback should guide search control rather than just proof repair, is simple but underexplored in the neural theorem proving literature. The results are strong enough to suggest this direction is worth pursuing further, particularly in combination with training-time methods. The code is publicly available at github.com/joeliuz6/lean_proof_search.