Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle across library versions, yet existing refactoring works overlook three practical challenges: 1) Lean refactoring is natively multi-objective (proof length, compilation cost, and version compatibility are often in tension); 2) Lean repositories have fragile compatibility, whereas LLM releases are unaware of Lean/Mathlib versions; 3) Training-based pipelines require repeated fine-tuning with each new LLM release, scaling neither with model churn nor with Lean's release cycle. Lean Refactor steers a frozen agentic LLM with retrievals from a curated database of multi-objective refactoring strategies, each densely annotated with metadata such as supported Lean/Mathlib versions and expected compilation-cost reduction. Experiments show over 70% token-level compression on competition benchmarks, over 20% on research repositories, and up to 60% compilation-time reduction, outperforming prior work and Claude Code. Version-filtered retrieval further improves compression on the target Lean version, and refactored miniF2F proofs exhibit stronger zero-shot version transfer to future Lean releases than their unrefactored counterparts.

📋 한 줄 요약

**[Lean Proof Refactoring / Agentic LLM]** Lean Refactor가 retrieval-augmented frozen LLM agent로 다목적·버전 강건 proof 리팩토링 — competition 70%·repository 20% token 압축·60% compile-time 감소, Claude Code 능가.

🎯 핵심 기여도

LLM 생성 Lean proof가 correct-but-verbose하고 library version에 brittle하지만 기존 refactoring 작업이 3 실용 도전(다목적성·fragile 버전 호환·model churn마다의 retraining 필요)을 간과함을 진단.
Lean Refactor 제안 — plug-and-play retrieval-augmented agentic framework로 multi-objective·controllable·version-robust Lean proof 리팩토링.
Frozen agentic LLM을 curated database의 multi-objective refactoring strategy retrieval로 steer, 각 strategy는 supported Lean/Mathlib version·expected compilation-cost 감소 등 metadata로 densely annotated.
실험에서 70% 이상 token-level compression(competition), 20% 이상(research repo), 최대 60% compilation-time 감소 — prior work·Claude Code outperform.

💡 핵심 아이디어

Lean proof 리팩토링은 fine-tuning 없이도 frozen agentic LLM에 multi-objective·version-aware refactoring strategy database를 RAG로 제공하면 다목적성·버전 호환·model churn 비용을 동시에 해결 가능하며, version-filtered retrieval은 target Lean release에 zero-shot transfer까지 강화한다.

🔬 기술적 접근법

**방법론**: Lean Refactor — RAG agentic framework.
**핵심 기법**: (1) Frozen agentic LLM이 fine-tuning 없이 동작, (2) Curated database의 multi-objective refactoring strategy(proof length·compile cost·version compatibility)를 retrieval, (3) 각 strategy에 supported Lean/Mathlib version·expected cost reduction 등 dense metadata annotation, (4) Version-filtered retrieval로 target version 정렬, (5) Refactored miniF2F proof가 future Lean release에 zero-shot transfer.

📊 주요 결과

Competition 벤치마크 token 70% 이상 압축.
Research repository 20% 이상 압축.
최대 60% compilation-time 감소.
Prior work·Claude Code 모두 outperform.
Version-filtered retrieval로 target version 압축 추가 개선, refactored proof의 future Lean release 강한 zero-shot transfer.

💭 의의 및 한계

**의의**: LLM 생성 proof의 brittleness·verbosity 동시 해결, RAG 기반 frozen agent로 model churn·Lean cycle 양쪽 비용 회피, multi-objective trade-off의 controllable 처리. **한계**: Curated strategy database 구축·유지 비용, Lean/Mathlib 특화로 다른 proof assistant 일반화 별도 작업 필요, strategy metadata 누락 시 retrieval 품질 의존.

🚀 실용적 활용

AI 보조 정리증명·formal verification.
LLM 생성 proof의 production-quality 정제.
Multi-objective code refactoring 일반 패턴 참고.