SkillEvoLean: Mutation-enhanced skill evolution for Lean provers

Excerpt

arXiv:2610.01799v1 Announce Type: new Abstract: 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, existi