aclanthology.orgSource publication:
Loading content…
In Lean 4 theorem proving that depends on project context, failed proofs used to be discarded as a final filter result, and independent sampling restarted later attempts nearly from scratch. This search framework draws one candidate each from a general-purpose reasoning model and a Lean-specialized prover, uses compiler errors in a pairwise comparison to pick the current-best proof, accepts a revision only when the comparison judges it better, and resamples when refinement stagnates. On seven real Lean 4 projects from miniCTX-v2, within the pass@32 budget it improves average pass rate by 12.8 percentage points over the two base models' average pass@32 while cutting LLM calls by 21.9%.
Failed proofs are no longer discarded but become starting points for later search: the system keeps a single current-best proof state, refines around it, and switches starting point when it stagnates. Independent sampling treated the compiler as a final filter, counting only whether any of k candidates verifies, so failed proofs were dropped even when they held a project-specific lemma or a nearly correct tactic sequence. On seven real Lean 4 projects from miniCTX-v2, within the pass@32 budget the method improves average pass rate by 12.8 percentage points over the two base models' average pass@32 while reducing LLM calls by 21.9%.
Exploration draws one candidate from each of two complementary models, one better at long project context and one better at Lean syntax and tactics. Repeated sampling from a single model tends to repeat the same kind of error, whereas the two models fail in different ways and give more diverse starting points. Across 391 comparisons where both models produced a candidate, GPT-5-mini was selected 58.6% of the time and DeepSeek-Prover-V2 still 41.4%, indicating the specialist supplies complementary candidates.
A revision no longer overwrites the current proof unconditionally; it is proposed then accepted, with an LLM judge comparing old and new proofs together with their compiler errors and replacing only when the new one looks more likely to succeed. Standard iterative refinement treats every revision as a state update, so a revision that fixes one error while introducing another accumulates over rounds and pushes the search away from a correct proof. On successful refinement trajectories about 50.4% of refinement proposals are rejected on average, and among solved trajectories whose final verification follows a comparison step, 39.5% verify after the judge keeps the existing current-best proof rather than the newest proposal.
When N consecutive revisions are rejected and the current path stops improving, the system returns to exploration and draws fresh candidates from both models rather than only the model that produced the stagnated proof. Pairwise comparison preserves promising proof states but cannot escape a fundamentally bad proof strategy, and resampling is the fallback for that case. On mathlib-valid, a stagnation threshold of K/4 reaches 60.00% pass rate at 24.42 average LLM calls, better than the K/12, K/6, K/3 and K/2 settings.
The demonstrated setting is the test split of seven real Lean 4 projects from miniCTX-v2 and 84 theorems from RLMEval-FLT3 in the easy setting with all project lemmas available; the method generates, refines and compares complete proofs at the whole-proof level and does not explicitly search over tactic-level proof states.
The comparison is made by an LLM judge, which the source notes is flexible but may not always reflect true proof progress; the framework uses pretrained models at inference time and does not train models through multi-turn Lean feedback; main results are reported from a single run for each method and budget.