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

arXiv: https://arxiv.org/abs/2605.20244 · HTML: https://mlsanity.com/paper/2605.20244/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 27 of its 47 references that are in the map.
- First posted on arXiv 18 May 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 27 of 27)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [SWE-Perf: Can Language Models Optimize Code Performance on Real-World Repositories?](https://mlsanity.com/paper/2507.12415/) (2025)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [RefactorBench: Evaluating Stateful Reasoning in Language Agents Through Code](https://mlsanity.com/paper/2503.07832/) (2025)
- [Language Models for Code Optimization: Survey, Challenges and Future Directions](https://mlsanity.com/paper/2501.01277/) (2025)
- [ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations](https://mlsanity.com/paper/2510.15700/) (2025)
- [ImProver: Agent-Based Automated Proof Optimization](https://mlsanity.com/paper/2410.04753/) (2024)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [RefAgent: A Multi-agent LLM-based Framework for Automatic Software Refactoring](https://mlsanity.com/paper/2511.03153/) (2025)
- [Tuning LLM-based Code Optimization via Meta-Prompting: An Industrial Perspective](https://mlsanity.com/paper/2508.01443/) (2025)
- [Do Large Language Models Understand Performance Optimization?](https://mlsanity.com/paper/2503.13772/) (2025)
- [Growing Mathlib: maintenance of a large scale mathematical library](https://mlsanity.com/paper/2508.21593/) (2025)
- [PerfCoder: Large Language Models for Interpretable Code Performance Optimization](https://mlsanity.com/paper/2512.14018/) (2025)
- [FasterPy: An LLM-based Code Execution Efficiency Optimization Framework](https://mlsanity.com/paper/2512.22827/) (2025)
- [Refactoring with LLMs: Bridging Human Expertise and Machine Understanding](https://mlsanity.com/paper/2510.03914/) (2025)
- [SemOpt: LLM-Driven Code Optimization via Rule-Based Analysis](https://mlsanity.com/paper/2510.16384/) (2025)

## Built on by (most cited first, 1 of 1)

- [LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs](https://mlsanity.com/paper/2610.11862/) (2026)

## Abstract (arXiv)

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.