SkillEvoLean: Mutation-enhanced skill evolution for Lean provers
SkillEvoLean tackles the challenge of improving LLM agents for Lean theorem proving without updating model parameters. The core idea is to evolve natural-language procedural skills through progressive refinement from execution trajectories and, crucially, a mutation operator that perturbs skills in a semantic concept space to escape local optima when all proof attempts fail. This matters because existing skill-evolution methods stagnate on hard theorems where no sampled trajectory succeeds, leaving the solver with no signal for improvement.
The paper offers a well-motivated conceptual framework: it correctly identifies that trajectory-based skill evolution stalls when every proof attempt fails, and proposes a plausible escape route via semantic mutation in an abstract concept space. Unfortunately, the experimental evaluation is almost entirely hypothetical. Multiple table captions and inline notes explicitly state that the reported numbers are planning targets and baseline assumptions, not measured results, yet the abstract presents these same figures as definitive achieved outcomes. This contradiction makes it impossible to trust the empirical claims.
The problem diagnosis is sound: when all trajectories fail, contrasting successful and failed behaviors is impossible, so progressive evolution has no update direction. The proposed Concept-Guided Skill Refinement (CGSR) addresses this by mapping a textual skill to a compact concept set, applying randomized add/remove/replace perturbations, and mapping back to a coherent skill, which preserves syntactic and semantic structure better than raw text mutation. The skill definition as $sk := (\mathcal{M}, \mathcal{R}, \mathcal{E})$ is clean, and the operator pipeline is clearly specified.
The central and disqualifying flaw is that the results are planning targets rather than measurements. Table 3 is labeled a Planning scenario, not measured results with Component ablation targets. Table 4 is labeled Mutation-guidance targets. Table 5 states No token usage, timing, or variability has been measured for this scenario. Section 3.4 notes No standard deviations are assumed; independent runs must supply them. Despite this, the abstract reports concrete success rates and ablation gaps as if they were observed, which makes the empirical claims impossible to substantiate.
The evidence does not support the claims because the evidence is not empirical. All baseline comparisons use provisional targets rather than actual benchmark runs; the paper states Actual resource consumption must be measured under these limits; the present entries are design targets and baseline assumptions. Without measured data, statistical testing, or variance estimates, it is impossible to know whether the reported gaps over Trace2Skill, SkillOpt, or Human Skill are real or simply optimistic projections. The ablation of mutation is labeled a target scenario, not an experiment.
Reproduction is impossible from the manuscript. The paper repeatedly labels its tables as planning targets and explicitly states No token usage, timing, or variability has been measured for this scenario. No code repository is mentioned, prompts are deferred to supplementary material, and the method depends on backbone models and tools such as GPT-5.5 and Claude Code whose exact versions and availability are unclear. The only concrete hyperparameter disclosed is $I_{\max} = 5$, leaving the full evolution protocol underspecified.
Skill evolution offers a promising way to improve large language model agents without updating their parameters, but its use in formal theorem proving remains underexplored. Existing methods mainly target natural-language reasoning, improving skills by analyzing successful and failed trajectories and incrementally revising solving strategies. Although the Lean verifier provides reliable execution feedback, when all sampled trajectories fail, existing skill evolution methods lack successful trajectories from which to infer effective update directions. Furthermore, these methods also focus mainly on the root instruction file, thus underexploring the evolution of reference knowledge including mathematical concepts and proving techniques. To address these limitations, we propose a mutation-enhanced skill self-evolution framework for building skill-augmented Lean provers. The framework jointly evolves a high-level solving policy and its reference knowledge through progressive and mutation-based updates. Progressive evolution derives local improvements from successful and failed trajectories, while mutation is triggered when no complete proof can be generated, sampling mathematical concepts to produce and select new skill candidates under verifier feedback. We evaluate our method on MiniF2F, PutnamBench, the 2025 International Mathematical Olympiad (IMO 2025), and the 2026 USA Mathematical Olympiad (USAMO 2026). Under the same backbone model, trajectorysampling budget, and test-time compute, our method achieves proof success rates of 100.0%, 90.6%, 4/6, and 4/6, respectively, with GPT-5.5, outperforming the baseline methods. Further analysis shows that concept-guided mutation outperforms random-text-guided mutation by 6.9 and 8.2 percentage points on MiniF2F and PutnamBench, respectively, while solving one additional problem on both IMO 2025 and USAMO 2026.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.