Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Summary
Lean Refactor presents a retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs, achieving significant compression and compilation-time reduction.
View Cached Full Text
Cached at: 05/22/26, 02:20 PM
Paper page - Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Source: https://huggingface.co/papers/2605.20244
Abstract
Lean Refactor presents a retrieval-augmented agentic framework that improves Lean proof refactoring by addressing multi-objective optimization, version compatibility, and scalability challenges through curated strategy databases and version-filtered retrieval.
We present Lean Refactor, a plug-and-playretrieval-augmented agentic frameworkfor multi-objective, controllable, andversion-robust refactoringofLean 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 versionsand expected compilation-cost reduction. Experiments show over 70%token-level compressionon 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 strongerzero-shot version transferto future Lean releases than their unrefactored counterparts.
View arXiv pageView PDFProject pageAdd to collection
Get this paper in your agent:
hf papers read 2605\.20244
Don’t have the latest CLI?curl \-LsSf https://hf\.co/cli/install\.sh \| bash
Models citing this paper0
No model linking this paper
Cite arxiv.org/abs/2605.20244 in a model README.md to link it from this page.
Datasets citing this paper0
No dataset linking this paper
Cite arxiv.org/abs/2605.20244 in a dataset README.md to link it from this page.
Spaces citing this paper0
No Space linking this paper
Cite arxiv.org/abs/2605.20244 in a Space README.md to link it from this page.
Collections including this paper0
No Collection including this paper
Add this paper to acollectionto link it from this page.
Similar Articles
AgRefactor: Self-Evolving Agentic Workflow for HLS Compatibility and Performance
AgRefactor is an LLM-based multi-agent workflow for refactoring software into HLS-compatible programs, featuring a self-evolving memory system and automated refactoring tools, achieving significant speedups on real-world benchmarks.
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
This paper introduces Discover and Prove (DAP), an open-source agentic framework for automated theorem proving in Lean 4 that tackles 'Hard Mode' problems where the answer must be discovered independently before formal proof construction. The work releases new Hard Mode benchmark variants and achieves state-of-the-art results while revealing a significant gap between LLM answer accuracy (>80%) and formal prover success (<10%).
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
OpenProver is an open-source system for LLM-driven automated theorem proving using Lean 4, featuring a Planner-Worker-Verifier architecture and both autonomous and interactive modes. It enables reproducible evaluation and human-AI synergy in mathematical proof search.
Process-Verified Reinforcement Learning for Theorem Proving via Lean
This paper presents Process-Verified Reinforcement Learning, using the Lean proof assistant as a process oracle to provide fine-grained tactic-level feedback during training, improving theorem proving performance.
OProver: A Unified Framework for Agentic Formal Theorem Proving
OProver is a unified framework for agentic formal theorem proving in Lean 4 that iteratively improves proof generation through training with verified proofs and compiler feedback, achieving state-of-the-art results on multiple benchmarks.