大型语言模型（LLMs）已被用于在 Lean 等证明助手中生成数学定理的形式化证明。然而，我们经常希望根据证明的后续用途，针对各种标准优化形式化证明。例如，我们可能希望证明符合某种风格，或者易于阅读、简洁或模块化结构。拥有适当优化的证明对于学习任务也很重要，尤其是因为人类编写的证明可能不适合该目的。为此，我们研究了一种新的自动证明优化问题：重写证明，使其正确并针对长度或可读性等任意标准进行优化。作为第一个自动证明优化方法，我们提出了 ImProver，这是一个大型语言模型代理，它重写证明以优化 Lean 中任意用户定义的指标。我们发现，将 LLMs 朴素地应用于证明优化效果不佳，我们在 ImProver 中加入了各种改进，例如在一种新颖的链式状态技术中使用符号 Lean 上下文，以及错误校正和检索。我们测试了 ImProver 对真实世界的本科、竞赛和研究级数学定理的重写，发现 ImProver 能够重写证明，使其更短、更模块化、更易读。