Research map / Large language models / Agents, code and math

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

NeurIPS 2026 · Large language models › Agents, code and math · approach: LLMs for optimization and heuristics · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Lean Refactor steers a frozen LLM agent with a version- and compile-cost-annotated bank of 9K refactoring strategies, retrieved with objective-specific rules, to shorten and speed up Lean proofs.

Problem

LLM-generated Lean proofs are correct but verbose, slow to compile, and brittle across Lean/Mathlib versions; existing refactoring approaches optimize a single objective, require fine-tuning, and ignore version drift.

Approach

A training-free, plug-and-play agent loop over a densely annotated strategy bank (compile-time reduction and Lean toolchain compatibility metadata), where user objectives are realized as retrieval rules (cosine top-K, compile-cost reranking, or version filtering) over the same bank, with a fine-tuned embedding retriever.

Key results

• Lean Refactor reaches 88.40% average length reduction on miniF2F and 70.38% on PutnamBench with Gemini 3 Flash, versus 87.90% and 57.20% for ProofOptimizer.
• On research benchmarks, Lean Refactor achieves 33.54% (Analysis), 23.55% (FLT), 20.37% (PFR), and 27.69% (PhysLean) length reduction.
• Reranking by compile-cost metadata yields 42.62% relative compile-time reduction on PutnamBench and 60.14% on Putnam2025 (vs. 37.11% and 56.21% for cosine-only retrieval).

Surprising findings

• Cosine-only retrieval on miniF2F yields a -103.98% relative compile-time change, meaning compile time roughly doubles on average, showing token compression can increase compile cost.
• Refactored miniF2F proofs remain type-checkable at more future Lean releases than the originals, and the original verbose proofs trail the shortened variants on PutnamBench in version transfer.

Limitations

• Cross-version evaluation limited to PutnamBench because research projects are pinned to specific toolchains.
• Strategy-level metadata uses cluster-level median and intersection aggregation, so per-strategy marginal contributions are not disentangled.
• ProofOptimizer comparison is not matched in backbone or budget, and its checkpoints are not public.

Experimental setup

Datasets: NuminaMath-1.5 FineLeanCorpus Mathlib4 ATLAS miniF2F PutnamBench Putnam2025 Analysis FLT PFR PhysLean PDE

Benchmarks: miniF2F PutnamBench Putnam2025 Analysis FLT PFR PhysLean PDE Verina

Metrics: relative proof-length reduction compilation-time reduction heartbeat reduction cross-version compatibility zero-shot version transfer

Baselines: ProofOptimizer Claude Code Base Agent Base Agent w/o Retrieval Lean Refactor w/o Retrieval Lean Refactor w/ Random Retrieval

Builds on: ProofOptimizer ImProver Qwen3-Embedding

Closest papers by meaning

• ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.87)
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.86)
• Code Repair with LLMs gives an Exploration-Exploitation Tradeoff (NeurIPS 2024 · similarity 0.85)
• ReGAL: Refactoring Programs to Discover Generalizable Abstractions (ICML 2024 · similarity 0.85)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.85)
• SlopCodeBench: Benchmarking How Coding Agents Degrade Over Long-Horizon Iterative Tasks (NeurIPS 2026 · similarity 0.85)