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

Abstract

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/N^{4})$ 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-\sqrt{μ/L})^{2}$. The convergence theorems of both case studies are formalized and machine-checked in Lean 4.

Disclosure

“ntly, frontier models have also begun proving research- level results in optimization theory: an AI agent writing directly in Lean discovered an improved last-iterate rate for anchored gradient descent ascent for minimax optimization [60], GPT 5.6 Sol Pro closed a query-complexity gap open since 1996 in derivative-free convex optimization, with the central lower bound subsequently formalized in Lean [29], and ChatGPT 5.5 produced the first convergence proof for Bregman Douglas–Rachf”

PDF page 4

Classification

Substantial mathematical content or result generation

Multiplier

10

Verified

2026-08-23T05:00:07.597225Z

Structural counts