ImProver: Agent-Based Automated Proof Optimization

Riyaz Ahuja, Jeremy Avigad, Prasad Tetali +1

Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof…