Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913146621394944 |
|---|---|
| author | Lu, Jialin Kong, Soonho Stehling, Rodrigo Yang, Kaiyu Wang, Zhangyang Sun, Weiran Chen, Wuyang |
| author_facet | Lu, Jialin Kong, Soonho Stehling, Rodrigo Yang, Kaiyu Wang, Zhangyang Sun, Weiran Chen, Wuyang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_20244 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search Lu, Jialin Kong, Soonho Stehling, Rodrigo Yang, Kaiyu Wang, Zhangyang Sun, Weiran Chen, Wuyang Logic in Computer Science Artificial Intelligence Computation and Language Machine Learning Software Engineering 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. |
| title | Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search |
| topic | Logic in Computer Science Artificial Intelligence Computation and Language Machine Learning Software Engineering |
| url | https://arxiv.org/abs/2605.20244 |