Lean Refactor Arena: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Lean Refactor Arena is a retrieval-augmented, agentic framework for optimizing
Lean 4 proofs.
LLM-generated proofs are notoriously correct-but-verbose and brittle across library versions.
Lean Refactor rewrites these proofs to be shorter, faster to compile, and more robust — using
frozen LLMs guided by a curated database of refactoring strategies with version-specific metadata,
so there is no need to retrain with every new model or Lean release.
Key Results: >70% token-level compression on competition benchmarks |
20%+ compression on research repositories | up to 60% compilation-time reduction |
outperforms prior methods and Claude Code
What Lean Refactor Addresses
1. Competing Optimization Objectives
Proof length, compilation cost, and version compatibility often pull in different directions.
Lean Refactor treats refactoring as a multi-objective, controllable problem, letting you steer
toward the trade-offs that matter for your project.
2. Version Incompatibility
Tools and proofs frequently break across Lean library versions. Version-filtered retrieval
selects strategies with the right version-specific metadata, improving compression on the
target Lean version and enabling stronger zero-shot transfer to future releases.
3. No Retraining Required
Rather than fine-tuning with each new model release, Lean Refactor keeps the LLM frozen and
relies on retrieval over a curated strategy database — a practical, scalable approach that
stays current as models and libraries evolve.
4. Agentic Strategy Search
An agent searches over refactoring strategies to find and apply the transformations that best
compress proofs and reduce compilation time while preserving correctness.
Why Lean Refactor?
Modern LLMs can produce correct Lean proofs, but they are typically verbose, slow to compile, and
fragile when the underlying library changes. Lean Refactor closes this gap by:
- Compressing correct-but-verbose proofs by 70%+ on competition benchmarks
- Cutting compilation time by up to 60%
- Making refactored proofs robust across Lean library versions
- Scaling to research repositories, not just competition problems
- Working with frozen, off-the-shelf LLMs — no retraining needed
Read the paper: Lean Refactor: Multi-Objective Controllable
Proof Optimization via Agentic Strategy Search (arXiv:2605.20244).
Ready to refactor your Lean proofs?
Try Lean Refactor Arena now →
Lean Refactor Arena proof optimization proof compression Lean 4 theorem prover formal mathematics
proof assistant agentic strategy search retrieval augmented generation refactoring strategies
version compatibility compilation time reduction multi-objective controllable optimization
mathlib formal verification automated theorem proving interactive theorem prover dependent type theory
Lean programming language functional programming formal methods proof engineering tactics
LLM generated proofs frozen language models zero-shot transfer library versions