Finding Simple Proofs for First-Order Optimization

Large language models (LLMs) are increasingly used in research across mathematics and machine learning, and their impact is shaped by the workflows researchers build around them. A central challenge is to identify tasks where LLM assistance is genuinely useful, design reproducible tool-augmented procedures for those tasks, and structure the underlying problems to exploit these procedures. First-order optimization offers a natural setting for this question: many convergence proofs admit certificate representations that can be searched, simplified, and interpreted. Recent work on performance estimation problems has shown that proofs of convergence for first-order optimization methods can be discovered by searching over a structured space of Lagrangian dual certificates. This paper studies the simplification of such proofs as an optimization problem. Starting from dual certificates, we develop post-processing procedures using tools from sparse optimization and statistical learning. We measure complexity through features such as active hypotheses and residual structure, and introduce methods based on (weighted) $\ell_1$-heuristics, and formulations for discovering simple proofs using intermediate lemmas. Examples on gradient descent, proximal methods, and fast-gradient methods show that these procedures can autonomously prune redundant inequalities, reveal structured proof patterns, and, in the proximal setting, recover standard intermediate lemmas that lead to streamlined proofs. By distilling dense machine-generated certificates into compact proof structures, this workflow acts as a pre-processing step for the final proof, reducing the complexity that must be managed during human interpretation, reuse, and formalization.