A Domain-Specific Harness for End-to-End Automation of Optimization Research

We present AutoOPT, a domain-specific harness for end-to-end automation of optimization research. AutoOPT organizes the discovery of optimal first-order methods into four stages: numerical design through the BnB-PEP methodology; symbolic discovery of the analytic description and a convergence proof through frontier large language models (LLMs); formal verification in the Lean 4 proof assistant; and human interpretation and write-up. We demonstrate the framework on two case studies, each of independent interest. The first, lemniscate acceleration, is a new accelerated gradient method for minimizing the gradient norm of a smooth convex function: after N gradient steps it reduces the squared gradient norm at the optimal O(1/N4) rate, with a constant governed by the lemniscate constant varpi, a classical elliptic-integral constant. The second is the analytic description of ITEM-f, a method previously known only numerically: for L-smooth, μ-strongly convex minimization it contracts the function-value gap at an accelerated linear rate with a per-step factor (1-√μ/L)2. The convergence theorems of both case studies are formalized and machine-checked in Lean 4.